Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

GibbsGradientKernelEquality: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual same-original Gibbs zero-gradient kernel equality
Samplinglib mathematical lesson

Actual same-original Gibbs zero-gradient kernel equality

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernelEquality.closed_gradient_zero_iff_ae_constant · theorem · Teaching coverage

Read this first

Mathematical statement

For EVERY u in SAME original Gibbs closed-gradient domain, D.closure u=0 IFF its weighted representative is AE ONE real constant. True domain converse is proved from the new constant producer. No spectral-gap/range/Poincare claim.

\[\forall u\in\operatorname{dom}\overline D:\quad\overline Du=0\iff\exists c\in\mathbb R:\ u=c\ \mu\text{-a.e.}\]
Lean statement · closed_gradient_zero_iff_ae_constant

For EVERY u in SAME original Gibbs closed-gradient domain, D.closure u=0 IFF its weighted representative is AE ONE real constant. True domain converse is proved from the new constant producer. No spectral-gap/range/Poincare claim.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem closed_gradient_zero_iff_ae_constant
    (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (D : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)) →ₗ.[ℝ]
      Lp E 2 ((volume : Measure E).tilted (fun x => -W x))) (hD : D.IsClosable)
    (hgraph : ∀ (a : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
      (H : Lp E 2 ((volume : Measure E).tilted (fun x => -W x))), (a,H) ∈ D.graph ↔
      ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
        a =ᵐ[(volume : Measure E).tilted (fun x => -W x)] φ ∧
        H =ᵐ[(volume : Measure E).tilted (fun x => -W x)] gradient φ)
    (u : D.closure.domain) :
    D.closure u=0 ↔ ∃ c : ℝ, (u : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
      =ᵐ[(volume : Measure E).tilted (fun x => -W x)] (fun _ => c)

Exact module and namespace context

Proof roadmap

  1. 1Retain the accepted zero-output implies constant direction

    Actual C1 Gibbs W/partition integrability and the SAME original closable exact D feed the accepted ordinary weak/mollifier and BOTH AE-transfer producer. No new rough derivative or kernel premise is introduced.

  2. 2Produce a real constant-domain witness for the reverse direction

    Given actual AE constant c, the new finite-measure constant producer gives v in SAME original domain, with v=c AE and output0. Normalized tilted Gibbs is genuinely finite.

  3. 3Identify actual quotient and domain elements

    The two representatives are AE equal, so Lp extensionality and subtype extensionality give u=v. Their actual partial outputs agree. This gives full constant kernel equality only; centered residual/range/Poincare and BL remain separate.

Full assumptions and notation

All objects and hypotheses

  • Full finite real Hilbert/Borel E including dimension0. Fix SAME original real weighted-L2 partial-linear gradient D with exact compact-C-infinity genuine gradient graph and closability BEFORE all queried functions or classes.
  • mu is exactly volume.tilted(-W); W is C1 and exp(-W) is genuinely integrable against canonical full-space volume. Positive normalized density and both AE transfer directions come from the accepted one-way theorem.
  • u is in SAME D.closure.domain. Constant-domain converse is produced, not assumed as a final kernel certificate.

Mathematical proof

1. Retain the accepted zero-output implies constant direction

Actual C1 Gibbs W/partition integrability and the SAME original closable exact D feed the accepted ordinary weak/mollifier and BOTH AE-transfer producer. No new rough derivative or kernel premise is introduced.

\[\overline Du=0\Longrightarrow\exists c:\ u=c\ \mu\text{-a.e.}\]
Corresponding Lean step

GibbsGradientKernel.closed_gradient_zero_ae_constant

2. Produce a real constant-domain witness for the reverse direction

Given actual AE constant c, the new finite-measure constant producer gives v in SAME original domain, with v=c AE and output0. Normalized tilted Gibbs is genuinely finite.

\[\exists v\in\operatorname{dom}\overline D:\ v=c\ \mu\text{-a.e.},\quad\overline Dv=0.\]
Corresponding Lean step

WeightedC1GradientDomain.constants_in_closed_gradient

3. Identify actual quotient and domain elements

The two representatives are AE equal, so Lp extensionality and subtype extensionality give u=v. Their actual partial outputs agree. This gives full constant kernel equality only; centered residual/range/Poincare and BL remain separate.

\[u=v\quad\text{in the SAME domain}\Longrightarrow\overline Du=\overline Dv=0.\]
Corresponding Lean step

Lp.ext; Subtype.ext; closed_gradient_zero_iff_ae_constant

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · closed_gradient_zero_iff_ae_constant

Retain the accepted zero-output implies constant direction; Produce a real constant-domain witness for the reverse direction; Identify actual quotient and domain elements

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem closed_gradient_zero_iff_ae_constant
    (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (D : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)) →ₗ.[ℝ]
      Lp E 2 ((volume : Measure E).tilted (fun x => -W x))) (hD : D.IsClosable)
    (hgraph : ∀ (a : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
      (H : Lp E 2 ((volume : Measure E).tilted (fun x => -W x))), (a,H) ∈ D.graph ↔
      ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
        a =ᵐ[(volume : Measure E).tilted (fun x => -W x)] φ ∧
        H =ᵐ[(volume : Measure E).tilted (fun x => -W x)] gradient φ)
    (u : D.closure.domain) :
    D.closure u=0 ↔ ∃ c : ℝ, (u : Lp ℝ 2 ((volume : Measure E).tilted (fun x => -W x)))
      =ᵐ[(volume : Measure E).tilted (fun x => -W x)] (fun _ => c) := by
  constructor
  · exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel.closed_gradient_zero_ae_constant
      W hW hI D hD hgraph u
  · rintro ⟨c,hc⟩
    obtain ⟨v,hv,hvz⟩ := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.constants_in_closed_gradient _ D hD hgraph c
    have he : u=v := Subtype.ext (Lp.ext (hc.trans hv.symm))
    rwa [he]

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernelEquality

Exact module and namespace context

Scope and omitted-condition boundaries
  • Actual finite real Hilbert/Borel E including0. Fix actual finite mu and SAME original closable exact compact-C-infinity gradient D BEFORE ALL C1 f with actual MemLp f2mu and MemLp gradientf2mu. Genuine smooth cutoff exhaustion/derivative-product/weighted L2 limits put actual class pair into SAME closure graph, without compact support or extra spatial moment. Finite mu constants are genuinely in original closure domain with outputzero. For actual C1 Gibbs W/exp(-W) integrable, combine actual constants-domain with accepted one-way implication for full zero-output iff AEconstant on SAME D. Actual PBPS common Gaussian J/R/S/Sdensity/positive partitions/sourceC2 alpha beta eta cap and original D_y beforeALL constants/u/directions; real unnormalized y-score C1/L2/boundedgradient from accepted score producer transfers along ONLY explicit reflected density equality S2_y=S_y and enters SAME original closed graph. No R2=R or alternateD equality, global ordinary L1, C-infinity potential, gradient of rough representative, Nontrivial E, spatial moment, supplied domain/fullkernel/spectralgap/Poincare certificate, epsilon0/range/centering/measurablejointselector/core/BL/main/composition. TV never transfers unbounded cost.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Lp.ext
  • Subtype.ext

Mathematical sources

  • PBPS AppC1 authored original-gradient domain prerequisite — Actual finite real Hilbert/Borel E including0. Fix actual finite mu and SAME original closable exact compact-C-infinity gradient D BEFORE ALL C1 f with actual MemLp f2mu and MemLp gradientf2mu. Genuine smooth cutoff exhaustion/derivative-product/weighted L2 limits put actual class pair into SAME closure graph, without compact support or extra spatial moment. Finite mu constants are genuinely in original closure domain with outputzero. For actual C1 Gibbs W/exp(-W) integrable, combine actual constants-domain with accepted one-way implication for full zero-output iff AEconstant on SAME D. Actual PBPS common Gaussian J/R/S/Sdensity/positive partitions/sourceC2 alpha beta eta cap and original D_y beforeALL constants/u/directions; real unnormalized y-score C1/L2/boundedgradient from accepted score producer transfers along ONLY explicit reflected density equality S2_y=S_y and enters SAME original closed graph. No R2=R or alternateD equality, global ordinary L1, C-infinity potential, gradient of rough representative, Nontrivial E, spatial moment, supplied domain/fullkernel/spectralgap/Poincare certificate, epsilon0/range/centering/measurablejointselector/core/BL/main/composition. TV never transfers unbounded cost.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.