Samplinglib mathematical lesson

The actual PBPS source mean belongs to the closed-gradient domain

AutoSamplingTheory.ExampleCases.ProximalBPS.SourceMeanGradientDomain.literal_source_mean_in_closed_gradient · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert space with its Borel structure and canonical volume, including rank zero. Let V:E→ℝ be C2, 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), ν=J.snd, and S_y=volume.tilted(u↦−V((y+u)/2)−‖y−u‖²/(8η)). Then ν is a probability and there is one dense closable compact-gradient operator G:L²(ν;ℝ)⇀L²(ν;E), chosen before f, with closed closure and exact graph consisting of the pairs represented by φ and ∇φ for φ∈C∞_c(E). For every signed f∈C∞_c(E), let Tf(y)=∫f(u)S_y(du). Both Tf and ∇Tf belong to L²(ν), and their canonical classes satisfy ([Tf],[∇Tf])∈graph(closure G). No compact support of Tf or caller normalization, regularity, Lp or closure certificate is assumed. This is attributed analytic integration of the compact source branch, not the full rough B.13 statement.

\[\nu=\operatorname{law}(X+\sqrt\eta Z),\quad Tf(y)=\int f(u)S_y(du),\qquad \exists G\ \forall f\in C_c^\infty(E):\quad Tf,\nabla Tf\in L^2(\nu),\quad ([Tf],[\nabla Tf])\in\operatorname{graph}(\overline G).\]

