Actual PBPS conditional C1 weak-resolvent tests

Samplinglib explicit full-space analytic prerequisite to Chen, Chewi, Lu and Zhang Appendix C.1; not a quoted numbered theorem or full Lemma C.1/Poincare result.

Complete source statement (Samplinglib restatement)

For actual C2 V with 0<alpha<=beta global Hessian bounds, eta>0 and beta eta<=1, construct the actual Gibbs-Gaussian augmentation and common Markov conditional kernels R,S, with disintegration R and S_y=(R_y)#(x->2x-y). S_y is the true normalized reflected Gibbs law for W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), with C2 regularity and positive integrable weight. For every y, retain one dense closable exact compact-smooth gradient D, fixed before epsilon/input, and derive every positive-epsilon L2 forcing weak solution, ordinary weak gradient/local integrability and all C1 compact weighted volume test equations. No measurable solution selection in y is claimed.

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

Actual PBPS conditional C1 weak-resolvent tests

AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalC1Resolvent.conditional_c1_resolvent · theorem · Teaching coverage

Read this first

Mathematical statement

For actual C2 V with 0<alpha≤beta global Hessian bounds, eta>0 and beta eta≤1, construct the actual Gibbs-Gaussian augmentation and common Markov conditional kernels R,S, with disintegration R and S_y=(R_y)#(x→2x-y). S_y is the true normalized reflected Gibbs law for W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), with C2 regularity and positive integrable weight. For every y, retain one dense closable exact compact-smooth gradient D, fixed before epsilon/input, and derive every positive-epsilon L2 forcing weak solution, ordinary weak gradient/local integrability and all C1 compact weighted volume test equations. No measurable solution selection in y is claimed.

\[S_y=(2x-y)_\#R_y=Z_y^{-1}e^{-W_y(u)}du,\quad W_y(u)=V((y+u)/2)+\|u-y\|^2/(8\eta);\quad\varepsilon\!\int e^{-W_y}u\psi+\!\int e^{-W_y}\langle\overline D_yu,\nabla\psi\rangle=\!\int e^{-W_y}f\psi.\]

Lean statement · conditional_c1_resolvent

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 conditional_c1_resolvent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : NNReal} {η : ℝ}
    (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 := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
    let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
      ∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
        ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
        0 < (∫ u, Real.exp (-W y u)) ∧
        ∃ D : Lp ℝ 2 (S y) →ₗ.[ℝ] Lp E 2 (S y),
          Dense (D.domain : Set (Lp ℝ 2 (S y))) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
          (∀ (u : Lp ℝ 2 (S y)) (v : Lp E 2 (S y)), (u,v) ∈ D.graph ↔
            ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
              u =ᵐ[S y] f ∧ v =ᵐ[S y] gradient f) ∧
      ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 (S y),
      ∃ u : D.closure.domain,
        (∀ v : D.closure.domain,
          ε * ⟪(u : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
            ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) ∧
        LocallyIntegrable (fun x => (u : Lp ℝ 2 (S y)) x) ∧
        LocallyIntegrable (fun x => D.closure u x) ∧
        (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (D.closure u x) v) ∧
          Integrable (fun x => (u : Lp ℝ 2 (S y)) x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (D.closure u x) v) =
            - ∫ x, (u : Lp ℝ 2 (S y)) x * fderiv ℝ ψ x v) ∧
        ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ →
          Integrable (fun x => Real.exp (-W y x) * ((u : Lp ℝ 2 (S y)) x * ψ x)) ∧
          Integrable (fun x => Real.exp (-W y x) * inner ℝ (D.closure u x) (gradient ψ x)) ∧
          Integrable (fun x => Real.exp (-W y x) * (f x * ψ x)) ∧
          ε * (∫ x, Real.exp (-W y x) * ((u : Lp ℝ 2 (S y)) x * ψ x)) +
            (∫ x, Real.exp (-W y x) * inner ℝ (D.closure u x) (gradient ψ x)) =
            ∫ x, Real.exp (-W y x) * (f x * ψ x)

Exact module and namespace context

Proof roadmap

1Use the actual common conditional kernels
The existing conditional gradient producer constructs true Gibbs-Gaussian augmentation, Markov R/S, original disintegration and reflection pushforward. Every selected reflected fiber is an actual normalized density, not an abstract replacement.
2Keep the reflected source potential and partition
Retain W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), its true C2 regularity, integrable exp(-W_y) and positive partition. Its Hessian is one quarter of the unreflected shifted Hessian; no same-law/operator identification is used.
3Fix the original gradient before epsilon and input
For each observation use the original dense closable exact compact smooth graph D supplied by that actual fiber. Its closure is closed, and the operator is fixed before arbitrary epsilon and forcing.
4Apply the real C1 weighted weak equation
Reduce the true C2 potential to C1 and rewrite only the exact measure equality S_y=volume.tilted(-W_y). Apply the canonical C1 resolvent to that same original D, not another convenient operator.
5Carry every weak-gradient and integrability conclusion
The ordinary volume weak-gradient identities, local integrability and all three weighted L1 products remain explicit in the actual fiber result. Tests instantiate a true nonquadratic potential and a compact norm^(3/2) observable with only C1 regularity.
6Retain fiberwise and full-paper boundaries
No measurable y-selection of weak solutions is constructed, and no H2, generator-core/global Bochner, Poincare or macro H1 theorem follows just from the test upgrade. Both paper main results and actual-input cost composition remain unfinished.

