The actual conditional PBPS gradient is densely defined and closable
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient.conditional_gradient_closable · theorem · Teaching coverage
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.
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 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 fLean 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.ConditionalGradientScope 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.
Source and reuse
ASTIS 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.