Samplinglib mathematical lesson

Actual compact weak Poisson: original weighted gradient domain and scalar coercivity

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeightedPoissonCoercivity.compact_weak_poisson_weighted_coercivity · theorem · Teaching coverage

Read this first

Mathematical statement

From the stated genuine compact weak data and original gradient interface, Derive actual weighted MemLp2 of v,G,A=inner(gradientW,G)-F. Return actual vW,AW,GW L2 classes with all three mu-AE links, (vW,GW) in the SAME D.closure graph, and m*norm(GW)^2≤norm(AW)^2. The actual ordinary smooth sequence, common compact weighted transfer and generator-gradient limits are produced internally. This is compact scalar coercivity, not a rough Hessian, full Bochner/adjoint/operator-core identity, global cutoff result, epsilon-zero/Poincare/BL or complete main theorem.

\[\mu=Z^{-1}e^{-W}dx,\quad A=\langle\nabla W,G\rangle-F:\quad(v_W,G_W)\in\operatorname{graph}\overline D,\quad m\|G_W\|_{L^2(\mu)}^2\le\|A_W\|_{L^2(\mu)}^2.\]

Lean statement · compact_weak_poisson_weighted_coercivity

From the stated genuine compact weak data and original gradient interface, Derive actual weighted MemLp2 of v,G,A=inner(gradientW,G)-F. Return actual vW,AW,GW L2 classes with all three mu-AE links, (vW,GW) in the SAME D.closure graph, and m*norm(GW)^2<=norm(AW)^2. The actual ordinary smooth sequence, common compact weighted transfer and generator-gradient limits are produced internally. This is compact scalar coercivity, not a rough Hessian, full Bochner/adjoint/operator-core identity, global cutoff result, epsilon-zero/Poincare/BL or complete main theorem.

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 compact_weak_poisson_weighted_coercivity
    (W : E → ℝ) (hW : ContDiff ℝ 2 W)
    (hI : Integrable (fun x => Real.exp (-W x))) (hZ : 0 < ∫ x, Real.exp (-W x))
    (m : ℝ) (hl : ∀ x a, m * ‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a)
    (μ : Measure E) (hμ : μ = (volume : Measure E).tilted (fun x => -W x))
    (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ)
    (hD : D.IsClosable)
    (hgraph : ∀ a H, (a,H) ∈ D.graph ↔
      ∃ ψ : E → ℝ, ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧
        a =ᵐ[μ] ψ ∧ H =ᵐ[μ] gradient ψ)
    (v F : E → ℝ) (G : E → E) (K : Set E) (hK : IsCompact K)
    (hv : tsupport v ⊆ K) (hF : tsupport F ⊆ K) (hG : tsupport G ⊆ K)
    (hv2 : MemLp v 2 volume) (hF2 : MemLp F 2 volume) (hG2 : MemLp G 2 volume)
    (hd : ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (G x) a) volume ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) volume ∧
      (∫ x, ψ x * inner ℝ (G x) a) = -∫ x, v x * fderiv ℝ ψ x a)
    (hweak : ∀ ψ : E → ℝ, ContDiff ℝ 2 ψ → HasCompactSupport ψ →
      Integrable (fun x => v x * Laplacian.laplacian ψ x) volume ∧
      Integrable (fun x => F x * ψ x) volume ∧
      (∫ x, v x * Laplacian.laplacian ψ x) = ∫ x, F x * ψ x) :
    let A := fun x => inner ℝ (gradient W x) (G x)-F x
    MemLp v 2 μ ∧ MemLp G 2 μ ∧ MemLp A 2 μ ∧
    ∃ vW AW : Lp ℝ 2 μ, ∃ GW : Lp E 2 μ,
      vW =ᵐ[μ] v ∧ AW =ᵐ[μ] A ∧ GW =ᵐ[μ] G ∧
      (vW,GW) ∈ D.closure.graph ∧ m * ‖GW‖^2 ≤ ‖AW‖^2

Exact module and namespace context

Proof roadmap

