ASTIS mathematical exposition

From the closed Gibbs gradient to ordinary weak derivatives

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientDistribution.closed_gradient_distributional · theorem · Teaching coverage

Statement

The scalar representative u and vector representative G are locally integrable for ordinary Euclidean volume. For every ψ and v as above, both ψ⟨G,v⟩ and uD_vψ are volume-integrable, and their integrals have opposite signs. Thus G is the ordinary distributional gradient of u in this test sense; the converse graph-domain characterization is not claimed.

\[u,G\in L^1_{\mathrm{loc}}(dx),\qquad\int\psi\langle G,v\rangle\,dx=-\int uD_v\psi\,dx.\]

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.
Fix (u,G) in the graph of this same D.closure. Tests ψ are arbitrary C1 compact scalar functions, and v is any constant vector. The L2 coercions select measurable representatives; no differentiability, global volume integrability or tail bound for these representatives is assumed.

Mathematical proof

1. Start with integrability for the Gibbs law

For either scalar or vector representative h, finite μ makes L² membership imply L¹ membership. The actual tilted-measure integrability equivalence transfers this to integrability of e^(−W)h for volume. Positivity and finiteness of normalization follow from the assumed integrable exponential density.

\[h\in L^2(\mu)\Longrightarrow h\in L^1(\mu)\Longleftrightarrow e^{-W}h\in L^1(dx).\]

Corresponding Lean step

private lp_locallyIntegrable_volume: MemLp.integrable, Lp.memLp, integrable_tilted_iff

2. Remove the weight locally

Multiplication by a continuous scalar preserves local integrability. Apply this to e^W and the locally integrable e^(−W)h, then cancel exponentials. Doing this for both u and G establishes their local volume integrability without asserting global volume integrability.

\[h=e^W(e^{-W}h)\in L^1_{\mathrm{loc}}(dx).\]

Corresponding Lean step

LocallyIntegrable.continuous_smul (Real.continuous_exp.comp hW); smul_smul, Real.exp_add

3. Choose the inverse-weighted test

Given compact C1 ψ, set φ=e^Wψ. Continuity at infinity is irrelevant: its support stays inside the compact support of ψ, and φ is genuinely C1. Apply the existing weighted identity to the same D,u,G; no operator is replaced.

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

Corresponding Lean step

hφ,hφc; WeightedGradientWeak.closed_gradient_weighted_ibp

4. Use the genuine first-order product rule

Differentiate e^Wψ using the C1 hypotheses. Subtract φD_vW and cancel its two drift contributions. No classical derivative of u is used.

\[D_v(e^W\psi)=e^W\psi D_vW+e^WD_v\psi,\qquad D_v\varphi-\varphi D_vW=e^WD_v\psi.\]

Corresponding Lean step

hq; HasFDerivAt.exp.mul, hd.fderiv, ring

5. Transfer both test-product integrabilities

The parent proves both weighted products integrable under μ. Apply integrable_tilted_iff to each separately; multiply by e^(−W) and cancel e^(−W)e^W=1. These are actual volume-integrability proofs, not an appeal to the convention for undefined integrals.

\[e^{-W}\varphi\langle G,v\rangle=\psi\langle G,v\rangle,\qquad e^{-W}u(D_v\varphi-\varphi D_vW)=uD_v\psi.\]

Corresponding Lean step

hcancel,hl,hr; hli,hri from integrable_tilted_iff

6. Cancel the positive normalization

The tilted integral is Z⁻¹ times its density-weighted volume integral. Substitute the two pointwise cancellations into the parent identity and cancel Z⁻¹, which is nonzero. Together with local integrability this is the ordinary weak derivative identity, in one direction only.

\[Z^{-1}\int\psi\langle G,v\rangle\,dx=-Z^{-1}\int uD_v\psi\,dx,\qquad Z=\int e^{-W}dx>0.\]

Corresponding Lean step

