Samplinglib mathematical lesson

Dense closable gradient on the actual Gaussian outer marginal

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalGradient.gaussian_marginal_gradient_closable · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert space with its Borel structure, including rank zero. Let μ be any probability measure on E and η>0. For independent X∼μ and G∼N(0,I), define the actual joint law J of (X,X+√η G) and its second marginal ν=J.snd. There exists one genuine real linear partial gradient operator D₀ from scalar L²(ν) to E-valued L²(ν), with norm-dense domain, closability and a closed graph for its operator closure. For every scalar class u and vector class v in these two actual L² spaces, (u,v) lies in D₀.graph if and only if there exists a globally C∞ compactly supported real function f with u=f ν-almost everywhere and v=∇f ν-almost everywhere. The gradient is the actual inverse-Riesz Fréchet derivative. No finite moment, input density, potential, integrability, normalizer or gradient-domain certificate is supplied. This is authored background for the paper's density/closedness invocation, not its full rough-input B.13 theorem.

\[\rho(y)=C\!\int e^{-\|y-x\|^2/(2\eta)}\,\mu(dx),\quad\int\rho\,dy=1,\quad\operatorname{graph}D_0=\{([f],[\nabla f]):f\in C_c^\infty(E)\},\quad\overline{\operatorname{dom}D_0}=L^2(\nu).\]

Lean statement · gaussian_marginal_gradient_closable

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.

Download module (.lean)

theorem gaussian_marginal_gradient_closable
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] {η : ℝ} (hη : 0 < η) :
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
    let ν := J.snd
    ∃ 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

Exact module and namespace context

Proof roadmap

1Keep the actual independent Gaussian marginal
The augmentation map is measurable. Actual product and map probability give J and ν as probabilities. Mapping the joint law by snd equals the actual add-noise pushforward; no replacement conditional measure is introduced.
2Produce the positive C2 outer density
Invoke the existing Gaussian-convolution producer with only probability μ and η>0. Its exact dimensional prefactor is C=(sqrt(2πη)⁻¹)^dimE, including rank0. It produces ρ>0 and C2 W=-logρ. Continuity of ρ supplies the actual strong-measurability domain.
3Derive L1 before evaluating the real normalizer
Apply the actual measure equality to the whole space. Probability mass1 and the with-density definition yield the nonnegative extended integral1. Continuous positive ρ gives the precise AEStrong/nonnegative prerequisites; finiteness of this extended integral proves actual L1.
4Identify the true normalized Gibbs law
Only after L1 is known, identify the Bochner integral with the nonnegative extended integral and conclude its real value is1. Positivity permits exp(logρ)=ρ. The genuine tilted denominator is therefore1, giving exactly the same ν.
5Join the genuine weighted-gradient graph
Rewrite the whole measure-indexed target using the exact tilted-law equality. Apply the existing weighted-gradient construction with C1 W and internally derived exponential integrability. It supplies the actual compact-gradient graph, dense domain, closability and closed closure on ν. D₀ here is the outer gradient, distinct from the microscopic joint block D in the previous result.
6Exercise the actual paper law and noncentered zero-dimensional class
The actual PBPS macroscopic-energy producer supplies probability for its unchanged μ/J/ν under the original curvature and step hypotheses. Smooth compact f and its true gradient produce actual scalar/vector L2 representatives belonging to the same D₀.graph. In rank0, f=1 is compact and its class has real mean1, paired with the zero gradient. No centering premise is present.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real Hilbert space E with Borel measurable structure; rank zero is an explicit authored extension.
Any actual probability measure μ on E and any positive real η. No moment or input-density assumption.
The exact graph uses globally smooth compactly supported real representatives; these are existential in the graph equivalence, not a supplied closed-gradient or regularity certificate.

Mathematical proof

1. Keep the actual independent Gaussian marginal

The augmentation map is measurable. Actual product and map probability give J and ν as probabilities. Mapping the joint law by snd equals the actual add-noise pushforward; no replacement conditional measure is introduced.