1Derive one actual ordinary smooth graph sequence
Apply the accepted compact weak-Poisson graph producer to genuine supports/L2 and both weak equations. It constructs ONE real Schwartz sequence with common compact Kprime and simultaneous function, gradient and Laplacian limits. It does not assert K is inside Kprime; take Kbar=K union Kprime. All gradient/Laplacian supports of the smooth terms lie in Kprime by derivative locality, including dimension zero.
2Bound the true normalized density and local drift on that same compact
Continuity yields finite upper bounds for rho=exp(-W)/Z and norm(gradientW) on Kbar. Use the actual tilted with-density definition and restriction/measure monotonicity to prove mu.restrict(Kbar)≤c*volume. The normalized measure is genuine probability from actual integrability; no global bounded drift, tails or position moments are assumed.
3Produce weighted L2 classes and the same three norm limits
Support-restricted seminorm and finite measure domination imply actual weighted MemLp for every compact-supported datum and term, then norm_mu(error)≤sqrt(c)*norm_dx(error). Indicator/restriction and quotient subtraction are handled explicitly. Squeeze all three errors to zero using the SAME sequence; convergence is in true L2 quotients, not pointwise. The bound is stated using exact ENNReal exponent/toReal operations at p=2.
4Derive the actual drift and generator convergence
Inner-product norm and the compact drift bound supply measurable MemLp of inner(gradientW,G) and every approximant. Prove the same bound for actual differences, identify toLp subtraction by all AE links, and squeeze drift errors. Subtract the weighted Laplacian limits to produce A_n=inner(gradientW,gradientphi_n)-Deltaphi_n → A; rough G and F are never classically differentiated.
5Pass the same function-gradient pairs through the original closed graph
Each actual phi_n is compact C-infinity, so the original exact graph characterization puts its AE-linked weighted function/gradient pair in D.graph. Product convergence and closability put the limiting pair in the topological graph closure, exactly D.closure.graph. No new gradient domain or final-domain premise replaces the original D.
6Normalize the actual compact Bochner inequality exactly once
Apply the accepted C2-potential/compact-smooth Bochner identity and its arbitrary-real curvature consequence to each phi_n. Its L=Delta-innerdrift is minus A_n, so squared scalars agree. The true tilted integral divides by positive Z exactly once; norm-square integrals use actual MemLp/AE links. No second-derivative limit or rough Hessian identification is needed for this scalar inequality.
7Pass both actual norms to the limit and expose the exact boundary
Norm and squaring are continuous; the simultaneous weighted gradient and generator limits pass each scalar inequality to the original G/A. Return actual weighted MemLp and three AE-linked quotient classes with same-D closure membership. Signed m is permitted. The result is a local scalar prerequisite, with no global/core/adjoint/Poincare/BL or source-completion claim.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real Hilbert/Borel E, canonical full-space volume, including dimension zero. W is C2, exp(-W) genuinely integrable with positive Z. The actual given measure mu equals volume.tilted(-W), hence is the normalized Gibbs law. The Hessian quadratic form is bounded below by m times squared norm for every point/vector; m is any real number, not necessarily positive.
The original partial real-linear gradient D on actual weighted L2 is closable. Its graph consists exactly of AE classes of C-infinity compact functions and their genuine classical gradients. This is an original structural interface, not a supplied final closure-domain, coercivity, adjoint or core certificate.
Pointwise real v,F and vector G are global ordinary-volume MemLp2 with topological supports in the same compact K. Every real C1 compact psi/every direction a has both legal L1 products and integral psi*inner(G,a)=-integral v*D_a psi. Every real C2 compact psi has both legal L1 products and integral v*Delta psi=integral F*psi. No approximation, weighted class/convergence, domain membership or scalar inequality is an input.

Mathematical proof

1. Derive one actual ordinary smooth graph sequence

Apply the accepted compact weak-Poisson graph producer to genuine supports/L2 and both weak equations. It constructs ONE real Schwartz sequence with common compact Kprime and simultaneous function, gradient and Laplacian limits. It does not assert K is inside Kprime; take Kbar=K union Kprime. All gradient/Laplacian supports of the smooth terms lie in Kprime by derivative locality, including dimension zero.

\[(\varphi_n,\nabla\varphi_n,\Delta\varphi_n)\to(v,G,F)\text{ in }L^2(dx),\quad\bar K=K\cup K\prime.\]

Corresponding Lean step

CompactPoissonSmoothGraph.compact_weak_poisson_smooth_graph_approximation; gradient_support; laplacian_support

2. Bound the true normalized density and local drift on that same compact

Continuity yields finite upper bounds for rho=exp(-W)/Z and norm(gradientW) on Kbar. Use the actual tilted with-density definition and restriction/measure monotonicity to prove mu.restrict(Kbar)≤c*volume. The normalized measure is genuine probability from actual integrability; no global bounded drift, tails or position moments are assumed.

\[\mu|_{\bar K}\le c\,dx,\quad c<\infty,\quad\|\nabla W(x)\|\le M\ (x\in\bar K).\]

Corresponding Lean step

compact_weight_bound; compact_drift_bound; isProbabilityMeasure_tilted

