Samplinglib mathematical lesson

Actual centered Gibbs original-gradient residual limit

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredGibbsResolventLimit.gibbs_centered_resolvent_sequence · theorem · Teaching coverage

Read this first

Mathematical statement

For every genuinely centered weighted L2 forcing and positive epsilon sequence→0, derive true f integrability and construct u_n in SAME original Gibbs D.closure.domain, retaining actual variational and ordinary local weak-gradient integrability facts; epsilon_n*u_n tends0 strongly.

\[\mu=Z^{-1}e^{-W}dx,\quad f\in L^2(\mu),\ \int f\,d\mu=0\Longrightarrow\exists u_n\in\operatorname{dom}\overline D:\ \varepsilon_nu_n\to0\text{ in }L^2(\mu).\]

Lean statement · gibbs_centered_resolvent_sequence

For every genuinely centered weighted L2 forcing and positive epsilon sequence->0, derive true f integrability and construct u_n in SAME original Gibbs D.closure.domain, retaining actual variational and ordinary local weak-gradient integrability facts; epsilon_n*u_n tends0 strongly.

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 gibbs_centered_resolvent_sequence
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (G : Lp E 2 μ), (a,G) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ G =ᵐ[μ] gradient φ) →
      ∀ f : Lp ℝ 2 μ, (∫ x, f x ∂μ)=0 →
      ∀ (ε : ℕ → ℝ), (∀ n, 0 < ε n) → Tendsto ε atTop (𝓝 0) →
      Integrable (fun x => f x) μ ∧
      ∃ u : ℕ → D.closure.domain,
        (∀ n, (∀ v : D.closure.domain,
          ε n*inner ℝ (u n : Lp ℝ 2 μ) (v : Lp ℝ 2 μ)+
            inner ℝ (D.closure (u n)) (D.closure v)=inner ℝ f (v : Lp ℝ 2 μ)) ∧
          LocallyIntegrable (fun x => (u n : Lp ℝ 2 μ) x) ∧
          LocallyIntegrable (fun x => D.closure (u n) x) ∧
          (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
            Integrable (fun x => ψ x*inner ℝ (D.closure (u n) x) a) ∧
            Integrable (fun x => (u n : Lp ℝ 2 μ) x*fderiv ℝ ψ x a) ∧
            (∫ x, ψ x*inner ℝ (D.closure (u n) x) a)=
              -∫ x, (u n : Lp ℝ 2 μ) x*fderiv ℝ ψ x a)) ∧
        Tendsto (fun n => ε n • (u n : Lp ℝ 2 μ)) atTop (𝓝 0)

Exact module and namespace context

Proof roadmap

1Derive actual probability and L2 separability
The true integrable positive Gibbs exponential normalizes to a probability. Finite-dimensional Borel E is countably generated; genuine finite mu and separable real coefficients give scalar L2 second-countability, with Fact2≠top explicit. L2 is not assumed finite-dimensional.
2Construct actual variational solutions in the SAME operator
For each epsilon use accepted WeightedResolvent for that SAME original D, then choose actual witnesses. Retain all variational tests, ordinary local integrability and every legal compact C1 directional weak-gradient identity. Choices are fiberwise, not jointly measurable.
3Prove forcing integrability and kernel orthogonality
Actual probability/L2 gives f in L1. The accepted SAME original Gibbs zero-gradient theorem gives every kernel representative as one AE constant c. Actual L2 inner integral and quotient AE substitution give c*integral f=0.
4Apply the compiled genuine Hilbert limit
Feed actual closedness, scalarL2 separability, all true variational equations and the just-derived kernel orthogonality into the new shared theorem. Return actual strong residualzero, not a supplied spectralgap/range certificate.
5Keep source truth and tests explicit
True nonquadratic eta1/2 and actual dimension0 constant7 Gibbs law exercise the actual source domains. A genuine closed zero operator with forcing7 has scaled residual7, showing kernel orthogonality cannot be dropped. No Poincare/BL/full source result is inferred.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real Hilbert Borel fullspace E including0, genuine C1 W and integrable exp(-W) against volume. Actual normalized probability mu=volume.tilted(-W), positive normalizer and finite-measure scalarL2 separability are derived. SAME exact original compact-smooth gradient D is closable before ALL f/epsilon.
Genuine f in L2(mu) with actual mean integral0; f integrability is derived from true probability/L2 and returned. Every positive epsilon sequence tends0; actual variational solutions are constructed rather than supplied.

Mathematical proof

