The actual conditional PBPS gradient is densely defined and closable
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient.conditional_gradient_closable · theorem · Teaching coverage
Mathematical statement
For the actual Gibbs-Gaussian augmentation, choose common Markov kernels R,S with R disintegrating the swapped joint law and S_y the reflected pushforward of R_y. For every y, S_y is normalized exp(-W_y) volume, W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), with W_y C2 and finite positive normalizer. On the scalar and vector L2 spaces of this same S_y there exists a partial real-linear gradient D_y with dense domain, IsClosable and closed closure. Its graph consists exactly of pairs represented by f and the genuine gradient f for smooth compact scalar f.
Lean statement · conditional_gradient_closable
One actual pair R,S before all y; for each y, actual density, C2 potential, positive finite normalizer and an operator with exact gradient graph.
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.
theorem conditional_gradient_closable {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 fProof roadmap
- 1Preserve the actual conditional law
Use the already proved ConditionalBochner construction once. Keep its same R,S, swapped disintegration and pointwise reflected pushforward, then fix y. No new abstract measure or surrogate score is substituted.
- 2Supply the genuine weight and regularity
The parent provides S_y as the actual tilt, W_y C2, integrable exp(-W_y) and a positive normalizer. Lower the regularity only to C1 for the shared construction. The finite positive normalizer remains explicitly stated under the same fiber law.
- 3Instantiate the exact gradient graph on that fiber
Rewrite the scalar/vector L2 spaces using the proved equality of measures and apply compact_gradient_closable with W_y. This gives the dense domain and closed extension together with the exact smooth-gradient graph. It is still an analytic prerequisite and supplies neither the generator core nor the conditional PI estimate.
Full assumptions and notation
All objects and hypotheses
- E is finite-dimensional real inner-product Borel, including dimension zero; V is C2.
- Alpha,beta are nonnegative real parameters with explicit 0<alpha≤beta and genuine alpha/beta Hessian quadratic-form bounds. Eta>0 and beta eta≤1 are retained from the parent conditional-kernel interface.
- Mu is volume tilted by -V and J is the law of (X,X+sqrt(eta)Z) under independent Gibbs X and standard Gaussian Z. The constructed R,S are shared before the universal quantifier over y.
- Weight integrability and positive normalization are conclusions inherited from the proved actual conditional law, not new hypotheses. The abstract gradient closure itself requires no curvature restrictions.
Mathematical proof
1. Preserve the actual conditional law
Use the already proved ConditionalBochner construction once. Keep its same R,S, swapped disintegration and pointwise reflected pushforward, then fix y. No new abstract measure or surrogate score is substituted.
Corresponding Lean step
The consumer destructures one conditional_bochner_energy witness and retains hR,hS,hcond,hSR.
2. Supply the genuine weight and regularity
The parent provides S_y as the actual tilt, W_y C2, integrable exp(-W_y) and a positive normalizer. Lower the regularity only to C1 for the shared construction. The finite positive normalizer remains explicitly stated under the same fiber law.
Corresponding Lean step
hSy,hW,hI,hZ are obtained from the same hfiber y; no new integrability assumption is added.
3. Instantiate the exact gradient graph on that fiber
Rewrite the scalar/vector L2 spaces using the proved equality of measures and apply compact_gradient_closable with W_y. This gives the dense domain and closed extension together with the exact smooth-gradient graph. It is still an analytic prerequisite and supplies neither the generator core nor the conditional PI estimate.
Corresponding Lean step
The final application uses the actual hI and hW.of_le; graph membership remains an iff for both directions.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_gradient_closable
Apply the proved conditional law and the genuine weighted-gradient construction; no PI, variance or core conclusion is assumed.
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.
theorem conditional_gradient_closable {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 := by
obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
ConditionalBochner.conditional_bochner_energy hα hαβ hV hH hη hβη
dsimp only
refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
intro y
obtain ⟨hSy,hW,hI,hZ,_⟩ := hfiber y
refine ⟨hSy,hW,hI,hZ,?_⟩
rw [hSy]
exact WeightedGradient.compact_gradient_closable _ (hW.of_le (by norm_num)) hI
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Paper setting: Euclidean d>=1, V C2, 0<alpha<=beta, genuine alpha/beta Hessian bounds, eta>0 and beta eta<=1. | E is finite-dimensional real inner-product Borel, including dimension zero; V is C2. | generalization | Finite-dimensional real inner-product Borel E includes dimension zero. This extends the source positive-dimensional Euclidean setting and is explicitly disclosed. |
| Appendix C.1 conditional Poincare application. | Actual conditional dense closable gradient construction only. | API-limitation | This prerequisite does not prove the source variance estimate, PI, a D*D core or resolvent regularity. |
| Source Hessian and scale assumptions. | Explicit 0<alpha<=beta, V C2, genuine Hessian bounds and beta eta<=1 retained. | same | The conditional parent interface retains these restrictions even though the abstract gradient result has no curvature hypothesis. |
| Actual conditional Gibbs normalization. | One common R,S with disintegration and reflected pushforward; every fiber has actual density, C2 potential, integrable weight and positive normalizer. | source-implicit | The shared exponential integrability premise is supplied by the proved actual conditional law, not introduced as a new paper assumption. |
Dense compact-test gradient operator, exact genuine-gradient graph and closed extension only. No operator core of D*D, dense mean-zero generator range, resolvent regularity, Poincare, noncompact score variance, macro coercivity, process/mixing/error/cost or complete-paper result.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Explicit abstract finite-dimensional and zero-dimensional extension. — Public domain and lesson explicitly allow zero dimension.
- scopes: Authored analytic prerequisite, not the PI assertion in C.1. — Operator core, resolvent regularity and PI remain open; pointwise properties concern the chosen conditional version.
- assumptions: Upper curvature and beta eta<=1 are inherited interface restrictions, absent from abstract gradient construction. — hSy,hW,hI,hZ from same hfiber y; shared hI and hW.of_le are supplied, not assumed anew.
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
- Dense compact-test gradient operator, exact genuine-gradient graph and closed extension only. No operator core of D*D, dense mean-zero generator range, resolvent regularity, Poincare, noncompact score variance, macro coercivity, process/mixing/error/cost or complete-paper result.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochner.conditional_bochner_energyAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradient.compact_gradient_closable
Mathlib API called (external library)
- ContDiff.of_le
Mathematical sources
- Chen, Chewi, Lu and Zhang, PBPS Appendix C.1 — Actual conditional weighted-space analytic prerequisite to PI, not PI or variance.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.