Lean statement · literal_source_mean_in_closed_gradient

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 literal_source_mean_in_closed_gradient
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    let S := fun y : E => (volume : Measure E).tilted
      (fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
    IsProbabilityMeasure ν ∧
      ∃ G : Lp ℝ 2 ν →ₗ.[ℝ] Lp E 2 ν,
        Dense (G.domain : Set (Lp ℝ 2 ν)) ∧ G.IsClosable ∧ G.closure.IsClosed ∧
        (∀ (u : Lp ℝ 2 ν) (v : Lp E 2 ν), (u,v) ∈ G.graph ↔
          ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
            u =ᵐ[ν] φ ∧ v =ᵐ[ν] gradient φ) ∧
        ∀ f : E → ℝ, ContDiff ℝ ∞ f → HasCompactSupport f →
          let Tf := fun y : E => ∫ u, f u ∂S y
          ∃ hTf : MemLp Tf 2 ν, ∃ hGrad : MemLp (gradient Tf) 2 ν,
            (hTf.toLp Tf,hGrad.toLp (gradient Tf)) ∈ G.closure.graph

Exact module and namespace context

Proof roadmap

1Keep the actual augmentation and produce the two L2 witnesses
The existing macroscopic-energy producer uses the original curvature and step regime on the genuine Gibbs law. It gives probability of μ and the actual outer ν, a reflected Markov kernel S₀ for the same augmentation, the EVERY-y literal identity S₀(y)=S_y, and square-integrability of its smooth-observer mean and true gradient. Rewrite the whole mean function, not an AE conditional version, to obtain the two witnesses on the literal source mean.
2Choose the genuine gradient core uniformly
The actual outer Gaussian law feeds the existing Gaussian-marginal-gradient theorem. It constructs one partial operator with dense domain, closability and closed closure. Its full graph is precisely the canonical pairs represented by smooth compact φ and its actual gradient. The operator is chosen before the observer f and is distinct from the lower-right reflection block D.
3Use C1 of the whole literal source mean
Smooth f is C1. The source-specific reflected-Gibbs-mean theorem applies to the literal source law at every y; its probability, normalization and dominated differentiation ingredients remain genuine internal background. This gives C1 of exactly Tf. Equality of AE conditional versions alone would not provide this pointwise regularity.
4Admit the actual pair through the C1 domain theorem
The outer law is a finite probability. The public C1 domain theorem applies to this SAME ν and the exact G graph, using actual C1, function-L2 and gradient-L2 evidence. Its existing smooth cutoff/approximation proof puts the canonical pair in the closed graph without assuming Tf compact. This closes the domain prerequisite; a separate all-L2 limit and source weak-H1 identification are still needed.
5Connect the real macroscopic representative and preserve constants
The genuine Test uses the actual reflection U and conditional projection P on L²(J). For each original smooth compact f it joins g=f∘snd, Pg=g and Ag=(Tf)∘snd for A=PUP to the new canonical gradient pair. The zero-dimensional Test consumes the actual source-volume mean1 and gradient0 and transports canonical Lp objects using MemLp.toLp_congr. Direct dependent rewrites were retired and their compiler negatives retained.

Full assumptions and notation

All objects and hypotheses

Finite real Hilbert/Borel E and canonical volume; rank zero is an explicit background extension of the source Euclidean presentation.
V is C2; α,β are nonnegative, α>0, α≤β and both global directional Hessian bounds hold. η>0 and βη≤1.
Every observer is signed smooth compact f; neither centering nor compact support of its mean Tf is required.
All laws and the mean are the literal displayed ones. G is constructed uniformly before all f; its entire smooth compact AE graph is characterized. Probability, Lp, C1 and graph membership are produced internally.

Mathematical proof

1. Keep the actual augmentation and produce the two L2 witnesses

The existing macroscopic-energy producer uses the original curvature and step regime on the genuine Gibbs law. It gives probability of μ and the actual outer ν, a reflected Markov kernel S₀ for the same augmentation, the EVERY-y literal identity S₀(y)=S_y, and square-integrability of its smooth-observer mean and true gradient. Rewrite the whole mean function, not an AE conditional version, to obtain the two witnesses on the literal source mean.

\[\mu=dx.\operatorname{tilted}(-V),\quad J=\operatorname{law}(X,X+\sqrt\eta Z),\quad\nu=J_2;\qquad S_0(y)=S_y\ (\forall y),\quad Tf,\nabla Tf\in L^2(\nu).\]

Corresponding Lean step

MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks; hμ; hν; hSd; henergy; hsame; hTf; hGrad

2. Choose the genuine gradient core uniformly

The actual outer Gaussian law feeds the existing Gaussian-marginal-gradient theorem. It constructs one partial operator with dense domain, closability and closed closure. Its full graph is precisely the canonical pairs represented by smooth compact φ and its actual gradient. The operator is chosen before the observer f and is distinct from the lower-right reflection block D.

\[\operatorname{graph}(G)=\{([\varphi],[\nabla\varphi]):\varphi\in C_c^\infty(E)\},\quad\overline{\operatorname{dom}G}=L^2(\nu),\quad G\text{ closable},\quad\operatorname{graph}(\overline G)\text{ closed}.\]

Corresponding Lean step

GaussianMarginalGradient.gaussian_marginal_gradient_closable μ hη; G; hDense; hClosable; hClosed; hGraph

3. Use C1 of the whole literal source mean

Smooth f is C1. The source-specific reflected-Gibbs-mean theorem applies to the literal source law at every y; its probability, normalization and dominated differentiation ingredients remain genuine internal background. This gives C1 of exactly Tf. Equality of AE conditional versions alone would not provide this pointwise regularity.

\[Tf(y)=\int f(u)S_y(du)\quad(\forall y),\qquad Tf\in C^1(E).\]

Corresponding Lean step

hf1; LiteralReflectedMean.reflected_gibbs_mean_c1; hC1

4. Admit the actual pair through the C1 domain theorem

The outer law is a finite probability. The public C1 domain theorem applies to this SAME ν and the exact G graph, using actual C1, function-L2 and gradient-L2 evidence. Its existing smooth cutoff/approximation proof puts the canonical pair in the closed graph without assuming Tf compact. This closes the domain prerequisite; a separate all-L2 limit and source weak-H1 identification are still needed.

\[\nu(E)=1,\quad Tf\in C^1,\quad Tf,\nabla Tf\in L^2(\nu)\quad\Longrightarrow\quad([Tf],[\nabla Tf])\in\operatorname{graph}(\overline G).\]

Corresponding Lean step

WeightedC1GradientDomain.c1_in_closed_gradient ν G hClosable hGraph hC1 hTf hGrad

5. Connect the real macroscopic representative and preserve constants

The genuine Test uses the actual reflection U and conditional projection P on L²(J). For each original smooth compact f it joins g=f∘snd, Pg=g and Ag=(Tf)∘snd for A=PUP to the new canonical gradient pair. The zero-dimensional Test consumes the actual source-volume mean1 and gradient0 and transports canonical Lp objects using MemLp.toLp_congr. Direct dependent rewrites were retired and their compiler negatives retained.

\[A=PUP,\quad g=f\circ\mathrm{snd},\quad Pg=g,\quad Ag=Tf\circ\mathrm{snd};\qquad d=0,\ f=1:\quad Tf\equiv1,\quad\nabla Tf=0,\quad([1],[0])\in\operatorname{graph}(\overline G).\]

Corresponding Lean step

Tests.ProximalBPSSourceMeanGradientDomain.actual_macroscopic_mean_closed_gradient; rank_zero_noncentered_source_mean_graph; MemLp.toLp_congr (Test only)

Lean verification

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

Lean proof · literal_source_mean_in_closed_gradient

Keep the actual augmentation and produce the two L2 witnesses; Choose the genuine gradient core uniformly; Use C1 of the whole literal source mean; Admit the actual pair through the C1 domain theorem; Connect the real macroscopic representative and preserve constants

Download module (.lean)

theorem literal_source_mean_in_closed_gradient
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    let S := fun y : E => (volume : Measure E).tilted
      (fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
    IsProbabilityMeasure ν ∧
      ∃ G : Lp ℝ 2 ν →ₗ.[ℝ] Lp E 2 ν,
        Dense (G.domain : Set (Lp ℝ 2 ν)) ∧ G.IsClosable ∧ G.closure.IsClosed ∧
        (∀ (u : Lp ℝ 2 ν) (v : Lp E 2 ν), (u,v) ∈ G.graph ↔
          ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
            u =ᵐ[ν] φ ∧ v =ᵐ[ν] gradient φ) ∧
        ∀ f : E → ℝ, ContDiff ℝ ∞ f → HasCompactSupport f →
          let Tf := fun y : E => ∫ u, f u ∂S y
          ∃ hTf : MemLp Tf 2 ν, ∃ hGrad : MemLp (gradient Tf) 2 ν,
            (hTf.toLp Tf,hGrad.toLp (gradient Tf)) ∈ G.closure.graph := by
  classical
  dsimp only
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
  let ν := J.snd
  let S := fun y : E => (volume : Measure E).tilted
    (fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
  obtain ⟨hμ,hJ,hν,R,S₀,hR,hS₀,hcond,hSR,hSd,hΛcond,hfst,
    U,hU,hUi,hUs,hBB,hBD,hblock,henergy⟩ :=
    MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks hα hαβ hV hH hη hβη
  letI : IsProbabilityMeasure μ := hμ
  letI : IsProbabilityMeasure ν := hν
  obtain ⟨G,hDense,hClosable,hClosed,hGraph⟩ :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalGradient.gaussian_marginal_gradient_closable μ hη
  refine ⟨hν,G,hDense,hClosable,hClosed,hGraph,?_⟩
  intro f hf hfc
  let Tf := fun y : E => ∫ u, f u ∂S y
  have hsame : (fun y : E => ∫ u, f u ∂S₀ y) = Tf := by
    funext y
    exact congrArg (fun m : Measure E => ∫ u, f u ∂m) (hSd y)
  obtain ⟨_,_,hTf₀,hGrad₀,_,_⟩ := henergy f hf hfc
  have hTf : MemLp Tf 2 ν := by simpa only [hsame] using hTf₀
  have hGrad : MemLp (gradient Tf) 2 ν := by simpa only [hsame] using hGrad₀
  have hf1 : ContDiff ℝ 1 f := hf.of_le (by simp)
  obtain ⟨_,hC1⟩ := LiteralReflectedMean.reflected_gibbs_mean_c1
    hα hV (fun x v => (hH x v).1) hη hf1 hfc
  change ContDiff ℝ 1 Tf at hC1
  refine ⟨hTf,hGrad,?_⟩
  exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.c1_in_closed_gradient ν G hClosable hGraph hC1 hTf hGrad

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.SourceMeanGradientDomain

Exact module and namespace context

Scope and omitted-condition boundaries

The literal source mean of each signed smooth compact observer has a canonical function/gradient L2 pair in the closure of one uniform genuine dense compact-gradient core on the SAME actual outer Gaussian law. Original C2 potential, two-sided Hessian and capped positive step are retained; finite Hilbert/rank0 is an explicit extension. The mean itself need not be compact. Full rough all-L2 B13, identification with separately defined weak H1, Gamma, dynamics, main results, errors, unbounded expected costs and actual-input composition remain separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MemLp.toLp
MemLp.toLp_congr
gradient_fun_const'
contDiff_infty
Filter.Eventually.of_forall

Mathematical sources

Pinned PBPS2609.06905v1 C.1 smoothcompact reduction physical4573–4576, literal S density4581–4587 and actual mean4597–4604, C.2 integrated actual gradient4654–4664 toward B.13 physical3777–3786. This is source-specific analytic integration of the compact branch, not printed full rough B.13. — The literal source mean of each signed smooth compact observer has a canonical function/gradient L2 pair in the closure of one uniform genuine dense compact-gradient core on the SAME actual outer Gaussian law. Original C2 potential, two-sided Hessian and capped positive step are retained; finite Hilbert/rank0 is an explicit extension. The mean itself need not be compact. Full rough all-L2 B13, identification with separately defined weak H1, Gamma, dynamics, main results, errors, unbounded expected costs and actual-input composition remain separate.

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