Actual PBPS conditional closed-gradient zero implies AE constant
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientKernel.conditional_gradient_zero_ae_constant · theorem · Teaching coverage
Mathematical statement
Construct actual common J/R/S and for each y SAME original dense/closable/exact compact-gradient D_y before ALL closure-domain elements u. Every such u with D_y.closure u=0 is S_y-AE ONE real constant. Actual laws, source hypotheses and partitions remain; no joint measurable selector or full kernel/Poincare result.
Lean statement · conditional_gradient_zero_ae_constant
Construct actual common J/R/S and for each y SAME original dense/closable/exact compact-gradient D_y before ALL closure-domain elements u. Every such u with D_y.closure u=0 is S_y-AE ONE real constant. Actual laws, source hypotheses and partitions remain; no joint measurable selector or full kernel/Poincare result.
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_zero_ae_constant
{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) ∧
∀ u : D.closure.domain, D.closure u = 0 →
∃ c : ℝ, (u : Lp ℝ 2 (S y)) =ᵐ[S y] (fun _ => c)Proof roadmap
- 1Produce the true common conditional law and SAME original gradient
Use the accepted ConditionalGradient producer to construct common Markov/disintegrating R/S, reflected law and actual normalized C2 W_y with positive integrable partition. For every y the original dense closable exact D_y is fixed before ALL closure-domain u; no new operator replaces it.
- 2Apply the shared one-way kernel implication to this actual law
The source C2 W_y gives the needed C1 regularity and genuine partition integrability. Substitute the actual S_y equality in the shared theorem and supply the SAME closable exact graph, retaining original density/closedness facts. No curvature/spectral-gap/final kernel certificate is supplied to the shared leaf.
- 3Exercise a true nonquadratic conditional model and expose residuals
The focused Test proves actual curvature[1/2,1] of V(x)=3x^2/8+sin(x)/8 and fixes eta1/2. It constructs actual J/R/S/positive partitions/SAME original D and exercises the ALL-domain one-way implication. Constant-domain converse, full kernel equality, centered scaled residual/epsilon0/range/Poincare/BL and both main/composition remain separate.
Full assumptions and notation
All objects and hypotheses
- Full finite real Hilbert/Borel E including0; V C2 with NNReal 0<alpha≤beta and actual all-point/all-vector alphaI≤HessV≤betaI. eta>0 and beta*eta≤1 are retained from the genuine conditional parent.
- Actual common Gaussian J=(x,x+sqrteta*xi)#(mu*standardGaussian), Markov/disintegrating R and reflected S_y=(2x-y)#R_y. True W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), S_y=volume.tilted(-W_y), integrable/positive partition and SAME dense closable exact original gradient D_y are produced before ALL closure-domain u.
Mathematical proof
1. Produce the true common conditional law and SAME original gradient
Use the accepted ConditionalGradient producer to construct common Markov/disintegrating R/S, reflected law and actual normalized C2 W_y with positive integrable partition. For every y the original dense closable exact D_y is fixed before ALL closure-domain u; no new operator replaces it.
Corresponding Lean step
ConditionalGradient.conditional_gradient_closable
2. Apply the shared one-way kernel implication to this actual law
The source C2 W_y gives the needed C1 regularity and genuine partition integrability. Substitute the actual S_y equality in the shared theorem and supply the SAME closable exact graph, retaining original density/closedness facts. No curvature/spectral-gap/final kernel certificate is supplied to the shared leaf.
Corresponding Lean step
GibbsGradientKernel.closed_gradient_zero_ae_constant; conditional_gradient_zero_ae_constant
3. Exercise a true nonquadratic conditional model and expose residuals
The focused Test proves actual curvature[1/2,1] of V(x)=3x^2/8+sin(x)/8 and fixes eta1/2. It constructs actual J/R/S/positive partitions/SAME original D and exercises the ALL-domain one-way implication. Constant-domain converse, full kernel equality, centered scaled residual/epsilon0/range/Poincare/BL and both main/composition remain separate.
Corresponding Lean step
Tests.WeakGradientZeroKernel.actual_nonquadratic_conditional_gradient_zero
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_gradient_zero_ae_constant
Produce the true common conditional law and SAME original gradient; Apply the shared one-way kernel implication to this actual law; Exercise a true nonquadratic conditional model and expose residuals
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_zero_ae_constant
{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) ∧
∀ u : D.closure.domain, D.closure u = 0 →
∃ c : ℝ, (u : Lp ℝ 2 (S y)) =ᵐ[S y] (fun _ => c) := 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,hd,hD,hDc,hgraph⟩ := hfiber y
refine ⟨hSy,hW,hI,hZ,D,hd,hD,hDc,hgraph,?_⟩
have hk := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel.closed_gradient_zero_ae_constant _ (hW.of_le (by norm_num)) hI
rw [← hSy] at hk
exact hk D hD hgraph
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientKernelScope and omitted-condition boundaries
- Full finite real Hilbert/Borel E including0 and actual full-space volume. Genuine locally-volume-L1 u, all C1 compact directional tests with legal integrable products and zero weak derivative imply ONE real constant volume-AE. Actual normalized Gibbs W C1/exp(-W) integrable, SAME original exact compact-smooth graph D and closability give closed-gradient-zero implies weighted-AE constant. Actual PBPS common Gaussian J/R/S and original dense D_y precede ALL closure-domain u; source C2 curvature/eta cap/positive partitions retained but no additional curvature is needed by the generic kernel leaf. Only one direction; constants-domain converse, full kernel equality, centered residual/epsilon0/range/Poincare/BL/core and both main/composition remain open. No global-volume integrability of constants, classical differentiability of rough u, Nontrivial E, final kernel certificate, spectral gap or joint fiber selector. TV never transfers unbounded cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient.conditional_gradient_closableAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel.closed_gradient_zero_ae_constant
Mathlib API called (external library)
- ContDiff.of_le
Mathematical sources
- PBPS AppendixC.1 authored analytic prerequisite — Full finite real Hilbert/Borel E including0 and actual full-space volume. Genuine locally-volume-L1 u, all C1 compact directional tests with legal integrable products and zero weak derivative imply ONE real constant volume-AE. Actual normalized Gibbs W C1/exp(-W) integrable, SAME original exact compact-smooth graph D and closability give closed-gradient-zero implies weighted-AE constant. Actual PBPS common Gaussian J/R/S and original dense D_y precede ALL closure-domain u; source C2 curvature/eta cap/positive partitions retained but no additional curvature is needed by the generic kernel leaf. Only one direction; constants-domain converse, full kernel equality, centered residual/epsilon0/range/Poincare/BL/core and both main/composition remain open. No global-volume integrability of constants, classical differentiability of rough u, Nontrivial E, final kernel certificate, spectral gap or joint fiber selector. TV never transfers unbounded 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.