Actual PBPS reflected resolvent: one solution before all cutoffs
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolvent.conditional_localized_resolvent · theorem · Teaching coverage
Mathematical statement
From actual source V/alpha/beta/eta construct true common augmentation R/S and reflected law, and for each y the original dense closable D_y before epsilon/forcing. Construct one actual u before all cutoffs in that same closure domain. Retain the actual all-domain variational equation, ordinary locally integrable u/G, all C1 compact directional weak-gradient tests, squared local integrability of r=epsilon*u+inner(grad W_y,G)-f, compact-volume L2 of u/G/r and every C2 original distribution test. For every C2 compact chi define v=chi*u, Gchi=chi*G+u*grad chi, Fchi=chi*r+2 inner(grad chi,G)+u Delta chi. Prove genuine global-volume L2 of v/Gchi/Fchi and each topological support contained in tsupport chi. For every C1 compact psi/direction a both weak-gradient products are L1 with integral psi inner(Gchi,a)=-integral v Dpsi[a]. For every C2 compact phi both PDE products are L1 with integral v Delta phi=integral Fchi phi. The same u is chosen before all cutoffs; only smooth test/cutoff functions have classical derivatives. Reflected and unreflected RGO laws/operators/scales remain distinct.
Lean statement · conditional_localized_resolvent
From actual source V/alpha/beta/eta construct true common augmentation R/S and reflected law, and for each y the original dense closable D_y before epsilon/forcing. Construct one actual u before all cutoffs in that same closure domain. Retain the actual all-domain variational equation, ordinary locally integrable u/G, all C1 compact directional weak-gradient tests, squared local integrability of r=epsilon*u+inner(grad W_y,G)-f, compact-volume L2 of u/G/r and every C2 original distribution test. For every C2 compact chi define v=chi*u, Gchi=chi*G+u*grad chi, Fchi=chi*r+2 inner(grad chi,G)+u Delta chi. Prove genuine global-volume L2 of v/Gchi/Fchi and each topological support contained in tsupport chi. For every C1 compact psi/direction a both weak-gradient products are L1 with integral psi inner(Gchi,a)=-integral v Dpsi[a]. For every C2 compact phi both PDE products are L1 with integral v Delta phi=integral Fchi phi. The same u is chosen before all cutoffs; only smooth test/cutoff functions have classical derivatives. Reflected and unreflected RGO laws/operators/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_localized_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) ∧
∀ χ : E → ℝ, ContDiff ℝ 2 χ → HasCompactSupport χ →
let v := fun x => χ x * (u : Lp ℝ 2 (S y)) x
let Gχ := fun x => χ x • D.closure u x + (u : Lp ℝ 2 (S y)) x • gradient χ x
let Fχ := fun x => χ x * (ε * (u : Lp ℝ 2 (S y)) x + inner ℝ (gradient (W y) x) (D.closure u x) - f x) + 2 * inner ℝ (gradient χ x) (D.closure u x) +
(u : Lp ℝ 2 (S y)) x * Laplacian.laplacian χ x
MemLp v 2 volume ∧ MemLp Gχ 2 volume ∧ MemLp Fχ 2 volume ∧
tsupport v ⊆ tsupport χ ∧ tsupport Gχ ⊆ tsupport χ ∧ tsupport Fχ ⊆ tsupport χ ∧
(∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
Integrable (fun x => ψ x * inner ℝ (Gχ x) a) ∧
Integrable (fun x => v x * fderiv ℝ ψ x a) ∧
(∫ x, ψ x * inner ℝ (Gχ x) a) = -∫ x, v x * fderiv ℝ ψ x a) ∧
∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
Integrable (fun x => v x * Laplacian.laplacian φ x) ∧
Integrable (fun x => Fχ x * φ x) ∧
(∫ x, v x * Laplacian.laplacian φ x) = ∫ x, Fχ x * φ xProof roadmap
- 1Construct the genuine common augmentation and reflection
Apply the actual conditional gradient producer to source V/alpha/beta/eta. Retain common Markov R/S, disintegration of the actual Gaussian/Gibbs joint law, and selected reflected S_y for every y.
- 2Keep the exact reflected density and operator scale
Retain true W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), C2 regularity and the positive integrable partition. Reflected Hessian is quarter-scaled; the unreflected RGO law, Dirichlet form and epsilon parameter are not identified without an actual adapter.
- 3Fix D_y and then one u before all cutoffs
For each fiber retain original dense closable exact compact-smooth D_y with closed closure before epsilon/forcing. The shared producer constructs u after those inputs, then all cutoffs use that u/G/r. No cutoff-specific operator or jointly measurable fiberwise solution is inserted.
- 4Derive every localized property from this actual fiber
Rewrite only the actual S_y=volume.tilted(-W_y) equality and apply the shared same-D producer. Global volume L2/support and both tested weak equations are conclusions, not new paper assumptions; keep every parent variational/ordinary/local-L2 property.
- 5Exercise an actual nonquadratic law and unnormalized cutoff
The focused Test uses V(x)=3x^2/8+sin(x)/8, genuine curvature in [1/2,1], eta in (0,1], an ordinary smooth bump chi with rIn1/rOut2 and the actual C2 test phi(x)=rho(x)(x^2)^(5/2), rho the normalized bump. For every source fiber/epsilon/forcing it extracts actual global L2/support, the particular directional weak-gradient equation at a=1, both PDE integrabilities and the localized PDE for the same u.
- 6Preserve the remaining full-paper and analytic obligations
This proves fiberwise compact localization. It supplies no localized weighted-domain membership, joint measurable selector, H2/core/Bochner, Poincare/BL, noncompact domains, epsilon0, invariance/hypocoercivity/cost or either complete sampling/composition result. The original reflected/RGO contracts remain separate.
Full assumptions and notation
All objects and hypotheses
- E has the same finite real Hilbert/Borel/full-space structure including dimension zero. Source 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.
- Actual common Gibbs/Gaussian augmentation J and Markov disintegrating R/S are constructed. S_y=(2x-y)#R_y is precisely volume.tilted(-W_y), W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), with true C2 regularity and positive integrable partition.
- For every y one original dense closable compact-smooth gradient D_y with closed closure is fixed before epsilon/input. For each epsilon>0 and true f in L2(S_y), one u/G/r serves all compact sets, ordinary tests and all C2 compact cutoffs. Existence is fiberwise; no jointly measurable solution selector, RGO operator identity or localized weighted-domain membership is concluded.
Mathematical proof
1. Construct the genuine common augmentation and reflection
Apply the actual conditional gradient producer to source V/alpha/beta/eta. Retain common Markov R/S, disintegration of the actual Gaussian/Gibbs joint law, and selected reflected S_y for every y.
Corresponding Lean step
ConditionalGradient.conditional_gradient_closable
2. Keep the exact reflected density and operator scale
Retain true W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), C2 regularity and the positive integrable partition. Reflected Hessian is quarter-scaled; the unreflected RGO law, Dirichlet form and epsilon parameter are not identified without an actual adapter.
Corresponding Lean step
hSy,hW,hI,hZ; explicit Wy
3. Fix D_y and then one u before all cutoffs
For each fiber retain original dense closable exact compact-smooth D_y with closed closure before epsilon/forcing. The shared producer constructs u after those inputs, then all cutoffs use that u/G/r. No cutoff-specific operator or jointly measurable fiberwise solution is inserted.
Corresponding Lean step
hDense,hClose,hClosed,hgraph; ContDiff.of_le
4. Derive every localized property from this actual fiber
Rewrite only the actual S_y=volume.tilted(-W_y) equality and apply the shared same-D producer. Global volume L2/support and both tested weak equations are conclusions, not new paper assumptions; keep every parent variational/ordinary/local-L2 property.
Corresponding Lean step
LocalizedWeakResolvent.localized_weak_resolvent
5. Exercise an actual nonquadratic law and unnormalized cutoff
The focused Test uses V(x)=3x^2/8+sin(x)/8, genuine curvature in [1/2,1], eta in (0,1], an ordinary smooth bump chi with rIn1/rOut2 and the actual C2 test phi(x)=rho(x)(x^2)^(5/2), rho the normalized bump. For every source fiber/epsilon/forcing it extracts actual global L2/support, the particular directional weak-gradient equation at a=1, both PDE integrabilities and the localized PDE for the same u.
Corresponding Lean step
Tests.LocalizedWeakResolvent.actual_nonconstant_cutoff_c2_pde
6. Preserve the remaining full-paper and analytic obligations
This proves fiberwise compact localization. It supplies no localized weighted-domain membership, joint measurable selector, H2/core/Bochner, Poincare/BL, noncompact domains, epsilon0, invariance/hypocoercivity/cost or either complete sampling/composition result. The original reflected/RGO contracts remain separate.
Corresponding Lean step
conditional_localized_resolvent
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_localized_resolvent
Construct the genuine common augmentation and reflection; Keep the exact reflected density and operator scale; Fix D_y and then one u before all cutoffs; Derive every localized property from this actual fiber; Exercise an actual nonquadratic law and unnormalized cutoff; Preserve the remaining full-paper and analytic obligations
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_localized_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) ∧
∀ χ : E → ℝ, ContDiff ℝ 2 χ → HasCompactSupport χ →
let v := fun x => χ x * (u : Lp ℝ 2 (S y)) x
let Gχ := fun x => χ x • D.closure u x + (u : Lp ℝ 2 (S y)) x • gradient χ x
let Fχ := fun x => χ x * (ε * (u : Lp ℝ 2 (S y)) x + inner ℝ (gradient (W y) x) (D.closure u x) - f x) + 2 * inner ℝ (gradient χ x) (D.closure u x) +
(u : Lp ℝ 2 (S y)) x * Laplacian.laplacian χ x
MemLp v 2 volume ∧ MemLp Gχ 2 volume ∧ MemLp Fχ 2 volume ∧
tsupport v ⊆ tsupport χ ∧ tsupport Gχ ⊆ tsupport χ ∧ tsupport Fχ ⊆ tsupport χ ∧
(∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
Integrable (fun x => ψ x * inner ℝ (Gχ x) a) ∧
Integrable (fun x => v x * fderiv ℝ ψ x a) ∧
(∫ x, ψ x * inner ℝ (Gχ x) a) = -∫ x, v x * fderiv ℝ ψ x a) ∧
∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
Integrable (fun x => v x * Laplacian.laplacian φ x) ∧
Integrable (fun x => Fχ x * φ x) ∧
(∫ x, v x * Laplacian.laplacian φ x) = ∫ 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.LocalizedWeakResolvent.localized_weak_resolvent Wy hW1 hI
dsimp only at hwc
rw [← hSy] at hwc
exact hwc D hClose hgraph ε hε f
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolventScope and omitted-condition boundaries
- Same actual original D/u/G/r, one u before all C2 compact chi: derive actual compact support/global volume L2 of chi*u, chi*G+u*gradchi, chi*r+2<gradchi,G>+u*Delta chi, all C1 compact weak-gradient and C2 compact distribution PDE with every L1 term legal. No localized weighted closure-domain membership, H2, Schwartz/tempered adapter, global core/Bochner, BL/Poincare, epsilon0, noncompact domain, measurable y-selector or either main/composition. Reflected/RGO law/scale remain distinct; 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.LocalizedWeakResolvent.localized_weak_resolvent
Mathlib API called (external library)
- ContDiff.of_le
Mathematical sources
- PBPS AppendixC.1 omitted analytic prerequisite — Same actual original D/u/G/r, one u before all C2 compact chi: derive actual compact support/global volume L2 of chi*u, chi*G+u*gradchi, chi*r+2<gradchi,G>+u*Delta chi, all C1 compact weak-gradient and C2 compact distribution PDE with every L1 term legal. No localized weighted closure-domain membership, H2, Schwartz/tempered adapter, global core/Bochner, BL/Poincare, epsilon0, noncompact domain, measurable y-selector or either main/composition. Reflected/RGO law/scale remain distinct; 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.