Actual PBPS reflected conditional resolvents have the ordinary weak Laplacian
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalOrdinaryResolvent.conditional_ordinary_resolvent · theorem · Teaching coverage
Mathematical statement
For actual source V/alpha/beta/eta, construct genuine common augmentation R/S and exact reflected conditional laws. For every y, retain the true positive integrable C2 W_y and original dense closable compact smooth gradient D_y before epsilon/input. Every epsilon>0 and actual f in L2(S_y) has u in that same closure domain, the full variational and ordinary weak-gradient identities, genuine local volume L2 of u/G/k_y, locally integrable squared norm of k_y, and for all C2 compact phi the legal ordinary volume distribution identity integral u Delta phi = integral k_y phi, where k_y=epsilon u+inner(gradient W_y,G)-f. Reflected/RGO laws and scales remain distinct.
Lean statement · conditional_ordinary_resolvent
For actual source V/alpha/beta/eta, construct genuine common augmentation R/S and exact reflected conditional laws. For every y, retain the true positive integrable C2 W_y and original dense closable compact smooth gradient D_y before epsilon/input. Every epsilon>0 and actual f in L2(S_y) has u in that same closure domain, the full variational and ordinary weak-gradient identities, genuine local volume L2 of u/G/k_y, locally integrable squared norm of k_y, and for all C2 compact phi the legal ordinary volume distribution identity integral u Delta phi = integral k_y phi, where k_y=epsilon u+inner(gradient W_y,G)-f. Reflected/RGO laws and scales remain distinct.
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_ordinary_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) ∧
LocallyIntegrable (fun x => ‖ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u x) - f x‖ ^ 2) ∧
(∀ K : Set E, IsCompact K →
MemLp (fun x => (u : Lp ℝ 2 (S y)) x) 2 (volume.restrict K) ∧
MemLp (fun x => D.closure u x) 2 (volume.restrict K) ∧
MemLp (fun x => ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u x) - f x) 2 (volume.restrict K)) ∧
∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
Integrable (fun x => (u : Lp ℝ 2 (S y)) x * Laplacian.laplacian φ x) ∧
Integrable (fun x => (ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u x) - f x) * φ x) ∧
(∫ x, (u : Lp ℝ 2 (S y)) x * Laplacian.laplacian φ x) =
∫ x, (ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u x) - f x) * φ xProof roadmap
- 1Construct actual common augmentation and conditional kernels
Use the true Gibbs/Gaussian augmentation and existing conditional gradient producer. Its common Markov R/S disintegrate the actual swapped joint law, with S_y the reflected pushforward of R_y for every selected fiber.
- 2Preserve the reflected potential and true partition
Retain the exact density, C2 regularity, integrable exponential weight and positive normalizing constant. This is W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta). The unreflected RGO potential has a different law and Hessian scale; no operator/domain identity is inferred from pushforward.
- 3Fix the original operator before epsilon and forcing
For each y retain the original dense closable exact compact smooth gradient D_y and its closed closure. Neither the operator nor kernels depend on epsilon or the forcing. Reduction of C2 W_y to C1 changes only the regularity interface.
- 4Apply the canonical ordinary PDE producer to this exact fiber
Rewrite only the true law equality S_y=volume.tilted(-W_y), then apply the canonical weak-Laplacian result to the same D_y. The actual u/G and drift-minus-forcing right-hand side are conclusions, not supplied certificates. The distribution identity uses ordinary volume and preserves unit epsilon/drift/Laplacian coefficients.
- 5Exercise the equation at a real C2 compact observable
A focused test uses the actual nonquadratic V(x)=3x^2/8+sin(x)/8, true curvature between 1/2 and 1, eta in (0,1], and phi(x)=rho(x)(x^2)^(5/2) with genuine normalized smooth compact bump rho. It extracts both integrability conclusions and the particular ordinary PDE from the true conditional solution, for every positive epsilon and actual forcing.
- 6Keep subsequent analytic and full-paper obligations visible
This remains a fiberwise ordinary weak-Laplacian/local-L2 prerequisite. It does not construct joint measurable resolvents or prove local H2, global core/Bochner, conditional Poincare/BL, macro H1, hypocoercivity or either full sampling/composition theorem. Noncompact constant/linear tests still require actual tail/domain arguments.
Full assumptions and notation
All objects and hypotheses
- E has the same real finite-dimensional Hilbert/Borel/full-space structure, including dimension zero. V is C2 with all-point/all-direction alpha I≤Hess V≤beta I, alpha,beta NNReal, 0<alpha≤beta; eta>0 and beta eta≤1.
- The Gibbs/Gaussian augmentation, common Markov R/S, disintegration R, reflection S_y=(2x-y)#R_y, and true reflected W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta) are derived. Each selected S_y is precisely volume.tilted(-W_y), with positive integrable partition and C2 W_y.
- For every y there is one original dense closable exact compact smooth gradient D_y with closed closure, fixed before epsilon and forcing. Every epsilon>0 and genuine f in L2(S_y) has one u/G serving all ordinary tests and compact sets. Existence is fiberwise; no joint measurable solution selection in y is concluded.
Mathematical proof
1. Construct actual common augmentation and conditional kernels
Use the true Gibbs/Gaussian augmentation and existing conditional gradient producer. Its common Markov R/S disintegrate the actual swapped joint law, with S_y the reflected pushforward of R_y for every selected fiber.
Corresponding Lean step
ConditionalGradient.conditional_gradient_closable
2. Preserve the reflected potential and true partition
Retain the exact density, C2 regularity, integrable exponential weight and positive normalizing constant. This is W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta). The unreflected RGO potential has a different law and Hessian scale; no operator/domain identity is inferred from pushforward.
Corresponding Lean step
hSy,hW,hI,hZ; explicit Wy
3. Fix the original operator before epsilon and forcing
For each y retain the original dense closable exact compact smooth gradient D_y and its closed closure. Neither the operator nor kernels depend on epsilon or the forcing. Reduction of C2 W_y to C1 changes only the regularity interface.
Corresponding Lean step
hDense,hClose,hClosed,hgraph; ContDiff.of_le
4. Apply the canonical ordinary PDE producer to this exact fiber
Rewrite only the true law equality S_y=volume.tilted(-W_y), then apply the canonical weak-Laplacian result to the same D_y. The actual u/G and drift-minus-forcing right-hand side are conclusions, not supplied certificates. The distribution identity uses ordinary volume and preserves unit epsilon/drift/Laplacian coefficients.
Corresponding Lean step
OrdinaryWeakResolvent.weak_resolvent_laplacian; rw [hSy]
5. Exercise the equation at a real C2 compact observable
A focused test uses the actual nonquadratic V(x)=3x^2/8+sin(x)/8, true curvature between 1/2 and 1, eta in (0,1], and phi(x)=rho(x)(x^2)^(5/2) with genuine normalized smooth compact bump rho. It extracts both integrability conclusions and the particular ordinary PDE from the true conditional solution, for every positive epsilon and actual forcing.
Corresponding Lean step
Tests.OrdinaryWeakResolvent.actual_nonconstant_c2_pde
6. Keep subsequent analytic and full-paper obligations visible
This remains a fiberwise ordinary weak-Laplacian/local-L2 prerequisite. It does not construct joint measurable resolvents or prove local H2, global core/Bochner, conditional Poincare/BL, macro H1, hypocoercivity or either full sampling/composition theorem. Noncompact constant/linear tests still require actual tail/domain arguments.
Corresponding Lean step
conditional_ordinary_resolvent
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_ordinary_resolvent
Construct actual common augmentation and conditional kernels; Preserve the reflected potential and true partition; Fix the original operator before epsilon and forcing; Apply the canonical ordinary PDE producer to this exact fiber; Exercise the equation at a real C2 compact observable; Keep subsequent analytic and full-paper obligations visible
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_ordinary_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) ∧
LocallyIntegrable (fun x => ‖ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u x) - f x‖ ^ 2) ∧
(∀ K : Set E, IsCompact K →
MemLp (fun x => (u : Lp ℝ 2 (S y)) x) 2 (volume.restrict K) ∧
MemLp (fun x => D.closure u x) 2 (volume.restrict K) ∧
MemLp (fun x => ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u x) - f x) 2 (volume.restrict K)) ∧
∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
Integrable (fun x => (u : Lp ℝ 2 (S y)) x * Laplacian.laplacian φ x) ∧
Integrable (fun x => (ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u x) - f x) * φ x) ∧
(∫ x, (u : Lp ℝ 2 (S y)) x * Laplacian.laplacian φ x) =
∫ x, (ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (W y) x) (D.closure u 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.OrdinaryWeakResolvent.weak_resolvent_laplacian Wy hW1 hI
dsimp only at hwc
rw [← hSy] at hwc
exact hwc D hClose hgraph ε hε f
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalOrdinaryResolventScope and omitted-condition boundaries
- Same actual D/u/G and forcing yield ordinary volume distribution Delta u=epsilon u+inner(gradient W,G)-f, all C2 compact tests with genuine L1 products, and genuine local L2 of u/G/right-hand side. Full existing variational and ordinary weak-gradient identities retained. Actual PBPS R/S/reflected law and fixed fiber D before epsilon/input. No local H2, global generator core/Bochner, Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1 or complete paper/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.OrdinaryWeakResolvent.weak_resolvent_laplacian
Mathlib API called (external library)
- ContDiff.of_le
Mathematical sources
- PBPS AppendixC.1 omitted analytic prerequisite — Same actual D/u/G and forcing yield ordinary volume distribution Delta u=epsilon u+inner(gradient W,G)-f, all C2 compact tests with genuine L1 products, and genuine local L2 of u/G/right-hand side. Full existing variational and ordinary weak-gradient identities retained. Actual PBPS R/S/reflected law and fixed fiber D before epsilon/input. No local H2, global generator core/Bochner, Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1 or complete paper/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.