A dense closable gradient for a genuine Gibbs measure
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradient.compact_gradient_closable · theorem · Teaching coverage
Statement
Let E be a finite-dimensional real inner-product Borel space, W:E->R be C1, and exp(-W) be integrable against canonical volume. Set mu=Z^{-1}exp(-W)dx. There is a partial real-linear operator D from scalar L2(mu) to vector L2(mu) whose domain is dense, whose graph is closable, and whose closure is closed. For any scalar L2 class u and vector L2 class v, (u,v) belongs to its graph exactly when there exists a smooth compactly supported scalar f with u=f and v=gradient f almost everywhere. This equivalence fixes the actual differential operator and its exact initial domain.
All objects and hypotheses
- E is finite-dimensional real inner-product with its Borel sigma algebra and canonical volume; dimension zero is included.
- W is C1 and the actual positive function exp(-W) is volume-integrable. No curvature, Poincare, gradient coercivity or operator-closure assumption is made.
- Mu is the actual normalized exponential tilt. Positive exponential and nonzero canonical volume give a finite positive normalizer and hence a probability; the zero-tilt fallback is not used.
- Lp objects are equivalence classes modulo mu-almost-everywhere equality. D is a partial linear map; closable means the topological closure of its graph is still the graph of a partial linear map, not that D is bounded or everywhere defined.
- Background weighted H1 completion in Kolesnikov-Milman section2.5 is on compact manifolds. This directly proved full-space Euclidean construction is a selected analytic prerequisite, not that source spectral theorem.
Mathematical proof
1. Establish weighted directional integration by parts
Take F=exp(-W)g with g C1 compact and f C1. F, its directional derivative, and all three products needed by Haar IBP are continuous and compactly supported. Apply the actual volume theorem and expand the genuine derivative of F. The drift term has the minus sign inside the derivative of exp(-W).
Corresponding Lean step
The local weighted_directional proof derives all three Integrable premises; it never applies a Haar theorem to mu.
2. Construct the weighted negative divergence test
For a C1 compact vector field P, project onto each orthonormal basis vector and sum the directional formula. This constructs a continuous compact scalar q, namely minus divergence P plus gradient W dot P. The public theorem does not separately export a divergence formula; this is a proved internal construction.
Corresponding Lean step
raw_vector_ibp proves the finite sum and integrability; tilted_vector_ibp transfers the exact identity and proves q in L2(mu).
3. Build the exact smooth gradient graph
Pairs of scalar and vector L2 classes belong to the graph when they have representatives f and gradient f for a smooth compact f. Genuine derivative addition and scalar multiplication prove this set is a linear submodule. This defines a relation before any representative-dependent operator is selected.
Corresponding Lean step
The local smoothGradientGraph submodule proves zero, addition and scalar closure using Lp coeFn almost-everywhere identities and genuine fderiv rules.
4. Extend the integration-by-parts pairing to the graph closure
For fixed smooth compact P and its scalar q, the equality between the two L2 inner products is a closed condition on a scalar/vector pair. Every graph pair satisfies it by the proved weighted IBP and representative identities, so every pair in the topological closure also satisfies it.
Corresponding Lean step
closure_unique uses continuous L2 inner products and closure_minimal; no closedness of the derivative is assumed.
5. Use vector-valued smooth density to prove single-valuedness
If (0,v) belongs to the closed graph relation, the pairing identity makes v orthogonal to every smooth compact vector test. The pinned Mathlib theorem makes these tests dense in vector L2 for every measure finite on compacts, including this probability. A continuous zero pairing therefore vanishes on all vector L2; pairing with v gives v=0.
Corresponding Lean step
Lp.dense_hasCompactSupport_contDiff, Dense.induction and inner_self_eq_zero prove the zero-fiber statement. This implies both G and its closure are single-valued.
6. Construct the partial operator and its dense closed extension
Only after single-valuedness is proved does toLinearPMap construct D from G. Its graph is proved equal to G, and the analogous construction from the closed relation proves IsClosable. Scalar smooth density and L2 integrability of each compact continuous gradient prove the initial domain dense. Mathlib then supplies the closed graph of D.closure.
Corresponding Lean step
Submodule.toLinearPMap_graph_eq is used with the proved zero-fiber witnesses; IsClosable.closure_isClosed is applied only after closability is derived.
Lean statement · compact_gradient_closable
Exact graph equivalence, dense domain, IsClosable and closed closure, for the actual normalized Gibbs L2 spaces.
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_gradient_closable (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 μ,
Dense (D.domain : Set (Lp ℝ 2 μ)) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
∀ (u : Lp ℝ 2 μ) (v : Lp E 2 μ), (u,v) ∈ D.graph ↔
∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
u =ᵐ[μ] f ∧ v =ᵐ[μ] gradient fLean proof · compact_gradient_closable
Every helper and the graph submodule are local haves/lets in the public proof; its folded Lean contains the complete argument.
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_gradient_closable (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 μ,
Dense (D.domain : Set (Lp ℝ 2 μ)) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
∀ (u : Lp ℝ 2 μ) (v : Lp E 2 μ), (u,v) ∈ D.graph ↔
∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
u =ᵐ[μ] f ∧ v =ᵐ[μ] gradient f := by
have weighted_directional (W f g : E → ℝ) (hW : ContDiff ℝ 1 W)
(hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g)
(hgc : HasCompactSupport g) (v : E) :
(∫ x, Real.exp (-W x) * g x * fderiv ℝ f x v) =
- ∫ x, Real.exp (-W x) *
(fderiv ℝ g x v - g x * fderiv ℝ W x v) * f x := by
let F := fun x => Real.exp (-W x) * g x
have hF : ContDiff ℝ 1 F := hW.neg.exp.mul hg
have hFc : HasCompactSupport F := hgc.mul_left
have hDF : Continuous (fun x => fderiv ℝ F x v) :=
(hF.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
have hDf : Continuous (fun x => fderiv ℝ f x v) :=
(hf.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
have hDFc : HasCompactSupport (fun x => fderiv ℝ F x v) := by
refine HasCompactSupport.of_support_subset_isCompact hFc.isCompact ?_
intro x hx
by_contra hn
exact hx (by simp [fderiv_of_notMem_tsupport ℝ hn])
have h1 : Integrable (fun x => fderiv ℝ F x v * f x) :=
(hDF.mul hf.continuous).integrable_of_hasCompactSupport hDFc.mul_right
have h2 : Integrable (fun x => F x * fderiv ℝ f x v) :=
(hF.continuous.mul hDf).integrable_of_hasCompactSupport hFc.mul_right
have h3 : Integrable (fun x => F x * f x) :=
(hF.continuous.mul hf.continuous).integrable_of_hasCompactSupport hFc.mul_right
have hi := integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable h1 h2 h3
(fun x _ => hF.differentiable one_ne_zero x)
(fun x _ => hf.differentiable one_ne_zero x)
change (∫ x, F x * fderiv ℝ f x v) = _
rw [hi]
congr 1
apply integral_congr_ae
filter_upwards [] with x
have hd := ((hW.differentiable one_ne_zero x).hasFDerivAt.neg.exp).mul
(hg.differentiable one_ne_zero x).hasFDerivAt
have he : fderiv ℝ F x v = Real.exp (-W x) *
(fderiv ℝ g x v - g x * fderiv ℝ W x v) := by
rw [show fderiv ℝ F x = _ from hd.fderiv]
simp only [add_apply, smul_apply, neg_apply, smul_eq_mul, Pi.neg_apply]
ring
rw [he]
have gradient_cont (f : E → ℝ) (hf : ContDiff ℝ 1 f) : Continuous (gradient f) := by
exact (toDual ℝ E).symm.continuous.comp (hf.fderiv_right (m := 0) (by norm_num)).continuous
have gradient_compact (f : E → ℝ) (hc : HasCompactSupport f) :
HasCompactSupport (gradient f) := by
refine HasCompactSupport.of_support_subset_isCompact hc.isCompact ?_
intro x hx
by_contra hn
exact hx (by simp [gradient, fderiv_of_notMem_tsupport ℝ hn])
have raw_vector_ibp (W : E → ℝ) (hW : ContDiff ℝ 1 W)
(P : E → E) (hP : ContDiff ℝ 1 P) (hPc : HasCompactSupport P) :
∃ q : E → ℝ, Continuous q ∧ HasCompactSupport q ∧
∀ (f : E → ℝ), ContDiff ℝ 1 f →
(∫ x, Real.exp (-W x) * inner ℝ (gradient f x) (P x)) =
∫ x, Real.exp (-W x) * f x * q x := by
let b := stdOrthonormalBasis ℝ E
let g := fun i x => inner ℝ (P x) (b i)
have hg (i) : ContDiff ℝ 1 (g i) := hP.inner ℝ contDiff_const
have hgc (i) : HasCompactSupport (g i) := by
refine HasCompactSupport.of_support_subset_isCompact hPc.isCompact ?_
intro x hx
by_contra hn
exact hx (by simp [g, image_eq_zero_of_notMem_tsupport hn])
have hdg (i) : Continuous (fun x => fderiv ℝ (g i) x (b i)) :=
((hg i).fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
have hdgc (i) : HasCompactSupport (fun x => fderiv ℝ (g i) x (b i)) := by
refine HasCompactSupport.of_support_subset_isCompact (hgc i).isCompact ?_
intro x hx
by_contra hn
exact hx (by simp [fderiv_of_notMem_tsupport ℝ hn])
have hdW (i) : Continuous (fun x => fderiv ℝ W x (b i)) :=
(hW.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const
let Q := fun i x => -(fderiv ℝ (g i) x (b i) - g i x * fderiv ℝ W x (b i))
have hQ (i) : Continuous (Q i) := ((hdg i).sub ((hg i).continuous.mul (hdW i))).neg
have hQc (i) : HasCompactSupport (Q i) := ((hdgc i).sub (hgc i).mul_right).neg
let q := fun x => ∑ i, Q i x
refine ⟨q,continuous_finsetSum _ (fun i _ => hQ i),?_,?_⟩
· have hfun : q = ∑ i, Q i := by funext x; simp [q]
rw [hfun]
exact HasCompactSupport.finset_sum (s := Finset.univ) (f := Q) fun i _ => hQc i
intro f hf
have hA (i) : Integrable (fun x => Real.exp (-W x) * g i x * fderiv ℝ f x (b i)) := by
apply (((hW.neg.exp).continuous.mul (hg i).continuous).mul
((hf.fderiv_right (m := 0) (by norm_num)).continuous.clm_apply continuous_const)).integrable_of_hasCompactSupport
exact (hgc i).mul_left.mul_right
have hB (i) : Integrable (fun x => Real.exp (-W x) * f x * Q i x) :=
(((hW.neg.exp).continuous.mul hf.continuous).mul (hQ i)).integrable_of_hasCompactSupport (hQc i).mul_left
have hpoint (x : E) : inner ℝ (gradient f x) (P x) =
∑ i, g i x * fderiv ℝ f x (b i) := by
rw [← b.sum_inner_mul_inner (gradient f x) (P x)]
apply Finset.sum_congr rfl
intro i _
rw [AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient.fderiv_apply_eq_inner_gradient_of_differentiableAt (hf.differentiable one_ne_zero x)]
simp only [g, real_inner_comm (b i) (P x), mul_comm]
simp_rw [hpoint, Finset.mul_sum]
rw [integral_finsetSum _ (fun i _ => by simpa [mul_assoc] using hA i)]
change _ = ∫ x, Real.exp (-W x) * f x * ∑ i, Q i x
simp_rw [Finset.mul_sum]
rw [integral_finsetSum _ (fun i _ => hB i)]
apply Finset.sum_congr rfl
intro i _
rw [show (∫ x, Real.exp (-W x) * (g i x * fderiv ℝ f x (b i))) =
∫ x, Real.exp (-W x) * g i x * fderiv ℝ f x (b i) by congr 1; funext x; ring]
rw [weighted_directional W f (g i) hW hf (hg i) (hgc i) (b i), ← integral_neg]
apply integral_congr_ae
filter_upwards [] with x
dsimp only [Q]
ring
have tilted_vector_ibp (W : E → ℝ) (hW : ContDiff ℝ 1 W)
(hI : Integrable (fun x => Real.exp (-W x)))
(P : E → E) (hP : ContDiff ℝ 1 P) (hPc : HasCompactSupport P) :
let μ := (volume : Measure E).tilted (fun x => -W x)
∃ q : E → ℝ, Continuous q ∧ HasCompactSupport q ∧ MemLp q 2 μ ∧
∀ (f : E → ℝ), ContDiff ℝ 1 f →
(∫ x, inner ℝ (gradient f x) (P x) ∂μ) = ∫ x, f x * q x ∂μ := by
let μ := (volume : Measure E).tilted (fun x => -W x)
let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
obtain ⟨q,hq,hqc,hi⟩ := raw_vector_ibp W hW P hP hPc
refine ⟨q,hq,hqc,hq.memLp_of_hasCompactSupport hqc,?_⟩
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 =
(∫ z, Real.exp (-W z))⁻¹ * (Real.exp (-W x) * g x)
simp only [smul_eq_mul, div_eq_mul_inv]
ring
intro f hf
rw [ht,ht,hi f hf]
congr 1
apply integral_congr_ae
filter_upwards [] with x
ring
let smoothGradientGraph (μ : Measure E) : Submodule ℝ (Lp ℝ 2 μ × Lp E 2 μ) :=
{
carrier := {u | ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
u.1 =ᵐ[μ] f ∧ u.2 =ᵐ[μ] gradient f}
zero_mem' := by
refine ⟨0,contDiff_const,HasCompactSupport.zero,?_,?_⟩
· exact Lp.coeFn_zero _ _ _
· have hz : gradient (0 : E → ℝ) = (0 : E → E) := by
funext x
exact gradient_fun_const x (0 : ℝ)
change (0 : Lp E 2 μ) =ᵐ[μ] gradient (0 : E → ℝ)
rw [hz]
exact Lp.coeFn_zero E 2 μ
add_mem' := by
rintro u v ⟨f,hf,hfc,hfu,hfg⟩ ⟨g,hg,hgc,hgu,hgg⟩
refine ⟨f+g,hf.add hg,hfc.add hgc,?_,?_⟩
· exact (Lp.coeFn_add u.1 v.1).trans (hfu.add hgu)
have he : gradient (f+g) = gradient f + gradient g := by
funext x
simp only [gradient, fderiv_add (hf.differentiable (by simp) x)
(hg.differentiable (by simp) x), map_add, Pi.add_apply]
rw [he]
exact (Lp.coeFn_add u.2 v.2).trans (hfg.add hgg)
smul_mem' := by
rintro a u ⟨f,hf,hfc,hfu,hfg⟩
refine ⟨a • f,contDiff_const.smul hf,hfc.smul_left,?_,?_⟩
· exact (Lp.coeFn_smul a u.1).trans (hfu.const_smul a)
have he : gradient (a • f) = a • gradient f := by
funext x
simp only [gradient, fderiv_const_smul (hf.differentiable (by simp) x),
map_smul, Pi.smul_apply]
rw [he]
exact (Lp.coeFn_smul a u.2).trans (hfg.const_smul a)
}
have closure_unique (W : E → ℝ) (hW : ContDiff ℝ 1 W)
(hI : Integrable (fun x => Real.exp (-W x))) :
let μ := (volume : Measure E).tilted (fun x => -W x)
∀ u ∈ (smoothGradientGraph μ).topologicalClosure, u.1 = 0 → u.2 = 0 := by
let μ := (volume : Measure E).tilted (fun x => -W x)
let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
dsimp only
intro u hu huz
have hd : Dense {v : Lp E 2 μ | ∃ P : E → E,
v =ᵐ[μ] P ∧ HasCompactSupport P ∧ ContDiff ℝ ∞ P} :=
Lp.dense_hasCompactSupport_contDiff (by norm_num)
have horth : ∀ v ∈ {v : Lp E 2 μ | ∃ P : E → E,
v =ᵐ[μ] P ∧ HasCompactSupport P ∧ ContDiff ℝ ∞ P}, inner ℝ u.2 v = 0 := by
rintro v ⟨P,hv,hPc,hP⟩
obtain ⟨q,hq,hqc,hqL,hqi⟩ := tilted_vector_ibp W hW hI P (contDiff_infty.mp hP 1) hPc
let qv : Lp ℝ 2 μ := hqL.toLp q
have hc : IsClosed {z : Lp ℝ 2 μ × Lp E 2 μ |
inner ℝ z.2 v = inner ℝ z.1 qv} :=
isClosed_eq (continuous_snd.inner continuous_const) (continuous_fst.inner continuous_const)
have hs : (smoothGradientGraph μ : Set (Lp ℝ 2 μ × Lp E 2 μ)) ⊆
{z | inner ℝ z.2 v = inner ℝ z.1 qv} := by
rintro z ⟨f,hf,hfc,hfz,hfg⟩
change inner ℝ z.2 v = inner ℝ z.1 qv
calc
inner ℝ z.2 v = ∫ x, inner ℝ (gradient f x) (P x) ∂μ := by
rw [L2.inner_def]
apply integral_congr_ae
filter_upwards [hfg,hv] with x hx hy
rw [hx,hy]
_ = ∫ x, f x * q x ∂μ := hqi f (contDiff_infty.mp hf 1)
_ = inner ℝ z.1 qv := by
rw [L2.inner_def]
apply integral_congr_ae
filter_upwards [hfz,hqL.coeFn_toLp] with x hx hy
rw [hx,show qv x = q x from hy]
simp [mul_comm]
have he := (closure_minimal hs hc) hu
change inner ℝ u.2 v = inner ℝ u.1 qv at he
simpa [huz] using he
have hall : ∀ v : Lp E 2 μ, inner ℝ u.2 v = 0 :=
hd.induction horth (isClosed_eq (continuous_const.inner continuous_id) continuous_const)
exact inner_self_eq_zero.mp (hall u.2)
let μ := (volume : Measure E).tilted (fun x => -W x)
let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
let G := smoothGradientGraph μ
have hu : ∀ z ∈ G.topologicalClosure, z.1 = 0 → z.2 = 0 := closure_unique W hW hI
let D := G.toLinearPMap
have hgraph : D.graph = G :=
G.toLinearPMap_graph_eq (fun z hz hzero => hu z (subset_closure hz) hzero)
have hc : D.IsClosable := by
refine ⟨G.topologicalClosure.toLinearPMap,?_⟩
rw [hgraph]
exact (G.topologicalClosure.toLinearPMap_graph_eq hu).symm
have hd : Dense {u : Lp ℝ 2 μ | ∃ f : E → ℝ,
u =ᵐ[μ] f ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f} :=
Lp.dense_hasCompactSupport_contDiff (by norm_num)
have hD : Dense (D.domain : Set (Lp ℝ 2 μ)) := by
apply hd.mono
rintro u ⟨f,huf,hfc,hf⟩
have hgf : MemLp (gradient f) 2 μ :=
(gradient_cont f (contDiff_infty.mp hf 1)).memLp_of_hasCompactSupport (gradient_compact f hfc)
change u ∈ G.map (LinearMap.fst ℝ (Lp ℝ 2 μ) (Lp E 2 μ))
exact ⟨(u,hgf.toLp (gradient f)),⟨f,hf,hfc,huf,hgf.coeFn_toLp⟩,rfl⟩
refine ⟨D,hD,hc,hc.closure_isClosed,?_⟩
intro u v
rw [hgraph]
rfl
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientScope and omitted-condition boundaries
- Dense compact-test gradient operator, exact genuine-gradient graph and closed extension only. No operator core of D*D, dense mean-zero generator range, resolvent regularity, Poincare, noncompact score variance, macro coercivity, process/mixing/error/cost or complete-paper result.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
- MeasureTheory.integral_tilted
- MeasureTheory.Lp.dense_hasCompactSupport_contDiff
- Dense.induction
- Submodule.toLinearPMap_graph_eq
- LinearPMap.IsClosable.closure_isClosed
Mathematical sources
- Kolesnikov and Milman, section2.5 weighted Sobolev completion — Direct Euclidean full-space analytic prerequisite; compact manifold spectral conclusions are outside this result.
- Chen, Chewi, Lu and Zhang, PBPS Appendix C.1 — Weighted-space construction needed by the conditional Poincare route; does not prove PI.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.