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

WeightedGradientDistribution: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. From the closed Gibbs gradient to ordinary weak derivatives
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.

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 := 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

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

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