3. Produce weighted L2 classes and the same three norm limits

Support-restricted seminorm and finite measure domination imply actual weighted MemLp for every compact-supported datum and term, then norm_mu(error)≤sqrt(c)*norm_dx(error). Indicator/restriction and quotient subtraction are handled explicitly. Squeeze all three errors to zero using the SAME sequence; convergence is in true L2 quotients, not pointwise. The bound is stated using exact ENNReal exponent/toReal operations at p=2.

\[\|h\|_{L^2(\mu)}\le\sqrt c\,\|h\|_{L^2(dx)},\quad\varphi_n\to v,\ \nabla\varphi_n\to G,\ \Delta\varphi_n\to F\text{ in }L^2(\mu).\]

Corresponding Lean step

memLp_compact_domination; norm_compact_domination; compact_convergence

4. Derive the actual drift and generator convergence

Inner-product norm and the compact drift bound supply measurable MemLp of inner(gradientW,G) and every approximant. Prove the same bound for actual differences, identify toLp subtraction by all AE links, and squeeze drift errors. Subtract the weighted Laplacian limits to produce A_n=inner(gradientW,gradientphi_n)-Deltaphi_n → A; rough G and F are never classically differentiated.

\[\|\langle\nabla W,\nabla\varphi_n-G\rangle\|_2\le M\|\nabla\varphi_n-G\|_2,\quad A_n\to A.\]

Corresponding Lean step

drift_memLp; drift_norm_bound; drift_convergence; hAW,hAn,hAT

5. Pass the same function-gradient pairs through the original closed graph

Each actual phi_n is compact C-infinity, so the original exact graph characterization puts its AE-linked weighted function/gradient pair in D.graph. Product convergence and closability put the limiting pair in the topological graph closure, exactly D.closure.graph. No new gradient domain or final-domain premise replaces the original D.

\[(\varphi_{n,W},\nabla\varphi_{n,W})\in\operatorname{graph}D\ \Longrightarrow\ (v_W,G_W)\in\operatorname{graph}\overline D.\]

Corresponding Lean step

LinearPMap.IsClosable.graph_closure_eq_closure_graph; hgraph; hpT.prodMk_nhds hpgT

6. Normalize the actual compact Bochner inequality exactly once

Apply the accepted C2-potential/compact-smooth Bochner identity and its arbitrary-real curvature consequence to each phi_n. Its L=Delta-innerdrift is minus A_n, so squared scalars agree. The true tilted integral divides by positive Z exactly once; norm-square integrals use actual MemLp/AE links. No second-derivative limit or rough Hessian identification is needed for this scalar inequality.

\[m\int e^{-W}\|\nabla\varphi_n\|^2\le\int e^{-W}L_n^2\ \Longrightarrow\ m\|\nabla\varphi_n\|_\mu^2\le\|A_n\|_\mu^2.\]

Corresponding Lean step

WeightedBochner.integrated_bochner_identity; norm_sq_integral; compact_normalized_bochner

7. Pass both actual norms to the limit and expose the exact boundary

Norm and squaring are continuous; the simultaneous weighted gradient and generator limits pass each scalar inequality to the original G/A. Return actual weighted MemLp and three AE-linked quotient classes with same-D closure membership. Signed m is permitted. The result is a local scalar prerequisite, with no global/core/adjoint/Poincare/BL or source-completion claim.

\[m\|G_W\|_\mu^2\le\|A_W\|_\mu^2.\]

Corresponding Lean step

le_of_tendsto_of_tendsto; compact_weak_poisson_weighted_coercivity

Lean verification

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

Lean proof · compact_weak_poisson_weighted_coercivity

Derive one actual ordinary smooth graph sequence; Bound the true normalized density and local drift on that same compact; Produce weighted L2 classes and the same three norm limits; Derive the actual drift and generator convergence; Pass the same function-gradient pairs through the original closed graph; Normalize the actual compact Bochner inequality exactly once; Pass both actual norms to the limit and expose the exact boundary

Download module (.lean)