\[J=\bigl((x,g)\mapsto(x,x+\sqrt\eta g)\bigr)_\#(\mu\otimes\gamma),\qquad\nu=J_Y=\bigl((x,g)\mapsto x+\sqrt\eta g\bigr)_\#(\mu\otimes\gamma).\]

Corresponding Lean step

hpair; Measure.isProbabilityMeasure_map; hmap; Measure.map_map

2. Produce the positive C2 outer density

Invoke the existing Gaussian-convolution producer with only probability μ and η>0. Its exact dimensional prefactor is C=(sqrt(2πη)⁻¹)^dimE, including rank0. It produces ρ>0 and C2 W=-logρ. Continuity of ρ supplies the actual strong-measurability domain.

\[C=(\sqrt{2\pi\eta}^{\,-1})^{\dim E},\quad Z(y)=\int e^{-\|y-x\|^2/(2\eta)}\mu(dx),\quad\rho=CZ>0,\quad W=-\log\rho\in C^2,\quad\nu=\rho\,dy.\]

Corresponding Lean step

GaussianConvolutionRegularity.gaussian_convolution_potential_c2; hνdensity; hpos; hZ; hW; hρ

3. Derive L1 before evaluating the real normalizer

Apply the actual measure equality to the whole space. Probability mass1 and the with-density definition yield the nonnegative extended integral1. Continuous positive ρ gives the precise AEStrong/nonnegative prerequisites; finiteness of this extended integral proves actual L1.

\[1=\nu(E)=\int\rho\,dy\ \text{as a nonnegative extended integral},\qquad\int^{\!-}\operatorname{ofReal}(\rho)\,dy=1<\infty\Rightarrow\rho\in L^1(dy).\]

Corresponding Lean step

hmass; withDensity_apply; Measure.restrict_univ; hnn; lintegral_ofReal_ne_top_iff_integrable; hI

4. Identify the true normalized Gibbs law

Only after L1 is known, identify the Bochner integral with the nonnegative extended integral and conclude its real value is1. Positivity permits exp(logρ)=ρ. The genuine tilted denominator is therefore1, giving exactly the same ν.

\[\int\rho\,dy=1,\qquad e^{-W}=\rho,\qquad dy.\operatorname{tilted}(-W)=\frac{e^{-W}}{\int e^{-W}dy}\,dy=\rho\,dy=\nu.\]

Corresponding Lean step

ofReal_integral_eq_lintegral_ofReal; ENNReal.ofReal_eq_one; hnorm; hexp; Real.exp_log; hWI; Measure.tilted; htilt

5. Join the genuine weighted-gradient graph

Rewrite the whole measure-indexed target using the exact tilted-law equality. Apply the existing weighted-gradient construction with C1 W and internally derived exponential integrability. It supplies the actual compact-gradient graph, dense domain, closability and closed closure on ν. D₀ here is the outer gradient, distinct from the microscopic joint block D in the previous result.

\[\operatorname{graph}D_0=\{([f]_\nu,[\nabla f]_\nu):f\in C_c^\infty(E)\},\quad\overline{\operatorname{dom}D_0}=L^2(\nu),\quad\overline{\operatorname{graph}D_0}=\operatorname{graph}\overline D_0\ \text{is single-valued and closed}.\]

Corresponding Lean step

rw [← htilt]; WeightedGradient.compact_gradient_closable; hW.of_le; hWI

6. Exercise the actual paper law and noncentered zero-dimensional class

The actual PBPS macroscopic-energy producer supplies probability for its unchanged μ/J/ν under the original curvature and step hypotheses. Smooth compact f and its true gradient produce actual scalar/vector L2 representatives belonging to the same D₀.graph. In rank0, f=1 is compact and its class has real mean1, paired with the zero gradient. No centering premise is present.

\[\mu=dy.\operatorname{tilted}(-V),\quad\nu=J_Y:\ ([f],[\nabla f])\in\operatorname{graph}D_0;\qquad\dim E=0,\ f=1:\ \int u\,d\nu=1,\ (u,0)\in\operatorname{graph}D_0.\]

Corresponding Lean step

Tests.ProximalBPSGaussianMarginalGradient.actual_pbps_compact_gradient_graph; rank_zero_noncentered_graph; actual50 probability output; canonical continuous_gradient_of_contDiff_one (Test only)

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · gaussian_marginal_gradient_closable

Keep the actual independent Gaussian marginal; Produce the positive C2 outer density; Derive L1 before evaluating the real normalizer; Identify the true normalized Gibbs law; Join the genuine weighted-gradient graph; Exercise the actual paper law and noncentered zero-dimensional class

Download module (.lean)

theorem gaussian_marginal_gradient_closable
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] {η : ℝ} (hη : 0 < η) :
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
    let ν := J.snd
    ∃ 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
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
  let ν := J.snd
  change ∃ 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
  let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
  let Z := fun y : E => ∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ
  let ρ := fun y : E => C*Z y
  let W := fun y : E => -Real.log (ρ y)
  have hpair : Measurable (fun p : E × E =>
      (p.1, p.1 + Real.sqrt η • p.2)) := by fun_prop
  let : IsProbabilityMeasure J := Measure.isProbabilityMeasure_map hpair.aemeasurable
  let : IsProbabilityMeasure ν := Measure.isProbabilityMeasure_map measurable_snd.aemeasurable
  have hmap : ν = (μ.prod (stdGaussian E)).map
      (fun p : E × E => p.1 + Real.sqrt η • p.2) :=
    Measure.map_map measurable_snd hpair
  obtain ⟨hdensity,hpos,hZ,hW⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity.gaussian_convolution_potential_c2 μ hη
  have hνdensity : ν = (volume : Measure E).withDensity
      (fun y => ENNReal.ofReal (ρ y)) := hmap.trans hdensity
  have hρ : Continuous ρ := continuous_const.mul hZ.continuous
  have hnn : 0 ≤ᵐ[(volume : Measure E)] ρ :=
    Filter.Eventually.of_forall fun y => (hpos y).le
  have hmass : (∫⁻ y, ENNReal.ofReal (ρ y) ∂(volume : Measure E)) = 1 := by
    have hm := congrArg (fun m : Measure E => m Set.univ) hνdensity
    rw [withDensity_apply _ MeasurableSet.univ] at hm
    simpa only [measure_univ,Measure.restrict_univ] using hm.symm
  have hI : Integrable ρ (volume : Measure E) :=
    (lintegral_ofReal_ne_top_iff_integrable hρ.aestronglyMeasurable hnn).mp
      (by rw [hmass]; exact ENNReal.one_ne_top)
  have hnorm : (∫ y, ρ y ∂(volume : Measure E)) = 1 :=
    ENNReal.ofReal_eq_one.mp ((ofReal_integral_eq_lintegral_ofReal hI hnn).trans hmass)
  have hexp (y : E) : Real.exp (-W y) = ρ y := by
    dsimp only [W]
    rw [neg_neg,Real.exp_log (hpos y)]
  have hWI : Integrable (fun y => Real.exp (-W y)) (volume : Measure E) := by
    simpa only [hexp] using hI
  have htilt : (volume : Measure E).tilted (fun y => -W y) = ν := by
    rw [Measure.tilted]
    simp_rw [hexp]
    rw [hnorm]
    simpa only [div_one] using hνdensity.symm
  rw [← htilt]
  exact WeightedGradient.compact_gradient_closable W
    (hW.of_le (by norm_num)) hWI