Full assumptions and notation

All objects and hypotheses

E has the same full-space finite-dimensional real Hilbert/Borel structure, including dimension zero. V is C2 with true all-point/all-direction alpha I≤Hess V≤beta I, alpha,beta NNReal, 0<alpha≤beta, eta>0 and beta eta≤1.
The original Gibbs law, genuine independent Gaussian augmentation, selected R,S kernels, reflected W_y, finite positive partition and fixed original gradient D per fiber are derived by the existing actual conditional producer. Neither normalization nor a convenient replacement operator is supplied.
The potential is reflected, with quarter Hessian scaling. The unreflected SPHMC RGO potential/law is different. Existence is fiberwise for every y; no joint measurable resolvent selection, unbounded cost transfer or macroscopic H1/Poincare theorem is asserted.

Mathematical proof

1. Use the actual common conditional kernels

The existing conditional gradient producer constructs true Gibbs-Gaussian augmentation, Markov R/S, original disintegration and reflection pushforward. Every selected reflected fiber is an actual normalized density, not an abstract replacement.

\[S_y=(2x-y)_\#R_y,\quad S_y=Z_y^{-1}e^{-W_y}du.\]

Corresponding Lean step

ConditionalGradient.conditional_gradient_closable

2. Keep the reflected source potential and partition

Retain W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), its true C2 regularity, integrable exp(-W_y) and positive partition. Its Hessian is one quarter of the unreflected shifted Hessian; no same-law/operator identification is used.

\[W_y(u)=V((y+u)/2)+\|u-y\|^2/(8\eta),\quad D^2W_y=\tfrac14(D^2V+\eta^{-1}I).\]

Corresponding Lean step

hSy,hW,hI,hZ; explicit Wy

3. Fix the original gradient before epsilon and input

For each observation use the original dense closable exact compact smooth graph D supplied by that actual fiber. Its closure is closed, and the operator is fixed before arbitrary epsilon and forcing.

\[\forall y\ \exists D_y\ \forall\varepsilon>0\ \forall f\in L^2(S_y).\]

Corresponding Lean step

hDense,hClose,hClosed,hgraph

4. Apply the real C1 weighted weak equation

Reduce the true C2 potential to C1 and rewrite only the exact measure equality S_y=volume.tilted(-W_y). Apply the canonical C1 resolvent to that same original D, not another convenient operator.

\[\varepsilon\int e^{-W_y}u\psi+\int e^{-W_y}\langle\overline D_yu,\nabla\psi\rangle=\int e^{-W_y}f\psi.\]

Corresponding Lean step

WeightedResolventC1.weak_resolvent_c1; rw [hSy]

5. Carry every weak-gradient and integrability conclusion

The ordinary volume weak-gradient identities, local integrability and all three weighted L1 products remain explicit in the actual fiber result. Tests instantiate a true nonquadratic potential and a compact norm^(3/2) observable with only C1 regularity.

\[\psi\in C_c^1,\quad u,\overline D_yu\in L^1_{loc}(du),\quad\text{three weighted products in }L^1.\]

Corresponding Lean step

Tests.CompactC1GradientDomain.actual_nonconstant_source

6. Retain fiberwise and full-paper boundaries

No measurable y-selection of weak solutions is constructed, and no H2, generator-core/global Bochner, Poincare or macro H1 theorem follows just from the test upgrade. Both paper main results and actual-input cost composition remain unfinished.

\[\text{fiberwise weak tests}\ne\text{measurable joint selection or conditional Poincare}.\]

Corresponding Lean step

conditional_c1_resolvent

Lean verification

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

Lean proof · conditional_c1_resolvent

Use the actual common conditional kernels; Keep the reflected source potential and partition; Fix the original gradient before epsilon and input; Apply the real C1 weighted weak equation; Carry every weak-gradient and integrability conclusion; Retain fiberwise and full-paper boundaries

Download module (.lean)

