Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Closed gradients satisfy weighted compact-test integration by parts

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeak.closed_gradient_weighted_ibp · theorem · Teaching coverage

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.

\[\int \varphi\langle G,v\rangle\,d\mu=-\int u\,(D_v\varphi-\varphi D_vW)\,d\mu.\]

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.

\[D_vF=e^{-W}(D_v\varphi-\varphi D_vW),\qquad \int F D_vf\,dx=-\int f D_vF\,dx.\]
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.

\[Z=\int e^{-W}\,dx,\qquad d\mu=Z^{-1}e^{-W}dx,\qquad \int\varphi D_vf\,d\mu=-\int f(D_v\varphi-\varphi D_vW)\,d\mu.\]
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.

\[P(x)=\varphi(x)v,\qquad q(x)=D_v\varphi(x)-\varphi(x)D_vW(x),\qquad P\in L^2(\mu;E),\quad q\in L^2(\mu).\]
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.

\[\int|\langle G,P\rangle|\,d\mu\le\|G\|_2\|P\|_2,\qquad\int|uq|\,d\mu\le\|u\|_2\|q\|_2.\]
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.

\[(a,H)\in\operatorname{graph}D\ \Longrightarrow\ \langle H,P\rangle_{L^2}=-\langle a,q\rangle_{L^2}.\]
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.

\[\overline{\operatorname{graph}D}\subseteq\{(a,H):\langle H,P\rangle=-\langle a,q\rangle\},\qquad\overline{\operatorname{graph}D}=\operatorname{graph}(\overline D).\]
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.

\[\int \varphi\langle G,v\rangle\,d\mu=-\int u\,(D_v\varphi-\varphi D_vW)\,d\mu.\]
Corresponding Lean step

he; L2.inner_def,integral_congr_ae (hPe G),integral_congr_ae (hqe u)

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) ∂μ

Exact module and namespace context

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.WeightedGradientWeak

Exact module and namespace context

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.

Source and reuse

ASTIS 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

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