1. Derive actual probability and L2 separability

The true integrable positive Gibbs exponential normalizes to a probability. Finite-dimensional Borel E is countably generated; genuine finite mu and separable real coefficients give scalar L2 second-countability, with Fact2≠top explicit. L2 is not assumed finite-dimensional.

\[\mu(E)=1,\quad L^2(\mu)\text{ is separable}.\]

Corresponding Lean step

isProbabilityMeasure_tilted; MeasureTheory.Lp.SecondCountableTopology

2. Construct actual variational solutions in the SAME operator

For each epsilon use accepted WeightedResolvent for that SAME original D, then choose actual witnesses. Retain all variational tests, ordinary local integrability and every legal compact C1 directional weak-gradient identity. Choices are fiberwise, not jointly measurable.

\[\varepsilon_n\langle u_n,v\rangle+\langle\overline Du_n,\overline Dv\rangle=\langle f,v\rangle.\]

Corresponding Lean step

WeightedResolvent.weak_resolvent_distributional; Classical.choose

3. Prove forcing integrability and kernel orthogonality

Actual probability/L2 gives f in L1. The accepted SAME original Gibbs zero-gradient theorem gives every kernel representative as one AE constant c. Actual L2 inner integral and quotient AE substitution give c*integral f=0.

\[\langle f,v\rangle=\int fc\,d\mu=c\int f\,d\mu=0\quad(v\in\ker\overline D).\]

Corresponding Lean step

GibbsGradientKernel.closed_gradient_zero_ae_constant; MemLp.integrable; L2.inner_def; integral_mul_const

4. Apply the compiled genuine Hilbert limit

Feed actual closedness, scalarL2 separability, all true variational equations and the just-derived kernel orthogonality into the new shared theorem. Return actual strong residualzero, not a supplied spectralgap/range certificate.

\[\varepsilon_nu_n\to0\quad L^2(\mu).\]

Corresponding Lean step

ScaledClosedGraphResolvent.scaled_resolvent_sequence_tendsto_zero

5. Keep source truth and tests explicit

True nonquadratic eta1/2 and actual dimension0 constant7 Gibbs law exercise the actual source domains. A genuine closed zero operator with forcing7 has scaled residual7, showing kernel orthogonality cannot be dropped. No Poincare/BL/full source result is inferred.

\[D=0,\ f=7\Longrightarrow\varepsilon u_\varepsilon=7\not\to0.\]

Corresponding Lean step

Tests.ScaledResolventLimit.noncentered_constant_residual; Tests.ScaledResolventLimit.zeroOperator_isClosed

Lean verification

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

Lean proof · gibbs_centered_resolvent_sequence

Derive actual probability and L2 separability; Construct actual variational solutions in the SAME operator; Prove forcing integrability and kernel orthogonality; Apply the compiled genuine Hilbert limit; Keep source truth and tests explicit

Download module (.lean)

theorem gibbs_centered_resolvent_sequence
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (G : Lp E 2 μ), (a,G) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ G =ᵐ[μ] gradient φ) →
      ∀ f : Lp ℝ 2 μ, (∫ x, f x ∂μ)=0 →
      ∀ (ε : ℕ → ℝ), (∀ n, 0 < ε n) → Tendsto ε atTop (𝓝 0) →
      Integrable (fun x => f x) μ ∧
      ∃ u : ℕ → D.closure.domain,
        (∀ n, (∀ v : D.closure.domain,
          ε n*inner ℝ (u n : Lp ℝ 2 μ) (v : Lp ℝ 2 μ)+
            inner ℝ (D.closure (u n)) (D.closure v)=inner ℝ f (v : Lp ℝ 2 μ)) ∧
          LocallyIntegrable (fun x => (u n : Lp ℝ 2 μ) x) ∧
          LocallyIntegrable (fun x => D.closure (u n) x) ∧
          (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
            Integrable (fun x => ψ x*inner ℝ (D.closure (u n) x) a) ∧
            Integrable (fun x => (u n : Lp ℝ 2 μ) x*fderiv ℝ ψ x a) ∧
            (∫ x, ψ x*inner ℝ (D.closure (u n) x) a)=
              -∫ x, (u n : Lp ℝ 2 μ) x*fderiv ℝ ψ x a)) ∧
        Tendsto (fun n => ε n • (u n : Lp ℝ 2 μ)) atTop (𝓝 0) := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph f hf ε hε hε0
  letI : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  have hfi : Integrable (fun x => f x) μ := (Lp.memLp f).integrable (by norm_num)
  letI : Fact ((2 : ENNReal) ≠ ⊤) := ⟨by norm_num⟩
  letI : SecondCountableTopology (Lp ℝ 2 μ) := inferInstance
  have hsol (n : ℕ) :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolvent.weak_resolvent_distributional
      W hW hI D hD hgraph (ε n) (hε n) f
  let u (n : ℕ) : D.closure.domain := Classical.choose (hsol n)
  have hu (n : ℕ) := Classical.choose_spec (hsol n)
  refine ⟨hfi,u,?_,?_⟩
  · intro n
    exact ⟨(hu n).1,(hu n).2.1,(hu n).2.2.1,(hu n).2.2.2.1⟩
  · have hk : ∀ v : D.closure.domain, D.closure v=0 → inner ℝ f (v : Lp ℝ 2 μ)=0 := by
      intro v hv
      obtain ⟨c,hc⟩ :=
        AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel.closed_gradient_zero_ae_constant
          W hW hI D hD hgraph v hv
      rw [L2.inner_def]
      calc
        _ = ∫ x, f x*c ∂μ := integral_congr_ae (by
          filter_upwards [hc] with x hx
          simp [hx,mul_comm])
        _ = 0 := by rw [integral_mul_const,hf,zero_mul]

    exact (AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ScaledClosedGraphResolvent.scaled_resolvent_sequence_tendsto_zero
      D.closure hD.closure_isClosed f ε hε hε0 u (fun n => (hu n).1) hk).1

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredGibbsResolventLimit

