Actual PBPS reflected global quarter-scale coercivity

Samplinglib authored full-space positive-epsilon scalar prerequisite toward PBPS conditional Poincare and SPHMC BL; not a quoted numbered theorem or complete paper result.

Complete source statement (Samplinglib restatement)

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.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual PBPS reflected global quarter-scale coercivity

AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGlobalCoercivity.conditional_global_coercivity · theorem · Teaching coverage

Read this first

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.

\[\exists R,S\ \forall y\ \exists D_y\ \forall\varepsilon>0,f\ \exists u:\quad\frac{\alpha+\eta^{-1}}4\|\overline D_yu\|_{S_y}^2\le\|f-\varepsilon u\|_{S_y}^2\le\|f\|_{S_y}^2.\]

Lean statement · conditional_global_coercivity

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.

Download module (.lean)

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

Exact module and namespace context

Proof 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.

\[S_y=Z_y^{-1}e^{-W_y}dz,\quad W_y(z)=V((y+z)/2)+\|z-y\|^2/(8\eta).\]

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.

\[\frac{\alpha+\eta^{-1}}4I\preceq\nabla^2W_y\preceq\frac{\beta+\eta^{-1}}4I.\]

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.

\[\frac{\alpha+\eta^{-1}}4\|\overline D_yu\|^2\le\|f-\varepsilon u\|^2\le\|f\|^2.\]

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.

\[m=(1/2+2)/4=5/8.\]

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.

\[\text{positive-epsilon scalar bound only; Poincare/BL/main/composition remain open}.\]

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

Download module (.lean)

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.ConditionalGlobalCoercivity

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source C2 curvature-bounded reflected conditional route.	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 betaeta<=1 are retained. Actual Gaussian augmentation J=(x,x+sqrtetaxi)#(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.	source-implicit	Generic normalized Gibbs/original gradient interface disclosed; true source C2/two-sided curvature/eta/reflected laws and quarter constants retained including0.
Analytic density/closedness and global scalar passage omitted in AppendixC.1.	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-epsilonu)^2<=normf^2 from true reflected lower/upper curvature. No joint measurable fiber choice or complete Poincare/BL/main result is inferred.	source-implicit	Derive actual weighted radial cutoff/commutator limits and compact scalar passage without extra spatial moments or final limit/core/inequality certificates.
Conditional Poincare, SPHMC BL covariance-upper and both main results.	Same original compact-smooth gradient D precedes epsilon/f; derive ONE actual variational/localized resolvent u and actual weighted radial cutoff/commutator limits. Prove mnorm(D.closure u)^2<=norm(f-epsilonu)^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.	unresolved	Positive-epsilon scalar control does not prove actual constant kernel/domain, centered residual/range/Poincare/BL, full core/adjoint/global Bochner or main/composition.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope 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

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.

Actual PBPS reflected global quarter-scale coercivity

Complete source statement (Samplinglib restatement)

Actual PBPS reflected global quarter-scale coercivity

Read the formalized proofs

Actual PBPS reflected global quarter-scale coercivity

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Keep the genuine reflected kernels and original graph

2. Extract BOTH reflected Hessian bounds for the explicit potential

3. Consume the actual shared global producer on original D_y

4. Exercise true nonquadratic curvature and exact5/8

5. Expose the remaining analytic and paper boundary

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?