Actual PBPS reflected resolvent: compact weighted coercivity
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactCoercivity.conditional_compact_coercivity · theorem · Teaching coverage
Mathematical statement
Construct genuine common R/S; for every y fix original D_y before epsilon/f, choose ONE u before ALL C2 compact chi. Retain actual R/S/reflection/positive partitions, the same original D graph/density/closability/closed closure, ONE u and all-domain variational identity, original local u/G/r square integrability, every original C1 weak-gradient test/C2 weak PDE, and every cutoff volumeL2/support/weak identity. For each cutoff produce actual weighted classes vW,AW,GW linked to v=chi*u, Gchi and Achi=inner(gradientW,Gchi)-Fchi, original (vW,GW) in D_y.closure.graph and ((alpha+eta^-1)/4)*norm(GW)^2≤norm(AW)^2.
Lean statement · conditional_compact_coercivity
Construct genuine common R/S; for every y fix original D_y before epsilon/f, choose ONE u before ALL C2 compact chi. Retain actual R/S/reflection/positive partitions, the same original D graph/density/closability/closed closure, ONE u and all-domain variational identity, original local u/G/r square integrability, every original C1 weak-gradient test/C2 weak PDE, and every cutoff volumeL2/support/weak identity. For each cutoff produce actual weighted classes vW,AW,GW linked to v=chi*u, Gchi and Achi=inner(gradientW,Gchi)-Fchi, original (vW,GW) in D_y.closure.graph and ((alpha+eta^-1)/4)*norm(GW)^2<=norm(AW)^2.
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_compact_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) ∧
∀ χ : 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) ∧
let Aχ := fun x => inner ℝ (gradient (W y) x) (Gχ x)-Fχ x
MemLp v 2 (S y) ∧ MemLp Gχ 2 (S y) ∧ MemLp Aχ 2 (S y) ∧
∃ vW AW : Lp ℝ 2 (S y), ∃ GW : Lp E 2 (S y),
vW =ᵐ[S y] v ∧ AW =ᵐ[S y] Aχ ∧ GW =ᵐ[S y] Gχ ∧
(vW,GW) ∈ D.closure.graph ∧ (((α:ℝ)+1/η)/4) * ‖GW‖^2 ≤ ‖AW‖^2Proof roadmap
- 1Keep genuine source kernels, reflected potential and original resolvent
Consume ConditionalLocalizedResolvent with exact source curvature/eta inputs. Retain its same J/R/S and true reflected density, positive partitions, original D before epsilon/f and ONE u before ALL C2 compact cutoffs. All original local/weak/volumeL2 identities remain visible.
- 2Reuse the exact quarter-scale Hessian lower bound
The accepted ConditionalScoreDomain producer proves the lower Hessian bound for this explicit W_y. Extract only that pointwise fact; do not identify its auxiliary kernels with the resolvent kernels. Reflected and RGO operators/laws remain distinct.
- 3Apply the shared producer to the same localized weak data
For each C2 cutoff extract actual volumeL2/support and every weak equation for v/Gchi/Fchi from the SAME u. Pass the true equality S_y=tilted(-W_y), original closable D/exact graph and actual lower curvature to the shared producer. It derives the actual weighted classes and same-D graph membership; the desired weighted conclusion is never a premise.
- 4Exercise a true nonquadratic source potential and C2 cutoff
The focused Test uses V=3x^2/8+sin(x)/8 with curvature[1/2,1], eta in(0,1], actual R/S/D/u and cutoff rho(x)*(x^2)^(5/2), certified C2 and not required to be smooth of all orders. It extracts true weighted MemLp/AE, original graph membership and the exact quarter-constant inequality.
- 5Keep the scalar endpoint separate from larger paper obligations
No jointly measurable fiber choice, cutoff removal, rough Hessian/global Bochner, adjoint/core identity, epsilon-zero/kernel/range/Poincare/BL or either main/composition follows from this packet. TV proximity still cannot transfer an unbounded expected cost.
Full assumptions and notation
All objects and hypotheses
- Same finite-dimensional real Hilbert/Borel structure including dimension zero. Source V is C2; alpha,beta are NNReal with 0<alpha≤beta, actual all-point/all-vector alpha I≤Hess V≤beta I, eta>0 and beta*eta≤1.
- Actual augmentation J=(x,x+sqrt(eta)*xi)#(mu*standardGaussian), common probability/disintegrating R/S, S_y=(2x-y)#R_y=volume.tilted(-W_y), W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), C2 W_y and positive integrable partition are genuine parent conclusions. The accepted curvature parent yields HessW_y ≥ ((alpha+eta^-1)/4)I for this same explicit W, without equating its auxiliary kernels with the resolvent kernels.
- Original dense closable exact compact-smooth gradient D_y and closed closure are fixed before epsilon/f. For every epsilon>0 and f in actual L2(S_y), ONE actual u precedes ALL real C2 compact cutoffs chi. Parent all-domain variational identity, original ordinary weak/local facts and actual localized v=chi*u, Gchi=chi*D.closure(u)+u*gradientchi, Fchi=chi*r+2inner(gradientchi,D.closure(u))+u*Deltachi, r=epsilon*u+inner(gradientW,D.closure(u))-f, are retained.
Mathematical proof
1. Keep genuine source kernels, reflected potential and original resolvent
Consume ConditionalLocalizedResolvent with exact source curvature/eta inputs. Retain its same J/R/S and true reflected density, positive partitions, original D before epsilon/f and ONE u before ALL C2 compact cutoffs. All original local/weak/volumeL2 identities remain visible.
Corresponding Lean step
ConditionalLocalizedResolvent.conditional_localized_resolvent
2. Reuse the exact quarter-scale Hessian lower bound
The accepted ConditionalScoreDomain producer proves the lower Hessian bound for this explicit W_y. Extract only that pointwise fact; do not identify its auxiliary kernels with the resolvent kernels. Reflected and RGO operators/laws remain distinct.
Corresponding Lean step
ConditionalScoreDomain.conditional_curvature_and_score_domain; hlower
3. Apply the shared producer to the same localized weak data
For each C2 cutoff extract actual volumeL2/support and every weak equation for v/Gchi/Fchi from the SAME u. Pass the true equality S_y=tilted(-W_y), original closable D/exact graph and actual lower curvature to the shared producer. It derives the actual weighted classes and same-D graph membership; the desired weighted conclusion is never a premise.
Corresponding Lean step
CompactWeightedPoissonCoercivity.compact_weak_poisson_weighted_coercivity
4. Exercise a true nonquadratic source potential and C2 cutoff
The focused Test uses V=3x^2/8+sin(x)/8 with curvature[1/2,1], eta in(0,1], actual R/S/D/u and cutoff rho(x)*(x^2)^(5/2), certified C2 and not required to be smooth of all orders. It extracts true weighted MemLp/AE, original graph membership and the exact quarter-constant inequality.
Corresponding Lean step
Tests.CompactWeightedPoissonCoercivity.actual_c2_cutoff_weighted_coercivity
5. Keep the scalar endpoint separate from larger paper obligations
No jointly measurable fiber choice, cutoff removal, rough Hessian/global Bochner, adjoint/core identity, epsilon-zero/kernel/range/Poincare/BL or either main/composition follows from this packet. TV proximity still cannot transfer an unbounded expected cost.
Corresponding Lean step
conditional_compact_coercivity
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_compact_coercivity
Keep genuine source kernels, reflected potential and original resolvent; Reuse the exact quarter-scale Hessian lower bound; Apply the shared producer to the same localized weak data; Exercise a true nonquadratic source potential and C2 cutoff; Keep the scalar endpoint separate from larger paper 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_compact_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) ∧
∀ χ : 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) ∧
let Aχ := fun x => inner ℝ (gradient (W y) x) (Gχ x)-Fχ x
MemLp v 2 (S y) ∧ MemLp Gχ 2 (S y) ∧ MemLp Aχ 2 (S y) ∧
∃ vW AW : Lp ℝ 2 (S y), ∃ GW : Lp E 2 (S y),
vW =ᵐ[S y] v ∧ AW =ᵐ[S y] Aχ ∧ GW =ᵐ[S y] Gχ ∧
(vW,GW) ∈ D.closure.graph ∧ (((α:ℝ)+1/η)/4) * ‖GW‖^2 ≤ ‖AW‖^2 := 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,hsolve⟩ := hfiber y
obtain ⟨_,_,_,_,hlower,_,_⟩ := hcurv y
refine ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph,?_⟩
intro ε hε f
obtain ⟨u,hu,huL,hgradL,hd,hr2,hl,hp,hcut⟩ := hsolve ε hε f
refine ⟨u,hu,huL,hgradL,hd,hr2,hl,hp,?_⟩
intro χ hχ hc
obtain ⟨hv,hg,hf,hvs,hgs,hfs,hfirst,hsecond⟩ := hcut χ hχ hc
refine ⟨hv,hg,hf,hvs,hgs,hfs,hfirst,hsecond,?_⟩
exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeightedPoissonCoercivity.compact_weak_poisson_weighted_coercivity
(fun z => V ((1/2:ℝ) • (y+z)) + ‖z-y‖^2/(8*η)) hW hI hZ
(((α:ℝ)+1/η)/4) hlower (S y) hSy D hClose hgraph
(fun x => χ x * (u : Lp ℝ 2 (S y)) x)
(fun x => χ x * (ε * (u : Lp ℝ 2 (S y)) x +
inner ℝ (gradient (fun z => V ((1/2:ℝ) • (y+z)) + ‖z-y‖^2/(8*η)) x)
(D.closure u x) - f x) + 2 * inner ℝ (gradient χ x) (D.closure u x) +
(u : Lp ℝ 2 (S y)) x * Laplacian.laplacian χ x)
(fun x => χ x • D.closure u x + (u : Lp ℝ 2 (S y)) x • gradient χ x)
(tsupport χ) hc hvs hfs hgs hv hf hg hfirst hsecond
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactCoercivityScope and omitted-condition boundaries
- Derive genuine compact weighted L2/AE classes vW/GW/AW for actual v/G/(innergradWG-F), same original D.closure graph membership and lambda*normGW^2≤normAW^2 via actual same ordinary-to-weighted smooth sequence. Source fixes originalD before epsilon/f and ONEu before ALLC2chi. No supplied weighted domain/core/convergence/coercivity certificate; no rough classical Hessian or full adjoint/generator-core identity, globalcutoff/tail/Bochner,epsilon0/kernel/range/noncompactlinear/Poincare/BL/jointmeasurablechoice/main/composition. 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.CompactWeightedPoissonCoercivity.compact_weak_poisson_weighted_coercivity
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
- PBPS AppendixC.1 authored analytic prerequisite — Derive genuine compact weighted L2/AE classes vW/GW/AW for actual v/G/(innergradWG-F), same original D.closure graph membership and lambda*normGW^2<=normAW^2 via actual same ordinary-to-weighted smooth sequence. Source fixes originalD before epsilon/f and ONEu before ALLC2chi. No supplied weighted domain/core/convergence/coercivity certificate; no rough classical Hessian or full adjoint/generator-core identity, globalcutoff/tail/Bochner,epsilon0/kernel/range/noncompactlinear/Poincare/BL/jointmeasurablechoice/main/composition. 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.