ht, integral_tilted; mul_left_cancel₀ (inv_ne_zero (integral_exp_pos hI).ne')

Lean statement · closed_gradient_distributional

All same-operator graph assumptions, local-volume and product-integrability conclusions are explicit 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_distributional (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 →
        LocallyIntegrable (fun x => u x) ∧ LocallyIntegrable (fun x => G x) ∧
        ∀ (ψ : E → ℝ), ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (G x) v) ∧
          Integrable (fun x => u x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (G x) v) = - ∫ x, u x * fderiv ℝ ψ x v

Exact module and namespace context

Lean proof · closed_gradient_distributional

Invert the positive density locally; insert exp(W)ψ in the weighted identity; cancel genuine derivative terms and positive normalization.

theorem closed_gradient_distributional (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 →
        LocallyIntegrable (fun x => u x) ∧ LocallyIntegrable (fun x => G x) ∧
        ∀ (ψ : E → ℝ), ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (G x) v) ∧
          Integrable (fun x => u x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (G x) v) = - ∫ x, u x * fderiv ℝ ψ x v := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph u G hu
  refine ⟨lp_locallyIntegrable_volume W hW.continuous hI u,
    lp_locallyIntegrable_volume W hW.continuous hI G, ?_⟩
  intro ψ hψ hc v
  let φ := fun x => Real.exp (W x) * ψ x
  have hφ : ContDiff ℝ 1 φ := hW.exp.mul hψ
  have hφc : HasCompactSupport φ := hc.mul_left
  have hq (x : E) : fderiv ℝ φ x v - φ x * fderiv ℝ W x v =
      Real.exp (W x) * fderiv ℝ ψ x v := by
    have hd := ((hW.differentiable one_ne_zero x).hasFDerivAt.exp).mul
      (hψ.differentiable one_ne_zero x).hasFDerivAt
    rw [show fderiv ℝ φ x = _ from hd.fderiv]
    simp only [add_apply, smul_apply, smul_eq_mul]
    dsimp [φ]
    ring
  have hcancel (x : E) : Real.exp (-W x) * Real.exp (W x) = 1 := by
    rw [← Real.exp_add]
    simp
  have hl (x : E) : Real.exp (-W x) * (φ x * inner ℝ (G x) v) =
      ψ x * inner ℝ (G x) v := by
    dsimp only [φ]
    rw [← mul_assoc, ← mul_assoc, hcancel, one_mul]
  have hr (x : E) : Real.exp (-W x) *
      (u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v)) = u x * fderiv ℝ ψ x v := by
    rw [hq]
    calc
      _ = (Real.exp (-W x) * Real.exp (W x)) * (u x * fderiv ℝ ψ x v) := by ring
      _ = _ := by rw [hcancel, one_mul]
  obtain ⟨hleft,hright,he⟩ := WeightedGradientWeak.closed_gradient_weighted_ibp
    W hW hI D hD hgraph u G hu φ hφ hφc v
  have hli := (integrable_tilted_iff hI _).mp hleft
  have hri := (integrable_tilted_iff hI _).mp hright
  simp only [smul_eq_mul, hl, hr] at hli hri
  refine ⟨hli,hri,?_⟩
  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
  change (∫ x, φ x * inner ℝ (G x) v ∂μ) =
    -∫ x, u x * (fderiv ℝ φ x v - φ x * fderiv ℝ W x v) ∂μ at he
  rw [ht, ht] at he
  simp only [hl, hr, ← mul_neg] at he
  exact mul_left_cancel₀ (inv_ne_zero (integral_exp_pos hI).ne') he

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientDistribution

Exact module and namespace context

Scope and omitted-condition boundaries

Ordinary weak derivative direction only: no converse domain characterization, H2, resolvent PDE adapter, D*D operator core, Poincare or complete paper.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeak.closed_gradient_weighted_ibp

Mathlib API called (external library)

MeasureTheory.MemLp.integrable
MeasureTheory.integrable_tilted_iff
MeasureTheory.LocallyIntegrable.continuous_smul
MeasureTheory.integral_tilted
MeasureTheory.integral_exp_pos
HasFDerivAt.exp
HasFDerivAt.mul

Mathematical sources

PBPS Appendix C.1: analytic prerequisite — Ordinary weak derivative direction only: no converse domain characterization, H2, resolvent PDE adapter, D*D operator core, Poincare or complete paper.
Kolesnikov–Milman §2.5: weighted Sobolev background — Direct full-space proof, not the compact-manifold spectral theorem.

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