Closed gradients satisfy weighted compact-test integration by parts
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeak.closed_gradient_weighted_ibp · theorem · Teaching coverage
Mathematical statement
Both φ⟨G,v⟩ and u(D_vφ−φD_vW) are μ-integrable, and their integrals have opposite signs. This holds for every graph-closure pair of the same operator D, not just for its original smooth core.
Lean statement · closed_gradient_weighted_ibp
All spaces, the exact graph, closability, representatives, compact C1 test and integrabilities appear explicitly below.
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 closed_gradient_weighted_ibp (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 →
(∀ (u : Lp ℝ 2 μ) (G : Lp E 2 μ), (u,G) ∈ D.graph ↔
∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
u =ᵐ[μ] f ∧ G =ᵐ[μ] gradient f) →
∀ (u : Lp ℝ 2 μ) (G : Lp E 2 μ), (u,G) ∈ D.closure.graph →
∀ (φ : E → ℝ), ContDiff ℝ 1 φ → HasCompactSupport φ → ∀ v : E,
Integrable (fun x => φ x * inner ℝ (G x) v) μ ∧
Integrable (fun x => u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v)) μ ∧
(∫ x, φ x * inner ℝ (G x) v ∂μ) =
- ∫ x, u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v) ∂μProof roadmap
- 1Localize the classical integration by parts
For a smooth core representative f, put F=e^(−W)φ. Both F and its directional derivative are continuous and compactly supported. Products with f or its continuous derivative are therefore integrable for volume. The classical full-space formula has no boundary term. No global boundedness of f or the score is needed.
- 2Normalize the actual Gibbs measure
The continuous strictly positive density exp(−W) is assumed integrable, so its normalizing integral is finite and positive and μ is a probability measure. Multiplying the volume identity by the reciprocal normalization gives the weighted identity. This uses the actual tilted measure, not an abstract measure with supplied IBP.
- 3Represent the tests in L²
Set P=φv and q=D_vφ−φD_vW. The C1 assumptions make both continuous. The derivative of φ vanishes off its topological support, so both tests have compact support even if D_vW grows at infinity. Finite measure and compact continuity imply L² membership.
- 4Establish genuine integrability and representative independence
Products of L² functions are integrable by Cauchy–Schwarz. The pointwise representatives supplied by toLp agree almost everywhere with the explicit tests; transfer both product integrabilities across these equalities. Changing u or G on a null set does not change the conclusion.
- 5Prove the pairing identity on the exact core
Take any pair in D.graph. Its exact graph characterization provides a smooth compact representative f and its genuine gradient. Transfer through the almost-everywhere equalities, use D_vf=⟨∇f,v⟩, and apply the normalized identity. This proves the equality on the whole original graph without assuming it.
- 6Pass to the graph closure by continuity
The two L² pairings are continuous functions on the product Hilbert space. Their equality set is closed and contains D.graph, hence contains its topological closure. Closability identifies that closure with D.closure.graph. This retains precisely the D already used in the weak resolvent.
- 7Return to the readable integral identity
Convert the two Hilbert pairings back to integrals using the same almost-everywhere test representatives. This establishes a weighted weak identity; it does not differentiate u pointwise. Passing to ordinary volume weak derivatives, or invoking elliptic regularity for the resolvent, still requires separate work.
Full assumptions and notation
All objects and hypotheses
- E is any finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. W:E→R is C1 and exp(-W) is integrable for Euclidean volume; μ=volume.tilted(-W) is the actual normalized Gibbs law.
- D is a given closable partial real-linear map from scalar L²(μ) to vector L²(μ). Its original graph is exactly the pairs represented μ-almost everywhere by (f,∇f) for smooth compactly supported f. This is the interface already proved by WeightedGradient, not an assumed integration-by-parts formula.
- (u,G) belongs to the graph of D.closure. The test φ:E→R is C1 with compact support and v is any constant vector. No differentiability of the chosen measurable L² representatives u or G is required.
Mathematical proof
1. Localize the classical integration by parts
For a smooth core representative f, put F=e^(−W)φ. Both F and its directional derivative are continuous and compactly supported. Products with f or its continuous derivative are therefore integrable for volume. The classical full-space formula has no boundary term. No global boundedness of f or the score is needed.
Corresponding Lean step
private compact_directional_ibp: hF,hFc,hDFc,h1,h2,h3,hi; genuine HasFDerivAt product rule
2. Normalize the actual Gibbs measure
The continuous strictly positive density exp(−W) is assumed integrable, so its normalizing integral is finite and positive and μ is a probability measure. Multiplying the volume identity by the reciprocal normalization gives the weighted identity. This uses the actual tilted measure, not an abstract measure with supplied IBP.
Corresponding Lean step
isProbabilityMeasure_tilted hI; ht uses integral_tilted and integral_const_mul
3. Represent the tests in L²
Set P=φv and q=D_vφ−φD_vW. The C1 assumptions make both continuous. The derivative of φ vanishes off its topological support, so both tests have compact support even if D_vW grows at infinity. Finite measure and compact continuity imply L² membership.
Corresponding Lean step
hP,hPc,hdφ,hdW,hdc,hq,hqc,hPL,hqL; pv and qv are toLp representatives
4. Establish genuine integrability and representative independence
Products of L² functions are integrable by Cauchy–Schwarz. The pointwise representatives supplied by toLp agree almost everywhere with the explicit tests; transfer both product integrabilities across these equalities. Changing u or G on a null set does not change the conclusion.
Corresponding Lean step
hPe,hqe; L2.integrable_inner and Integrable.congr
5. Prove the pairing identity on the exact core
Take any pair in D.graph. Its exact graph characterization provides a smooth compact representative f and its genuine gradient. Transfer through the almost-everywhere equalities, use D_vf=⟨∇f,v⟩, and apply the normalized identity. This proves the equality on the whole original graph without assuming it.
Corresponding Lean step
hsub uses hgraph, hleft, hright, ht and compact_directional_ibp
6. Pass to the graph closure by continuity
The two L² pairings are continuous functions on the product Hilbert space. Their equality set is closed and contains D.graph, hence contains its topological closure. Closability identifies that closure with D.closure.graph. This retains precisely the D already used in the weak resolvent.
Corresponding Lean step
hclosed,closure_minimal,hmem; hD.graph_closure_eq_closure_graph
7. Return to the readable integral identity
Convert the two Hilbert pairings back to integrals using the same almost-everywhere test representatives. This establishes a weighted weak identity; it does not differentiate u pointwise. Passing to ordinary volume weak derivatives, or invoking elliptic regularity for the resolvent, still requires separate work.
Corresponding Lean step
he; L2.inner_def,integral_congr_ae (hPe G),integral_congr_ae (hqe u)
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · closed_gradient_weighted_ibp
Compact classical weighted IBP plus a closed equality of continuous L² pairings, with explicit representative and integrability transfers.
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 closed_gradient_weighted_ibp (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 →
(∀ (u : Lp ℝ 2 μ) (G : Lp E 2 μ), (u,G) ∈ D.graph ↔
∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
u =ᵐ[μ] f ∧ G =ᵐ[μ] gradient f) →
∀ (u : Lp ℝ 2 μ) (G : Lp E 2 μ), (u,G) ∈ D.closure.graph →
∀ (φ : E → ℝ), ContDiff ℝ 1 φ → HasCompactSupport φ → ∀ v : E,
Integrable (fun x => φ x * inner ℝ (G x) v) μ ∧
Integrable (fun x => u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v)) μ ∧
(∫ x, φ x * inner ℝ (G x) v ∂μ) =
- ∫ x, u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v) ∂μ := by
let μ := (volume : Measure E).tilted (fun x => -W x)
let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
dsimp only
intro D hD hgraph u G hu φ hφ hc v
let P := fun x => φ x • v
let q := fun x => fderiv ℝ φ x v - φ x * fderiv ℝ W x v
have hP : Continuous P := hφ.continuous.smul continuous_const
have hPc : HasCompactSupport P := hc.smul_right
have hdφ : Continuous (fun x => fderiv ℝ φ x v) :=
(hφ.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
have hdW : Continuous (fun x => fderiv ℝ W x v) :=
(hW.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
have hdc : HasCompactSupport (fun x => fderiv ℝ φ x v) := by
refine HasCompactSupport.of_support_subset_isCompact hc.isCompact ?_
intro x hx
by_contra hn
exact hx (by simp [fderiv_of_notMem_tsupport ℝ hn])
have hq : Continuous q := hdφ.sub (hφ.continuous.mul hdW)
have hqc : HasCompactSupport q := hdc.sub hc.mul_right
have hPL : MemLp P 2 μ := hP.memLp_of_hasCompactSupport hPc
have hqL : MemLp q 2 μ := hq.memLp_of_hasCompactSupport hqc
let pv : Lp E 2 μ := hPL.toLp P
let qv : Lp ℝ 2 μ := hqL.toLp q
have hPe (H : Lp E 2 μ) :
(fun x => inner ℝ (H x) (pv x)) =ᵐ[μ] (fun x => φ x * inner ℝ (H x) v) := by
filter_upwards [hPL.coeFn_toLp] with x hx
rw [show pv x = P x from hx]
simp [P, inner_smul_right]
have hqe (a : Lp ℝ 2 μ) :
(fun x => inner ℝ (a x) (qv x)) =ᵐ[μ] (fun x => a x * q x) := by
filter_upwards [hqL.coeFn_toLp] with x hx
rw [show qv x = q x from hx]
simp [mul_comm]
refine ⟨(L2.integrable_inner (𝕜 := ℝ) G pv).congr (hPe G),
(L2.integrable_inner (𝕜 := ℝ) u qv).congr (hqe u), ?_⟩
have ht (g : E → ℝ) : (∫ x, g x ∂μ) =
(∫ x, Real.exp (-W x))⁻¹ * ∫ x, Real.exp (-W x) * g x := by
rw [show μ = (volume : Measure E).tilted (fun x => -W x) from rfl, integral_tilted]
rw [← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with x
change (Real.exp (-W x) / (∫ z, Real.exp (-W z))) • g x = _
simp only [smul_eq_mul, div_eq_mul_inv]
ring
have hclosed : IsClosed {z : Lp ℝ 2 μ × Lp E 2 μ |
inner ℝ z.2 pv = -inner ℝ z.1 qv} :=
isClosed_eq (continuous_snd.inner continuous_const)
(continuous_fst.inner continuous_const).neg
have hsub : (D.graph : Set (Lp ℝ 2 μ × Lp E 2 μ)) ⊆
{z | inner ℝ z.2 pv = -inner ℝ z.1 qv} := by
rintro ⟨a,H⟩ hz
obtain ⟨f,hf,hfc,ha,hH⟩ := (hgraph a H).mp hz
change inner ℝ H pv = -inner ℝ a qv
rw [L2.inner_def, L2.inner_def, integral_congr_ae (hPe H), integral_congr_ae (hqe a)]
have hff := contDiff_infty.mp hf 1
have hleft : (∫ x, φ x * inner ℝ (H x) v ∂μ) =
∫ x, φ x * fderiv ℝ f x v ∂μ := by
apply integral_congr_ae
filter_upwards [hH] with x hx
rw [hx, AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient.fderiv_apply_eq_inner_gradient_of_differentiableAt
(hff.differentiable one_ne_zero x)]
have hright : (∫ x, a x * q x ∂μ) = ∫ x, f x * q x ∂μ :=
integral_congr_ae (ha.mul (Filter.EventuallyEq.refl _ _))
rw [hleft, hright, ht, ht]
have hi := compact_directional_ibp W f φ hW hff hφ hc v
simp_rw [← mul_assoc] at ⊢
rw [hi]
simp only [mul_neg]
congr 1
congr 1
apply integral_congr_ae
filter_upwards [] with x
dsimp [q]
ring
have hmem : (u,G) ∈ D.graph.topologicalClosure := by
rwa [hD.graph_closure_eq_closure_graph]
have he := (closure_minimal hsub hclosed) hmem
change inner ℝ G pv = -inner ℝ u qv at he
rw [L2.inner_def, L2.inner_def, integral_congr_ae (hPe G), integral_congr_ae (hqe u)] at he
exact he
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeakSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source uses a conditional Euclidean Sobolev gradient and its closedness in the Poincare/density route. | Any given closable exact smooth compact gradient graph for normalized exp(-W) volume. | source-implicit | The same operator is supplied by an existing construction; the weak test identity is proved, not assumed. |
| Actual conditional potential comes from a C2 strongly convex V with proved normalization. | C1 W and integrable exp(-W), no curvature bound. | generalization | Only the local product rule and compact tests enter; no curvature-dependent coercivity is claimed. |
| Kolesnikov–Milman background discusses compact weighted manifolds, boundary conditions and spectral properties. | Only a full-space finite-dimensional weighted test identity, including dimension zero. | API-limitation | Domain and conclusion boundary deliberately narrower than a full background regularity/spectral result; this is a prerequisite, not that theorem. |
| Representative choice, compact approximation and integrability are implicit in the analytic route. | L2 equivalence classes, exact graph AE witnesses, both integrabilities, genuinely C1 compact test. | source-implicit | No totalized derivative of an arbitrary L2 representative is used; compact support prevents any global score integrability premise. |
Weighted compact-test identity for the same closed gradient only. Not an unweighted distributional derivative, H2 regularity, a D*D operator core, noncompact Bochner extension, Poincare, score variance, macroscopic coercivity or a complete paper.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- assumptions: The short route paraphrase is elaborated into C¹ regularity, integrable positive Gibbs density, a given closable exact smooth-compact gradient graph, and compact C¹ tests. These are explicit in the publication candidate and reconstruction; they are not silently supplied conclusions. — The declaration explicitly includes hW, hI, D.IsClosable, the universally quantified exact graph equivalence, closure-graph membership, and C¹ compact support of φ. The authored assumptions and blind reconstruction preserve each condition. The private helper establishes classical integration by parts under its stated C¹ hypotheses and compact support of the test.
- conclusion: Both product-integrability claims and almost-everywhere representative transfers are explicit, making the source's meaningful integral identity precise. — The theorem concludes two Integrable propositions together with the signed identity. The proof obtains these using L2.integrable_inner and transfers through hPe and hqe; the final conversion uses L2.inner_def and integral_congr_ae. Lesson steps four and seven accurately describe these operations.
- scopes: The general C¹ full-space theorem is an independently proved prerequisite applicable to the source route under specialization. Acceptance is not an equivalence claim between this theorem and either cited paper result. — The packet's source wording explicitly labels the result a route prerequisite. The module introduction and lesson source scopes exclude unweighted regularity, D*D operator-core claims, Poincaré, macroscopic coercivity and complete-paper claims. The supplied proof establishes only the weighted compact-test identity for D.closure.graph. The inspected primary PBPS Appendix C.1 and Kolesnikov–Milman §2.5 address broader analytic results that this module does not claim to prove.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- Weighted compact-test identity for the same closed gradient only. Not an unweighted distributional derivative, H2 regularity, a D*D operator core, noncompact Bochner extension, Poincare, score variance, macroscopic coercivity or a complete paper.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
- MeasureTheory.integral_tilted
- MeasureTheory.L2.integrable_inner
- MeasureTheory.L2.inner_def
- LinearPMap.IsClosable.graph_closure_eq_closure_graph
- closure_minimal
Mathematical sources
- PBPS Appendix C.1: analytic prerequisite — Weighted compact-test identity for the same closed gradient only. Not an unweighted distributional derivative, H2 regularity, a D*D operator core, noncompact Bochner extension, Poincare, score variance, macroscopic coercivity or a complete paper.
- Kolesnikov–Milman §2.5: weighted Sobolev background — Direct full-space proof, not the compact-manifold spectral theorem.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.