Actual PBPS reflected resolvent: localized complex Sobolev
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedSobolev.conditional_localized_sobolev · theorem · Teaching coverage
Mathematical statement
Construct genuine common R/S and original fiber D_y before epsilon/f; choose ONE actual u before ALL C2 compact cutoffs. Retain all-domain variational identity, ordinary locally integrable u/G, all C1 compact directional weak-gradient tests, locally integrable squared r=epsilon*u+inner(grad W_y,G)-f, compact-volume L2 of u/G/r and all original C2 compact distribution tests. For every C2 compact chi retain v=chi*u, Gchi=chi*G+u*grad chi, Fchi=chi*r+2 inner(grad chi,G)+u Delta chi, all three global-volume L2/support inclusions, all C1 localized weak-gradient and C2 localized PDE identities with legal products. For each cutoff, Construct actual vc,Fc in complex L2(volume), with vc=volume-a.e. ofReal(v) and Fc=volume-a.e. ofReal(Fchi). For every complex Schwartz psi, both (Delta psi)*ofReal(v) and psi*ofReal(Fchi) are L1 and their integrals equal. For T_v=Lp.toTemperedDistribution(vc) and T_F=Lp.toTemperedDistribution(Fc), derive Delta T_v=T_F and MemSobolev 2 2 T_v. The latter uses B2 T=T-(2pi)^(-2) Delta T and a genuine complex L2 witness, not a supplied regularity result. Reflected/RGO laws/operators/quarter Hessian and Dirichlet scales remain distinct.
Lean statement · conditional_localized_sobolev
Construct genuine common R/S and original fiber D_y before epsilon/f; choose ONE actual u before ALL C2 compact cutoffs. Retain all-domain variational identity, ordinary locally integrable u/G, all C1 compact directional weak-gradient tests, locally integrable squared r=epsilon*u+inner(grad W_y,G)-f, compact-volume L2 of u/G/r and all original C2 compact distribution tests. For every C2 compact chi retain v=chi*u, Gchi=chi*G+u*grad chi, Fchi=chi*r+2 inner(grad chi,G)+u Delta chi, all three global-volume L2/support inclusions, all C1 localized weak-gradient and C2 localized PDE identities with legal products. For each cutoff, Construct actual vc,Fc in complex L2(volume), with vc=volume-a.e. ofReal(v) and Fc=volume-a.e. ofReal(Fchi). For every complex Schwartz psi, both (Delta psi)*ofReal(v) and psi*ofReal(Fchi) are L1 and their integrals equal. For T_v=Lp.toTemperedDistribution(vc) and T_F=Lp.toTemperedDistribution(Fc), derive Delta T_v=T_F and MemSobolev 2 2 T_v. The latter uses B2 T=T-(2pi)^(-2) Delta T and a genuine complex L2 witness, not a supplied regularity result. Reflected/RGO laws/operators/quarter Hessian and Dirichlet 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_sobolev {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) ∧
∃ vc Fc : Lp ℂ 2 (volume : Measure E),
vc =ᵐ[volume] (fun x => (v x : ℂ)) ∧
Fc =ᵐ[volume] (fun x => (Fχ x : ℂ)) ∧
(∀ ψ : SchwartzMap E ℂ,
Integrable (fun x => (Laplacian.laplacian ψ) x * (v x : ℂ)) volume ∧
Integrable (fun x => ψ x * (Fχ x : ℂ)) volume ∧
(∫ x, (Laplacian.laplacian ψ) x * (v x : ℂ)) = ∫ x, ψ x * (Fχ x : ℂ)) ∧
Laplacian.laplacian (Lp.toTemperedDistribution vc) = Lp.toTemperedDistribution Fc ∧
MemSobolev 2 2 (Lp.toTemperedDistribution vc)Proof roadmap
- 1Consume the genuine common reflected conditional localization
Call the accepted actual ConditionalLocalizedResolvent producer with source C2 V and exact curvature/eta cap. Retain common Markov R/S, true augmentation disintegration, reflection and actual positive reflected density; no unreflected RGO operator substitution.
- 2Keep the original D and choose one u before all cutoffs
For each y keep original dense closable exact compact-smooth D_y and closed closure before epsilon/f. The accepted producer returns one actual u with all-domain variational equation, ordinary weak gradient/PDE and local squared/compact L2 facts before every cutoff.
- 3Derive the actual volume L2/support/PDE inputs for each cutoff
Extract formula-defined v/Gchi/Fchi, all three global volume L2/support inclusions and genuine all-C1 first/all-C2 second weak equations from this same u. Keep every property; no Schwartz validity, final TD identity or regularity/core certificate is a new source assumption.
- 4Apply the real-test to complex Sobolev producer
Use K=tsupport chi and actual compactness/support/L2/PDE conclusions to apply the new shared leaf. It constructs actual complex volume classes after each cutoff, every legal complex Schwartz identity, true TD Laplacian and Bessel-Sobolev membership. Fiberwise existences do not assert jointly measurable selectors.
- 5Exercise actual nonquadratic source and compact cutoff
The Test uses V(x)=3x^2/8+sin(x)/8 with genuine curvature[1/2,1], eta in(0,1], an ordinary bump chi with rIn1/rOut2, actual C2 phi=rho(x)(x^2)^(5/2), all true source fibers/epsilon/forcing and originalD. It retains the particular gradient/PDE tests and extracts actual complex classes, all Schwartz integrabilities/equalities, TD equation and Sobolev result for the same cutoff u.
- 6Preserve source scaling and remaining obligations
The reflected potential remains V((y+z)/2)+norm(z-y)^2/(8eta), with quarter Hessian and distinct Dirichlet/epsilon scale from unreflected RGO. This complex regularity prerequisite does not establish real Hessian reps, weighted core/Bochner, BL/Poincare, joint fiber selection, main sampling guarantees or actual-input expected-cost composition.
Full assumptions and notation
All objects and hypotheses
- E has the same finite real Hilbert/Borel/full-space structure including dimension zero. V is C2 with alpha,beta NNReal, 0<alpha≤beta, all-point/all-vector alpha I≤Hess V≤beta I; eta>0 and beta eta≤1.
- Construct the true Gaussian/Gibbs augmentation J, common Markov/disintegrating R/S, exact reflected S_y=(2x-y)#R_y=volume.tilted(-W_y), W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), C2 and positive integrable partition.
- For every fiber fix original dense closable exact compact-smooth gradient D_y with closed closure before epsilon/forcing. For each epsilon>0/f in L2(S_y), one actual u/G/r serves all C2 compact chi. Derive all local/global volume facts and PDE inputs from the accepted actual conditional localization. No measurable joint fiberwise solution/class selector, unreflected RGO identity or localized weighted-domain membership is assumed.
Mathematical proof
1. Consume the genuine common reflected conditional localization
Call the accepted actual ConditionalLocalizedResolvent producer with source C2 V and exact curvature/eta cap. Retain common Markov R/S, true augmentation disintegration, reflection and actual positive reflected density; no unreflected RGO operator substitution.
Corresponding Lean step
ConditionalLocalizedResolvent.conditional_localized_resolvent
2. Keep the original D and choose one u before all cutoffs
For each y keep original dense closable exact compact-smooth D_y and closed closure before epsilon/f. The accepted producer returns one actual u with all-domain variational equation, ordinary weak gradient/PDE and local squared/compact L2 facts before every cutoff.
Corresponding Lean step
hsolve; hDense,hClose,hClosed,hgraph; hu,huL,hGL,hd,hr2,hl,hp
3. Derive the actual volume L2/support/PDE inputs for each cutoff
Extract formula-defined v/Gchi/Fchi, all three global volume L2/support inclusions and genuine all-C1 first/all-C2 second weak equations from this same u. Keep every property; no Schwartz validity, final TD identity or regularity/core certificate is a new source assumption.
Corresponding Lean step
hcut; hv,hg,hf,hvs,hgs,hfs,hfirst,hsecond
4. Apply the real-test to complex Sobolev producer
Use K=tsupport chi and actual compactness/support/L2/PDE conclusions to apply the new shared leaf. It constructs actual complex volume classes after each cutoff, every legal complex Schwartz identity, true TD Laplacian and Bessel-Sobolev membership. Fiberwise existences do not assert jointly measurable selectors.
Corresponding Lean step
CompactWeakPoissonSobolev.compact_weak_poisson_sobolev
5. Exercise actual nonquadratic source and compact cutoff
The Test uses V(x)=3x^2/8+sin(x)/8 with genuine curvature[1/2,1], eta in(0,1], an ordinary bump chi with rIn1/rOut2, actual C2 phi=rho(x)(x^2)^(5/2), all true source fibers/epsilon/forcing and originalD. It retains the particular gradient/PDE tests and extracts actual complex classes, all Schwartz integrabilities/equalities, TD equation and Sobolev result for the same cutoff u.
Corresponding Lean step
Tests.CompactWeakPoissonSobolev.actual_nonconstant_cutoff_sobolev
6. Preserve source scaling and remaining obligations
The reflected potential remains V((y+z)/2)+norm(z-y)^2/(8eta), with quarter Hessian and distinct Dirichlet/epsilon scale from unreflected RGO. This complex regularity prerequisite does not establish real Hessian reps, weighted core/Bochner, BL/Poincare, joint fiber selection, main sampling guarantees or actual-input expected-cost composition.
Corresponding Lean step
conditional_localized_sobolev
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_localized_sobolev
Consume the genuine common reflected conditional localization; Keep the original D and choose one u before all cutoffs; Derive the actual volume L2/support/PDE inputs for each cutoff; Apply the real-test to complex Sobolev producer; Exercise actual nonquadratic source and compact cutoff; Preserve source scaling and remaining 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_sobolev {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) ∧
∃ vc Fc : Lp ℂ 2 (volume : Measure E),
vc =ᵐ[volume] (fun x => (v x : ℂ)) ∧
Fc =ᵐ[volume] (fun x => (Fχ x : ℂ)) ∧
(∀ ψ : SchwartzMap E ℂ,
Integrable (fun x => (Laplacian.laplacian ψ) x * (v x : ℂ)) volume ∧
Integrable (fun x => ψ x * (Fχ x : ℂ)) volume ∧
(∫ x, (Laplacian.laplacian ψ) x * (v x : ℂ)) = ∫ x, ψ x * (Fχ x : ℂ)) ∧
Laplacian.laplacian (Lp.toTemperedDistribution vc) = Lp.toTemperedDistribution Fc ∧
MemSobolev 2 2 (Lp.toTemperedDistribution vc) := by
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
refine ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph,?_⟩
intro ε hε f
obtain ⟨u,hu,huL,hGL,hd,hr2,hl,hp,hcut⟩ := hsolve ε hε f
refine ⟨u,hu,huL,hGL,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.CompactWeakPoissonSobolev.compact_weak_poisson_sobolev
_ _ (tsupport χ) hc hvs hfs hv hf hsecond
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedSobolevSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source Euclidean C2 positive-curvature reflected conditional route. | E has the same finite real Hilbert/Borel/full-space structure including dimension zero. V is C2 with alpha,beta NNReal, 0<alpha<=beta, all-point/all-vector alpha I<=Hess V<=beta I; eta>0 and beta eta<=1. Construct the true Gaussian/Gibbs augmentation J, common Markov/disintegrating R/S, exact reflected S_y=(2x-y)#R_y=volume.tilted(-W_y), W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), C2 and positive integrable partition. For every fiber fix original dense closable exact compact-smooth gradient D_y with closed closure before epsilon/forcing. For each epsilon>0/f in L2(S_y), one actual u/G/r serves all C2 compact chi. Derive all local/global volume facts and PDE inputs from the accepted actual conditional localization. No measurable joint fiberwise solution/class selector, unreflected RGO identity or localized weighted-domain membership is assumed. | source-implicit | Generic real compact-C2 weak Poisson interface, finite Hilbert/Borel/zero dimension, ordinary volume and complex distributions are disclosed; actual source V C2/curvature/eta cap and reflected law unchanged. |
| AppendixC.1 domain extension omits this real-test/Schwartz/Sobolev adapter. | Construct genuine common R/S and original fiber D_y before epsilon/f; choose ONE actual u before ALL C2 compact cutoffs. Retain all-domain variational identity, ordinary locally integrable u/G, all C1 compact directional weak-gradient tests, locally integrable squared r=epsilon*u+inner(grad W_y,G)-f, compact-volume L2 of u/G/r and all original C2 compact distribution tests. For every C2 compact chi retain v=chi*u, Gchi=chi*G+u*grad chi, Fchi=chi*r+2 inner(grad chi,G)+u Delta chi, all three global-volume L2/support inclusions, all C1 localized weak-gradient and C2 localized PDE identities with legal products. For each cutoff, Construct actual vc,Fc in complex L2(volume), with vc=volume-a.e. ofReal(v) and Fc=volume-a.e. ofReal(Fchi). For every complex Schwartz psi, both (Delta psi)*ofReal(v) and psi*ofReal(Fchi) are L1 and their integrals equal. For T_v=Lp.toTemperedDistribution(vc) and T_F=Lp.toTemperedDistribution(Fc), derive Delta T_v=T_F and MemSobolev 2 2 T_v. The latter uses B2 T=T-(2pi)^(-2) Delta T and a genuine complex L2 witness, not a supplied regularity result. Reflected/RGO laws/operators/quarter Hessian and Dirichlet scales remain distinct. | source-implicit | Derive all-Schwartz tests/actual AE-linked L2TD Laplacian and Fourier-normalized Sobolev witness; neither final Schwartz equation nor H2/core certificate supplied. |
| Source Poincare/macroscopic extension and SPHMC4.1 BL covariance bound. | Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer unbounded cost. | unresolved | Complex Bessel-Sobolev alone does not certify real mixed-second reps, original weighted core/Bochner/coercivity, law/operator scale adapter, source full4.1 or main/composition. |
Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer 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
- Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer unbounded cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolvent.conditional_localized_resolventAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeakPoissonSobolev.compact_weak_poisson_sobolev
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
- PBPS AppendixC.1 authored analytic prerequisite — Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer 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.