theorem compact_weak_poisson_weighted_coercivity
    (W : E → ℝ) (hW : ContDiff ℝ 2 W)
    (hI : Integrable (fun x => Real.exp (-W x))) (hZ : 0 < ∫ x, Real.exp (-W x))
    (m : ℝ) (hl : ∀ x a, m * ‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a)
    (μ : Measure E) (hμ : μ = (volume : Measure E).tilted (fun x => -W x))
    (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ)
    (hD : D.IsClosable)
    (hgraph : ∀ a H, (a,H) ∈ D.graph ↔
      ∃ ψ : E → ℝ, ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧
        a =ᵐ[μ] ψ ∧ H =ᵐ[μ] gradient ψ)
    (v F : E → ℝ) (G : E → E) (K : Set E) (hK : IsCompact K)
    (hv : tsupport v ⊆ K) (hF : tsupport F ⊆ K) (hG : tsupport G ⊆ K)
    (hv2 : MemLp v 2 volume) (hF2 : MemLp F 2 volume) (hG2 : MemLp G 2 volume)
    (hd : ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (G x) a) volume ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) volume ∧
      (∫ x, ψ x * inner ℝ (G x) a) = -∫ x, v x * fderiv ℝ ψ x a)
    (hweak : ∀ ψ : E → ℝ, ContDiff ℝ 2 ψ → HasCompactSupport ψ →
      Integrable (fun x => v x * Laplacian.laplacian ψ x) volume ∧
      Integrable (fun x => F x * ψ x) volume ∧
      (∫ x, v x * Laplacian.laplacian ψ x) = ∫ x, F x * ψ x) :
    let A := fun x => inner ℝ (gradient W x) (G x)-F x
    MemLp v 2 μ ∧ MemLp G 2 μ ∧ MemLp A 2 μ ∧
    ∃ vW AW : Lp ℝ 2 μ, ∃ GW : Lp E 2 μ,
      vW =ᵐ[μ] v ∧ AW =ᵐ[μ] A ∧ GW =ᵐ[μ] G ∧
      (vW,GW) ∈ D.closure.graph ∧ m * ‖GW‖^2 ≤ ‖AW‖^2 := by
  subst μ
  let μ := (volume : Measure E).tilted (fun x => -W x)
  let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  obtain ⟨K',hK',φ,hφs,hφv,hφG,hφgrad,hφF⟩ :=
    CompactPoissonSmoothGraph.compact_weak_poisson_smooth_graph_approximation
      v F G K hK hv hF hG hv2 hF2 hG2 hd hweak
  let Kbar := K ∪ K'
  have hKb : IsCompact Kbar := hK.union hK'
  obtain ⟨c,hc,hdom⟩ := compact_weight_bound W hW.continuous Kbar hKb
  obtain ⟨M,hM,hMb⟩ := compact_drift_bound W hW Kbar hKb
  have hvs : Function.support v ⊆ Kbar := (subset_tsupport v).trans (hv.trans Set.subset_union_left)
  have hFs : Function.support F ⊆ Kbar := (subset_tsupport F).trans (hF.trans Set.subset_union_left)
  have hGs : Function.support G ⊆ Kbar := (subset_tsupport G).trans (hG.trans Set.subset_union_left)
  have hps (n : ℕ) : Function.support (φ n : E → ℝ) ⊆ Kbar :=
    (subset_tsupport _).trans ((hφs n).trans Set.subset_union_right)
  have hpgs (n : ℕ) : Function.support (gradient (φ n : E → ℝ)) ⊆ Kbar :=
    (gradient_support _).trans ((hφs n).trans Set.subset_union_right)
  have hpls (n : ℕ) : Function.support (Laplacian.laplacian (φ n : E → ℝ)) ⊆ Kbar :=
    (laplacian_support _).trans ((hφs n).trans Set.subset_union_right)
  have hpl2 (n : ℕ) : MemLp (Laplacian.laplacian (φ n : E → ℝ)) 2 volume := by
    have he : ((Δ (φ n) : SchwartzMap E ℝ) : E → ℝ) =
        Laplacian.laplacian (φ n : E → ℝ) := by
      funext x; exact SchwartzMap.laplacian_apply (φ n) x
    rw [← he]
    exact (Δ (φ n)).memLp 2 volume
  have hplT : Tendsto (fun n => (hpl2 n).toLp _) atTop (𝓝 (hF2.toLp F)) := by
    have he (n : ℕ) : (hpl2 n).toLp _ = (Δ (φ n)).toLp 2 volume := by
      apply Lp.ext
      filter_upwards [(hpl2 n).coeFn_toLp,(Δ (φ n)).coeFn_toLp 2 volume] with x hx hy
      rw [hx,hy,SchwartzMap.laplacian_apply]
    simpa only [he] using hφF
  obtain ⟨hvW,hpW,hpT⟩ := compact_convergence μ volume Kbar hKb.measurableSet c hc hdom
    v (fun n => (φ n : E → ℝ)) hvs hps hv2 (fun n => (φ n).memLp 2 volume) hφv
  obtain ⟨hGW,hpgW,hpgT⟩ := compact_convergence μ volume Kbar hKb.measurableSet c hc hdom
    G (fun n => gradient (φ n : E → ℝ)) hGs hpgs hG2 hφG hφgrad
  obtain ⟨hFW,hplW,hplWT⟩ := compact_convergence μ volume Kbar hKb.measurableSet c hc hdom
    F (fun n => Laplacian.laplacian (φ n : E → ℝ)) hFs hpls hF2 hpl2 hplT
  obtain ⟨hB,hBn,hBT⟩ := drift_convergence μ W hW Kbar M hM hMb
    G (fun n => gradient (φ n : E → ℝ)) hGs hpgs hGW hpgW hpgT
  have hAW : MemLp (fun x => inner ℝ (gradient W x) (G x)-F x) 2 μ := hB.sub hFW
  have hAn (n : ℕ) : MemLp (fun x => inner ℝ (gradient W x) (gradient (φ n : E → ℝ) x)-
      Laplacian.laplacian (φ n : E → ℝ) x) 2 μ := (hBn n).sub (hplW n)
  have hAT : Tendsto (fun n => (hAn n).toLp _) atTop (𝓝 (hAW.toLp _)) := by
    change Tendsto (fun n => (hBn n).toLp _-(hplW n).toLp _) atTop
      (𝓝 (hB.toLp _-hFW.toLp _))
    exact hBT.sub hplWT
  dsimp only
  refine ⟨hvW,hGW,hAW,hvW.toLp _,hAW.toLp _,hGW.toLp _,
    hvW.coeFn_toLp,hAW.coeFn_toLp,hGW.coeFn_toLp,?_,?_⟩
  · rw [← hD.graph_closure_eq_closure_graph]
    apply D.graph.isClosed_topologicalClosure.mem_of_tendsto (hpT.prodMk_nhds hpgT)
    filter_upwards [] with n
    apply D.graph.le_topologicalClosure
    exact (hgraph _ _).mpr ⟨φ n,(φ n).smooth ⊤,HasCompactSupport.of_support_subset_isCompact
      hK' ((subset_tsupport _).trans (hφs n)),(hpW n).coeFn_toLp,(hpgW n).coeFn_toLp⟩
  · apply le_of_tendsto_of_tendsto (hpgT.norm.pow 2 |>.const_mul m) (hAT.norm.pow 2)
    filter_upwards [] with n
    exact compact_normalized_bochner W (φ n : E → ℝ) hW hZ ((φ n).smooth ⊤)
      (HasCompactSupport.of_support_subset_isCompact hK' ((subset_tsupport _).trans (hφs n)))
      m hl (hpgW n) (hAn n)

end Hilbert
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeightedPoissonCoercivity

Exact module and namespace context

Scope and omitted-condition boundaries

Derive genuine compact weighted L2/AE classes vW/GW/AW for actual v/G/(innergradWG-F), same original D.closure graph membership and lambda*normGW^2≤normAW^2 via actual same ordinary-to-weighted smooth sequence. Source fixes originalD before epsilon/f and ONEu before ALLC2chi. No supplied weighted domain/core/convergence/coercivity certificate; no rough classical Hessian or full adjoint/generator-core identity, globalcutoff/tail/Bochner,epsilon0/kernel/range/noncompactlinear/Poincare/BL/jointmeasurablechoice/main/composition. Reflected quarter/fourfold constants exact. TV never transfers unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MemLp.of_measure_le_smul
eLpNorm_le_of_measure_le_smul
eLpNorm_restrict_eq_of_support_subset
memLp_indicator_iff_restrict
IsCompact.bddAbove_image
restrict_withDensity
withDensity_mono
MemLp.of_le_mul
eLpNorm_le_mul_eLpNorm_of_ae_le_mul
LinearPMap.IsClosable.graph_closure_eq_closure_graph
integral_tilted
le_of_tendsto_of_tendsto

Mathematical sources

PBPS AppendixC.1 authored analytic prerequisite — Derive genuine compact weighted L2/AE classes vW/GW/AW for actual v/G/(innergradWG-F), same original D.closure graph membership and lambda*normGW^2<=normAW^2 via actual same ordinary-to-weighted smooth sequence. Source fixes originalD before epsilon/f and ONEu before ALLC2chi. No supplied weighted domain/core/convergence/coercivity certificate; no rough classical Hessian or full adjoint/generator-core identity, globalcutoff/tail/Bochner,epsilon0/kernel/range/noncompactlinear/Poincare/BL/jointmeasurablechoice/main/composition. Reflected quarter/fourfold constants exact. 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.