Actual noncompact conditional scores in original closed gradient
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreClosedDomain.conditional_score_closed_gradient_domain · theorem · Teaching coverage
Mathematical statement
Construct true common conditional J/R/S, positive reflected C2 potential and SAME original D_y before ALL c/u/a. Produce actual constant domain, full kernel equality and actual noncompact unnormalized directional-y score C1/gradient bound with true scalar/vector L2 class pair in SAME D_y.closure.graph. No R2/R identity or alternate operator is assumed.
Lean statement · conditional_score_closed_gradient_domain
Construct true common conditional J/R/S, positive reflected C2 potential and SAME original D_y before ALL c/u/a. Produce actual constant domain, full kernel equality and actual noncompact unnormalized directional-y score C1/gradient bound with true scalar/vector L2 class pair in SAME D_y.closure.graph. No R2/R identity or alternate operator 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_score_closed_gradient_domain
{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*η)
let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)
∃ 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) ∧
(∀ c : ℝ, ∃ u : D.closure.domain,
(u : Lp ℝ 2 (S y)) =ᵐ[S y] (fun _ => c) ∧ D.closure u=0) ∧
(∀ u : D.closure.domain, D.closure u=0 ↔
∃ c : ℝ, (u : Lp ℝ 2 (S y)) =ᵐ[S y] (fun _ => c)) ∧
∀ a : E, ContDiff ℝ 1 (fun u => s y u a) ∧
(∀ u, ‖gradient (fun z => s y z a) u‖ ≤ ((1/η-(α:ℝ))/4)*‖a‖) ∧
∃ hp : MemLp (fun u => s y u a) 2 (S y),
∃ hq : MemLp (gradient (fun u => s y u a)) 2 (S y),
(hp.toLp _,hq.toLp _) ∈ D.closure.graphProof roadmap
- 1Produce actual common law and original operator before all queries
Use the accepted conditional gradient-zero producer for common Gaussian augmentation, disintegration/reflection, actual W_y/density/positive partition and SAME original dense/closable/exact D_y. No new operator is chosen for a constant, u or direction.
- 2Produce true constants-domain and kernel on this SAME law
Apply the new shared constant-domain and Gibbs kernel equality leaves to the actual S_y and SAME D_y. Source C2 W_y yields C1; the actual partition and exact density feed the Gibbs leaf.
- 3Transfer actual score data along literal normalized density equality
The accepted score producer gives auxiliary S2_y with exactly the same explicit normalized reflected density, actual C1 scalar score/L2 and sharp gradient bound. Prove S2_y=S_y only through that density and rewrite scalar MemLp; do not identify auxiliary R2/R or separately chosen conditional versions globally.
- 4Produce genuine score gradient L2 and its original graph pair
Actual C1 score gives continuous genuine gradient, whose pointwise bound and actual Markov finite probability give vector MemLp. The new weighted C1 producer puts scalar/vector classes into SAME original D_y.closure.graph. True nonquadratic eta1/2 and E0 constant7 tests exercise source domain/kernel results; no Poincare is asserted.
Full assumptions and notation
All objects and hypotheses
- Full finite real Hilbert/Borel E including0; source V C2 and NNReal0<alpha≤beta with true all-point/all-vector alphaI≤HessV≤betaI, eta>0 and beta*eta≤1.
- Actual common Gaussian J=(x,x+sqrteta*xi)#(mu*standardGaussian), Markov/disintegrating R and reflected S_y=(2x-y)#R_y; actual W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), S_y=volume.tilted(-W_y), integrable/positive partition. SAME dense closable exact original D_y precedes ALL constants/domain elements/directions.
- Actual unnormalized parameter-y score s_y(u)[a]=-DV((y+u)/2)[a]/2-inner(y-u,a)/(4eta), not the negative u-gradient or already centered normalized score. Its C1/scalarL2/boundedgradient is produced by the accepted score theorem; only literal S2_y=S_y from exact density is used.
Mathematical proof
1. Produce actual common law and original operator before all queries
Use the accepted conditional gradient-zero producer for common Gaussian augmentation, disintegration/reflection, actual W_y/density/positive partition and SAME original dense/closable/exact D_y. No new operator is chosen for a constant, u or direction.
Corresponding Lean step
ConditionalGradientKernel.conditional_gradient_zero_ae_constant
2. Produce true constants-domain and kernel on this SAME law
Apply the new shared constant-domain and Gibbs kernel equality leaves to the actual S_y and SAME D_y. Source C2 W_y yields C1; the actual partition and exact density feed the Gibbs leaf.
Corresponding Lean step
WeightedC1GradientDomain.constants_in_closed_gradient; GibbsGradientKernelEquality.closed_gradient_zero_iff_ae_constant
3. Transfer actual score data along literal normalized density equality
The accepted score producer gives auxiliary S2_y with exactly the same explicit normalized reflected density, actual C1 scalar score/L2 and sharp gradient bound. Prove S2_y=S_y only through that density and rewrite scalar MemLp; do not identify auxiliary R2/R or separately chosen conditional versions globally.
Corresponding Lean step
ConditionalScoreDomain.conditional_curvature_and_score_domain; conditional_score_closed_gradient_domain
4. Produce genuine score gradient L2 and its original graph pair
Actual C1 score gives continuous genuine gradient, whose pointwise bound and actual Markov finite probability give vector MemLp. The new weighted C1 producer puts scalar/vector classes into SAME original D_y.closure.graph. True nonquadratic eta1/2 and E0 constant7 tests exercise source domain/kernel results; no Poincare is asserted.
Corresponding Lean step
MemLp.of_bound; WeightedC1GradientDomain.c1_in_closed_gradient; Tests.WeightedC1GradientDomain.actual_nonquadratic_score_original_domain
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_score_closed_gradient_domain
Produce actual common law and original operator before all queries; Produce true constants-domain and kernel on this SAME law; Transfer actual score data along literal normalized density equality; Produce genuine score gradient L2 and its original graph pair
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_score_closed_gradient_domain
{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*η)
let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)
∃ 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) ∧
(∀ c : ℝ, ∃ u : D.closure.domain,
(u : Lp ℝ 2 (S y)) =ᵐ[S y] (fun _ => c) ∧ D.closure u=0) ∧
(∀ u : D.closure.domain, D.closure u=0 ↔
∃ c : ℝ, (u : Lp ℝ 2 (S y)) =ᵐ[S y] (fun _ => c)) ∧
∀ a : E, ContDiff ℝ 1 (fun u => s y u a) ∧
(∀ u, ‖gradient (fun z => s y z a) u‖ ≤ ((1/η-(α:ℝ))/4)*‖a‖) ∧
∃ hp : MemLp (fun u => s y u a) 2 (S y),
∃ hq : MemLp (gradient (fun u => s y u a)) 2 (S y),
(hp.toLp _,hq.toLp _) ∈ D.closure.graph := by
obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientKernel.conditional_gradient_zero_ae_constant
hα hαβ hV hH hη hβη
obtain ⟨R2,S2,_,_,_,_,hfiber2⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain.conditional_curvature_and_score_domain
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
obtain ⟨hS2y,_,_,_,_,_,hscore⟩ := hfiber2 y
have hmeas : S2 y=S y := hS2y.trans hSy.symm
let : IsMarkovKernel S := hS
refine ⟨hSy,hW,hI,hZ,D,hd,hD,hDc,hgraph,?_,?_,?_⟩
· intro c
exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.constants_in_closed_gradient (S y) D hD hgraph c
· have hk := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernelEquality.closed_gradient_zero_iff_ae_constant _ (hW.of_le (by norm_num)) hI
rw [← hSy] at hk
exact hk D hD hgraph
· intro a
obtain ⟨hqa,hpa,_,hga⟩ := hscore a
rw [hmeas] at hpa
have hq : MemLp (gradient (fun u =>
(-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)) a)) 2 (S y) :=
MemLp.of_bound ((toDual ℝ E).symm.continuous.comp
(hqa.continuous_fderiv one_ne_zero)).aestronglyMeasurable _ (Eventually.of_forall hga)
exact ⟨hqa,hga,hpa,hq,AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.c1_in_closed_gradient (S y) D hD hgraph hqa hpa hq⟩
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreClosedDomainScope and omitted-condition boundaries
- Actual finite real Hilbert/Borel E including0. Fix actual finite mu and SAME original closable exact compact-C-infinity gradient D BEFORE ALL C1 f with actual MemLp f2mu and MemLp gradientf2mu. Genuine smooth cutoff exhaustion/derivative-product/weighted L2 limits put actual class pair into SAME closure graph, without compact support or extra spatial moment. Finite mu constants are genuinely in original closure domain with outputzero. For actual C1 Gibbs W/exp(-W) integrable, combine actual constants-domain with accepted one-way implication for full zero-output iff AEconstant on SAME D. Actual PBPS common Gaussian J/R/S/Sdensity/positive partitions/sourceC2 alpha beta eta cap and original D_y beforeALL constants/u/directions; real unnormalized y-score C1/L2/boundedgradient from accepted score producer transfers along ONLY explicit reflected density equality S2_y=S_y and enters SAME original closed graph. No R2=R or alternateD equality, global ordinary L1, C-infinity potential, gradient of rough representative, Nontrivial E, spatial moment, supplied domain/fullkernel/spectralgap/Poincare certificate, epsilon0/range/centering/measurablejointselector/core/BL/main/composition. TV never transfers unbounded cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.c1_in_closed_gradientAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.constants_in_closed_gradientAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernelEquality.closed_gradient_zero_iff_ae_constantAutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientKernel.conditional_gradient_zero_ae_constantAutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain.conditional_curvature_and_score_domain
Mathlib API called (external library)
- MemLp.of_bound
- ContDiff.continuous_fderiv
Mathematical sources
- PBPS AppC1 authored original-gradient domain prerequisite — Actual finite real Hilbert/Borel E including0. Fix actual finite mu and SAME original closable exact compact-C-infinity gradient D BEFORE ALL C1 f with actual MemLp f2mu and MemLp gradientf2mu. Genuine smooth cutoff exhaustion/derivative-product/weighted L2 limits put actual class pair into SAME closure graph, without compact support or extra spatial moment. Finite mu constants are genuinely in original closure domain with outputzero. For actual C1 Gibbs W/exp(-W) integrable, combine actual constants-domain with accepted one-way implication for full zero-output iff AEconstant on SAME D. Actual PBPS common Gaussian J/R/S/Sdensity/positive partitions/sourceC2 alpha beta eta cap and original D_y beforeALL constants/u/directions; real unnormalized y-score C1/L2/boundedgradient from accepted score producer transfers along ONLY explicit reflected density equality S2_y=S_y and enters SAME original closed graph. No R2=R or alternateD equality, global ordinary L1, C-infinity potential, gradient of rough representative, Nontrivial E, spatial moment, supplied domain/fullkernel/spectralgap/Poincare certificate, epsilon0/range/centering/measurablejointselector/core/BL/main/composition. 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.