Actual compact weak Poisson: original weighted gradient domain and scalar coercivity
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeightedPoissonCoercivity.compact_weak_poisson_weighted_coercivity · theorem · Teaching coverage
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.
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.
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‖^2Proof 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.
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.
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.
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.
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.
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.
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.
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
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.
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.CompactWeightedPoissonCoercivityScope 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
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactPoissonSmoothGraph.compact_weak_poisson_smooth_graph_approximationAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedBochner.integrated_bochner_identity
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.