Exact module and namespace context

Scope and omitted-condition boundaries

Fix real complete Hilbert H,K and SAME actual closed partial linear D before forcing f, positive epsilon sequence→0 and actual variational solutions u_n. H separable explicitly; actual finite-dimensional Borel Gibbs E gives genuine scalar L2 separability by countably generated finite measure, not finite-dimensional L2. Actual energy/scaled domain, Riesz WeakDual sequential compactness, WithLp2 genuine graph double-orthogonal and forcing orthogonal to EVERY kernel give strong epsilon*u_n→0 and epsilon*D(u_n)→0 without Poincare or uniform unscaled u. True C1 Gibbs W/positive exponential normalizer/actual normalized probability and SAME exact original compact-smooth closable gradient beforeALLf; genuine mean-zero L2 forcing is integrable and kernel-orthogonal via actual AEconstant. Construct actual positive-epsilon variational solutions, retaining ordinary localL1/weakC1 test integrabilities. Actual common PBPS J/R/S/reflected law/sourceC2 alpha-beta/eta cap/positive partitions and originalD_y beforeALLf/epsilon; fiberwise only. No epsilon0 solution/range/unscaled uniform bound/extra spatial moment/supplied weak-limit or graph or residual certificate/Poincare/BL/core/adjoint/jointselector/normalized conditional-score derivative/both main/composition; TV never transfers unbounded expectedcost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

isProbabilityMeasure_tilted
MeasureTheory.Lp.SecondCountableTopology
MemLp.integrable
L2.inner_def
integral_mul_const

Mathematical sources

PBPS AppC1 omitted-background analytic prerequisite — Fix real complete Hilbert H,K and SAME actual closed partial linear D before forcing f, positive epsilon sequence->0 and actual variational solutions u_n. H separable explicitly; actual finite-dimensional Borel Gibbs E gives genuine scalar L2 separability by countably generated finite measure, not finite-dimensional L2. Actual energy/scaled domain, Riesz WeakDual sequential compactness, WithLp2 genuine graph double-orthogonal and forcing orthogonal to EVERY kernel give strong epsilon*u_n->0 and epsilon*D(u_n)->0 without Poincare or uniform unscaled u. True C1 Gibbs W/positive exponential normalizer/actual normalized probability and SAME exact original compact-smooth closable gradient beforeALLf; genuine mean-zero L2 forcing is integrable and kernel-orthogonal via actual AEconstant. Construct actual positive-epsilon variational solutions, retaining ordinary localL1/weakC1 test integrabilities. Actual common PBPS J/R/S/reflected law/sourceC2 alpha-beta/eta cap/positive partitions and originalD_y beforeALLf/epsilon; fiberwise only. No epsilon0 solution/range/unscaled uniform bound/extra spatial moment/supplied weak-limit or graph or residual certificate/Poincare/BL/core/adjoint/jointselector/normalized conditional-score derivative/both main/composition; TV never transfers unbounded expectedcost.

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