Actual PBPS reflected global quarter-scale coercivity
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGlobalCoercivity.conditional_global_coercivity · theorem · Teaching coverage
Mathematical statement
Construct genuine common R/S and for each y fix original D_y before epsilon/f. Produce ONE actual u in the SAME original D.closure.domain for every positive epsilon and forcing, all-domain variational identity, local-volume L1 of u/G, ALL C1 compact ordinary weak-gradient products/identity, local squared PDE residual and compact-volume L2, ALL C2 compact ordinary weak-Poisson products/identity, and ALL C2 compact chi actual v/Gchi/Fchi volumeL2/support/weak identities. Derive exact ((alpha+eta^-1)/4)*norm(D_y.closureu)^2≤norm(f-epsilon*u)^2≤normf^2 from true reflected lower/upper curvature. No joint measurable fiber choice or complete Poincare/BL/main result is inferred.
Lean statement · conditional_global_coercivity
Construct genuine common R/S and for each y fix original D_y before epsilon/f. Produce ONE actual u in the SAME original D.closure.domain for every positive epsilon and forcing, all-domain variational identity, local-volume L1 of u/G, ALL C1 compact ordinary weak-gradient products/identity, local squared PDE residual and compact-volume L2, ALL C2 compact ordinary weak-Poisson products/identity, and ALL C2 compact chi actual v/Gchi/Fchi volumeL2/support/weak identities. Derive exact ((alpha+eta^-1)/4)*norm(D_y.closureu)^2<=norm(f-epsilon*u)^2<=normf^2 from true reflected lower/upper curvature. No joint measurable fiber choice or complete Poincare/BL/main result is inferred.
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_global_coercivity {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) ∧
(((α:ℝ)+1/η)/4)*‖D.closure u‖^2 ≤
‖f-ε • (u : Lp ℝ 2 (S y))‖^2 ∧
‖f-ε • (u : Lp ℝ 2 (S y))‖^2 ≤ ‖f‖^2 ∧
∀ χ : 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
- 1Keep the genuine reflected kernels and original graph
Consume the actual ConditionalLocalizedResolvent kernels/partition/original D_y before epsilon/f. Retain every original local/weak/cutoff fact. The shared global producer constructs the actual solution on this same graph, not an arbitrary supplied u or a new domain.
- 2Extract BOTH reflected Hessian bounds for the explicit potential
Use the accepted conditional Hessian formula and source V bounds to derive m=(alpha+eta^-1)/4 and M=(beta+eta^-1)/4 with 0<m≤M. Only explicit W_y derivative facts are reused; auxiliary kernels are not identified. Reflected and unreflected RGO constants and laws remain distinct.
- 3Consume the actual shared global producer on original D_y
Supply genuine S_y law equality, C2/partition/curvature and original closable exact graph. The shared producer derives ONE actual variational u, global quarter-scale coercivity and the forcing bound, with all original weak/local/cutoff data. No weighted cutoff limit or final inequality is an input.
- 4Exercise true nonquadratic curvature and exact5/8
The focused Test proves V=3x^2/8+sin(x)/8 has curvature[1/2,1], chooses actual eta1/2 and source common J/R/S/originalD/u. It extracts the actual global constant5/8, residual forcing bound and original ordinary C2-cutoff data for rho(x)*abs(x)^5, without requiring that cutoff to be C-infinity.
- 5Expose the remaining analytic and paper boundary
Actual kernel=constants, constant-domain membership, centered scaled residual/epsilon-zero/range/Poincare, linear-observable/BL, adjoint/core/global Bochner identity and both main/composition remain separate unproved obligations. No jointly measurable selector or TV-to-unbounded-cost implication is claimed.
Full assumptions and notation
All objects and hypotheses
- Finite real Hilbert/Borel E including0; V C2, NNReal alpha/beta with 0<alpha≤beta and actual all-point/all-vector alpha I≤HessV≤beta I. eta>0 and beta*eta≤1 are retained.
- Actual Gaussian augmentation J=(x,x+sqrteta*xi)#(mu*standardGaussian) and common genuine Markov/disintegrating R/S with S_y=(2x-y)#R_y and S_y=volume.tilted(-W_y), W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta). Source C2 W_y, integrability/positive partition and original dense closable exact compact-smooth D_y with closed closure are produced. Only explicit W_y Hessian facts are extracted from the accepted curvature parent; its auxiliary R2/S2 are not equated with the resolvent kernels.
Mathematical proof
1. Keep the genuine reflected kernels and original graph
Consume the actual ConditionalLocalizedResolvent kernels/partition/original D_y before epsilon/f. Retain every original local/weak/cutoff fact. The shared global producer constructs the actual solution on this same graph, not an arbitrary supplied u or a new domain.
Corresponding Lean step
ConditionalLocalizedResolvent.conditional_localized_resolvent
2. Extract BOTH reflected Hessian bounds for the explicit potential
Use the accepted conditional Hessian formula and source V bounds to derive m=(alpha+eta^-1)/4 and M=(beta+eta^-1)/4 with 0<m≤M. Only explicit W_y derivative facts are reused; auxiliary kernels are not identified. Reflected and unreflected RGO constants and laws remain distinct.
Corresponding Lean step
ConditionalScoreDomain.conditional_curvature_and_score_domain; hlower; hupper
3. Consume the actual shared global producer on original D_y
Supply genuine S_y law equality, C2/partition/curvature and original closable exact graph. The shared producer derives ONE actual variational u, global quarter-scale coercivity and the forcing bound, with all original weak/local/cutoff data. No weighted cutoff limit or final inequality is an input.
Corresponding Lean step
GlobalWeightedResolventCoercivity.global_weak_resolvent_coercivity
4. Exercise true nonquadratic curvature and exact5/8
The focused Test proves V=3x^2/8+sin(x)/8 has curvature[1/2,1], chooses actual eta1/2 and source common J/R/S/originalD/u. It extracts the actual global constant5/8, residual forcing bound and original ordinary C2-cutoff data for rho(x)*abs(x)^5, without requiring that cutoff to be C-infinity.
Corresponding Lean step
Tests.GlobalWeightedResolventCoercivity.actual_nonquadratic_global_coercivity
5. Expose the remaining analytic and paper boundary
Actual kernel=constants, constant-domain membership, centered scaled residual/epsilon-zero/range/Poincare, linear-observable/BL, adjoint/core/global Bochner identity and both main/composition remain separate unproved obligations. No jointly measurable selector or TV-to-unbounded-cost implication is claimed.
Corresponding Lean step
conditional_global_coercivity
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_global_coercivity
Keep the genuine reflected kernels and original graph; Extract BOTH reflected Hessian bounds for the explicit potential; Consume the actual shared global producer on original D_y; Exercise true nonquadratic curvature and exact5/8; Expose the remaining analytic and paper boundary
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_global_coercivity {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) ∧
(((α:ℝ)+1/η)/4)*‖D.closure u‖^2 ≤
‖f-ε • (u : Lp ℝ 2 (S y))‖^2 ∧
‖f-ε • (u : Lp ℝ 2 (S y))‖^2 ≤ ‖f‖^2 ∧
∀ χ : 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 ⟨_R2,_S2,_hR2,_hS2,_hcond2,_hSR2,hcurv⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain.conditional_curvature_and_score_domain
hα hαβ hV hH hη hβη
obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolvent.conditional_localized_resolvent
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
obtain ⟨_,_,_,hderiv,hlower,_,_⟩ := hcurv y
have hupper (x a : E) :
(fderiv ℝ (fderiv ℝ (fun z => V ((1/2:ℝ) • (y+z))+‖z-y‖^2/(8*η))) x a) a
≤ (((β:ℝ)+1/η)/4)*‖a‖^2 := by
rw [(hderiv x a a).1,real_inner_self_eq_norm_sq]
have hv := (hH ((1/2:ℝ) • (y+x)) a).2
have hn : (((β:ℝ)+1/η)/4)*‖a‖^2 =
(1/4:ℝ)*((β:ℝ)*‖a‖^2)+(1/(4*η))*‖a‖^2 := by ring
rw [hn]
nlinarith
have hβ : (α:ℝ) ≤ (β:ℝ) := by exact_mod_cast hαβ
have hm : 0 < ((α:ℝ)+1/η)/4 := by positivity
have hmM : ((α:ℝ)+1/η)/4 ≤ ((β:ℝ)+1/η)/4 := by linarith
refine ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph,?_⟩
exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GlobalWeightedResolventCoercivity.global_weak_resolvent_coercivity
(fun z => V ((1/2:ℝ) • (y+z))+‖z-y‖^2/(8*η)) hW hI hZ
(((α:ℝ)+1/η)/4) (((β:ℝ)+1/η)/4) hm hmM hlower hupper (S y) hSy D hClose hgraph
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGlobalCoercivityScope and omitted-condition boundaries
- Same original compact-smooth gradient D precedes epsilon/f; derive ONE actual variational/localized resolvent u and actual weighted radial cutoff/commutator limits. Prove m*norm(D.closure u)^2≤norm(f-epsilon*u)^2≤normf^2 with source C2/two-sided0<m≤M Hessian bounds. E0 retained. No final limit/coercivity/core certificate, extra norm(x)*u moment, global ordinary Laplacian or drift-product L2, C-infinity potential, epsilon0/kernel/constant-domain/range/Poincare/BL/adjoint/core/jointselector/main/composition is inferred. Reflected quarter/fourfold constants exact; TV never transfers unbounded cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolvent.conditional_localized_resolventAutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain.conditional_curvature_and_score_domainAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GlobalWeightedResolventCoercivity.global_weak_resolvent_coercivity
Mathlib API called (external library)
- real_inner_self_eq_norm_sq
Mathematical sources
- PBPS AppendixC.1 authored analytic prerequisite — Same original compact-smooth gradient D precedes epsilon/f; derive ONE actual variational/localized resolvent u and actual weighted radial cutoff/commutator limits. Prove m*norm(D.closure u)^2<=norm(f-epsilon*u)^2<=normf^2 with source C2/two-sided0<m<=M Hessian bounds. E0 retained. No final limit/coercivity/core certificate, extra norm(x)*u moment, global ordinary Laplacian or drift-product L2, C-infinity potential, epsilon0/kernel/constant-domain/range/Poincare/BL/adjoint/core/jointselector/main/composition is inferred. Reflected quarter/fourfold constants exact; 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.