end
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalGradient

Exact module and namespace context

Scope and omitted-condition boundaries

Actual Gaussian outer marginal nu=J.snd admits a dense genuine smooth-compact gradient graph, is closable, and has closed closure. No literal Tf graph membership, arbitrary rough L2 smoothing estimate, Gamma/half-turn/main/errors/cost or actual-input composition is proved. Focused3893 passed; complete independent mathematics/source/exact-commit/shared integration remain pending.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Measure.isProbabilityMeasure_map
MeasureTheory.Measure.map_map
MeasureTheory.withDensity_apply
MeasureTheory.Measure.restrict_univ
MeasureTheory.lintegral_ofReal_ne_top_iff_integrable
MeasureTheory.ofReal_integral_eq_lintegral_ofReal
ENNReal.ofReal_eq_one
Real.exp_log
MeasureTheory.Measure.tilted
ContDiff.of_le

Mathematical sources

Fixed PBPS arXiv2609.06905v1 Appendix C.1 density/closedness sentence physical4573-4576, required toward B.13 physical3779-3786. Authored generic Gaussian-marginal background integration; not full B.13. — Actual Gaussian outer marginal nu=J.snd admits a dense genuine smooth-compact gradient graph, is closable, and has closed closure. No literal Tf graph membership, arbitrary rough L2 smoothing estimate, Gamma/half-turn/main/errors/cost or actual-input composition is proved. Focused3893 passed; complete independent mathematics/source/exact-commit/shared integration remain pending.

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