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

ASTIS-authored source-specific compact-branch domain integration for Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. Original two-sided curvature/C2/capped step/signed smooth compact setting is retained. Finite Hilbert/rank0 is an explicit extension; closure of the canonical compact-gradient core is explicit authored background, without claiming equivalence to a separate weak H1 or full rough B.13.

Complete source statement (Samplinglib restatement)

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.

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

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

\[\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

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Original C2 V, two-sided positive α≤β curvature and positive η with βη≤1; signed smooth compact observer.	All original hypotheses are theorem binders and observer quantifiers; finite Hilbert/rank0 is explicit.	same	No hidden higher derivative, centering, compact mean, density, Lp or closure certificate premise.
C.1 uses density and closedness to pass from compact tests toward rough H1 in B.13.	Uniform actual smooth compact gradient graph and canonical mean/gradient pair in its closed extension.	unresolved	Source omitted analytic domain details are filled for this compact mean only; identification with separately defined weak H1 and all-L2 limit remain obligations.
C.1 literal reflected normalized source density and C.2 actual mean-gradient integrability.	Exact μ=volume.tilted(-V), SAME J=law(X,X+sqrt(eta)G), actual ν=J.snd, literal source S_y=volume.tilted(-V((y+u)/2)-norm(y-u)^2/(8eta)), Tf(y)=actual source S_y mean. Uniform G chosen BEFORE all smoothcompact f; produced hTf/hGrad toLp are canonical classes in the SAME ν and true G.closure.graph. G is distinct from50 lower-right blockD.	same	SAME actual laws and entire EVERY-y function equality precede differentiation; true uniform core is distinct from macroscopic lower-right blockD.
Full rough B.13, Gamma, sampling main results and query costs.	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.	unresolved	No whole-paper, dynamics or unbounded expected-cost result is exported.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

domains: Printed source Euclidean presentation; Finite real Hilbert/Borel and rank0 explicit attributed extension — Native independent source54 D54-authored-space: explicit-elaboration; formalization-artifact-risk
scopes: Source names gradient closedness/H1 and omits analytic details; Actual uniform full compact-gradient core and closed extension; classicalC1+trueLp pair supplied internally — Native independent source54 D54-closed-core: explicit-elaboration; source-implicit
conclusion: Full source B13 has allroughL2 and quantitative/Gamma identities; Advertisedcompact domain prerequisite only; fullrough conclusion remains explicitly residual — Native independent source54 D54-selected-scope: explicit-elaboration; source-implicit

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

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.

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

Complete source statement (Samplinglib restatement)

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

Read the formalized proofs

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

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

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

2. Choose the genuine gradient core uniformly

3. Use C1 of the whole literal source mean

4. Admit the actual pair through the C1 domain theorem

5. Connect the real macroscopic representative and preserve constants

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?