Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Dense closable gradient on the actual Gaussian outer marginal

ASTIS-authored full-space background making the source C.1 density/closedness invocation explicit. The printed paper has its Gibbs setting; this generic probability-input/finite-Hilbert/rank0 result and the internal normalization bridge are authored elaborations. Actual PBPS consumer preserves original curvature/step conditions. Source B.13 and main/cost conclusions remain open.

PBPS arXiv2609.06905v1; pinned Mathlib; Lean4.33.0 · 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. · faithful paraphrase

Complete source statement (Samplinglib restatement)

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.

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

Dense closable gradient on the actual Gaussian outer marginal

\[\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).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

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

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.

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

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

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

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

  4. 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 ν.

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

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

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

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
C.1 density/closedness invocation for the actual outer Gibbs-Gaussian marginal.Any probability μ and η>0 on finite real Hilbert/Borel E, including rank0; one genuine dense closable compact gradient on exactly ν=J.snd.generalizationAuthored background extension explicitly attributed; actual paper consumer retains all original global C2 Hessian/positive curvature/step-cap premises.
Gradient on smooth compact functions with density and closedness for approximation.Exact scalar/vector L2 graph with genuine gradient representatives, dense domain, closability and closed operator closure; real normalizer and integrability derived internally.sameMakes the omitted analytic domain construction explicit with existing compiled Gaussian/weighted-gradient parents.
B.13 every-L2 reflected-mean H1 and energy estimate, Gamma and full sampler/cost results.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.unresolvedNo literal Tf closure membership, rough allL2 energy, positive root, convergence/error/expected queries or actual-input composition is asserted.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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

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

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual Gaussian outer-marginal dense closable compact gradient and closed closure
  • TODO — not closed by these contributions Literal Tf closure membership/full rough H1/Gamma/main/cost/composition remain open