Actual PBPS conditional C1 weak-resolvent tests
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalC1Resolvent.conditional_c1_resolvent · theorem · Teaching coverage
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.
Lean statement · conditional_c1_resolvent
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.
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_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)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.
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.
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.
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.
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.
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.
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
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_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.ConditionalC1ResolventScope 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
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient.conditional_gradient_closableAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventC1.weak_resolvent_c1
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.