theorem conditional_c1_resolvent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : NNReal} {η : ℝ}
    (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 := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
    let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
      ∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
        ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
        0 < (∫ u, Real.exp (-W y u)) ∧
        ∃ D : Lp ℝ 2 (S y) →ₗ.[ℝ] Lp E 2 (S y),
          Dense (D.domain : Set (Lp ℝ 2 (S y))) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
          (∀ (u : Lp ℝ 2 (S y)) (v : Lp E 2 (S y)), (u,v) ∈ D.graph ↔
            ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
              u =ᵐ[S y] f ∧ v =ᵐ[S y] gradient f) ∧
      ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 (S y),
      ∃ u : D.closure.domain,
        (∀ v : D.closure.domain,
          ε * ⟪(u : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
            ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) ∧
        LocallyIntegrable (fun x => (u : Lp ℝ 2 (S y)) x) ∧
        LocallyIntegrable (fun x => D.closure u x) ∧
        (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (D.closure u x) v) ∧
          Integrable (fun x => (u : Lp ℝ 2 (S y)) x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (D.closure u x) v) =
            - ∫ x, (u : Lp ℝ 2 (S y)) x * fderiv ℝ ψ x v) ∧
        ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ →
          Integrable (fun x => Real.exp (-W y x) * ((u : Lp ℝ 2 (S y)) x * ψ x)) ∧
          Integrable (fun x => Real.exp (-W y x) * inner ℝ (D.closure u x) (gradient ψ x)) ∧
          Integrable (fun x => Real.exp (-W y x) * (f x * ψ x)) ∧
          ε * (∫ x, Real.exp (-W y x) * ((u : Lp ℝ 2 (S y)) x * ψ x)) +
            (∫ x, Real.exp (-W y x) * inner ℝ (D.closure u x) (gradient ψ x)) =
            ∫ x, Real.exp (-W y x) * (f x * ψ x) := by
  obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient.conditional_gradient_closable hα hαβ hV hH hη hβη
  dsimp only
  refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
  intro y
  obtain ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph⟩ := hfiber y
  refine ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph,?_⟩
  intro ε hε f
  let Wy : E → ℝ := fun u => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
  have hW1 : ContDiff ℝ 1 Wy := hW.of_le (by norm_num)
  have hwc := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventC1.weak_resolvent_c1 Wy hW1 hI
  dsimp only at hwc
  rw [← hSy] at hwc
  exact hwc D hClose hgraph ε hε f

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalC1Resolvent

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source Euclidean C2 positively curved Gibbs conditional weighted-H1 route.	E has the same full-space finite-dimensional real Hilbert/Borel structure, including dimension zero. V is C2 with true all-point/all-direction alpha I<=Hess V<=beta I, alpha,beta NNReal, 0<alpha<=beta, eta>0 and beta eta<=1. The original Gibbs law, genuine independent Gaussian augmentation, selected R,S kernels, reflected W_y, finite positive partition and fixed original gradient D per fiber are derived by the existing actual conditional producer. Neither normalization nor a convenient replacement operator is supplied. The potential is reflected, with quarter Hessian scaling. The unreflected SPHMC RGO potential/law is different. Existence is fiberwise for every y; no joint measurable resolvent selection, unbounded cost transfer or macroscopic H1/Poincare theorem is asserted.	source-implicit	Generic leaf uses finite measure or C1 normalized potential, with disclosed finite Hilbert/Borel/zero-dimension extension; actual source consumer retains exact source curvature/eta cap and true reflected law.
Source compact smooth calculations and extension to weighted H1 omit approximation/domain details.	For actual C2 V with 0<alpha<=beta global Hessian bounds, eta>0 and beta eta<=1, construct the actual Gibbs-Gaussian augmentation and common Markov conditional kernels R,S, with disintegration R and S_y=(R_y)#(x->2x-y). S_y is the true normalized reflected Gibbs law for W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), with C2 regularity and positive integrable weight. For every y, retain one dense closable exact compact-smooth gradient D, fixed before epsilon/input, and derive every positive-epsilon L2 forcing weak solution, ordinary weak gradient/local integrability and all C1 compact weighted volume test equations. No measurable solution selection in y is claimed.	source-implicit	Actually prove joint graph-domain approximation and C1 compact tests. Finite normalized laws permit bounded dominated convergence without an assumed uniform/common-support approximation. No higher/noncompact domain certificate supplied.
Appendix C.1 pursues conditional Poincare/macroscopic H1 extension.	Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete main/composition. TV never transfers unbounded expected cost.	unresolved	Only this analytic domain/test delta; global elliptic/core/Bochner/Poincare and complete papers remain independent.

Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete main/composition. TV never transfers unbounded expected cost.

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

Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete main/composition. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ContDiff.of_le

Mathematical sources

PBPS Appendix C.1 omitted analytic domain prerequisite — Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete main/composition. TV never transfers unbounded expected cost.

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

Actual PBPS conditional C1 weak-resolvent tests

Complete source statement (Samplinglib restatement)

Actual PBPS conditional C1 weak-resolvent tests

Read the formalized proofs

Actual PBPS conditional C1 weak-resolvent tests

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Use the actual common conditional kernels

2. Keep the reflected source potential and partition

3. Fix the original gradient before epsilon and input

4. Apply the real C1 weighted weak equation

5. Carry every weak-gradient and integrability conclusion

6. Retain fiberwise and full-paper boundaries

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?