Actual PBPS reflected resolvent: common compact smooth graph
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactSmoothGraph.conditional_compact_smooth_graph · theorem · Teaching coverage
Mathematical statement
Construct common R/S; for each y fix original D_y before epsilon/f, choose ONE u before ALL C2 compact chi. Retain original exact D graph, dense/closable/closed properties, all-domain positive-epsilon variational identity, ordinary locally integrable u/G, all-C1 compact directional weak-gradient identities, local squared-r integrability, compact-volumeL2 of u/G/r, original all-C2 PDE, and all actual localized volumeL2/support/first/second weak identities. The actual volumeL2 properties are retained; actual vL/FL/gradL quotient classes are returned with all three AE links and bind the simultaneous limits. For each cutoff apply the shared actual producer: Derive one real Schwartz sequence phi_n with one common outer compact Kprime containing every tsupport(phi_n), chosen before all n and all three limits. Actual volumeL2 classes of phi_n converge to v; actual classical gradient(phi_n) is MemLp2 and its class converges to the actual Gchi; actual Laplacian(phi_n) classes converge to Fchi. Every phi_n is C-infinity and compactly supported. The same sequence realizes all limits. Kprime need not equal K. No classical derivatives of rough v, real Hessian family, quantitative source complexity constant or weighted operator core is claimed.
Lean statement · conditional_compact_smooth_graph
Construct common R/S; for each y fix original D_y before epsilon/f, choose ONE u before ALL C2 compact chi. Retain original exact D graph, dense/closable/closed properties, all-domain positive-epsilon variational identity, ordinary locally integrable u/G, all-C1 compact directional weak-gradient identities, local squared-r integrability, compact-volumeL2 of u/G/r, original all-C2 PDE, and all actual localized volumeL2/support/first/second weak identities. The actual volumeL2 properties are retained; actual vL/FL/gradL quotient classes are returned with all three AE links and bind the simultaneous limits. For each cutoff apply the shared actual producer: Derive one real Schwartz sequence phi_n with one common outer compact Kprime containing every tsupport(phi_n), chosen before all n and all three limits. Actual volumeL2 classes of phi_n converge to v; actual classical gradient(phi_n) is MemLp2 and its class converges to the actual Gchi; actual Laplacian(phi_n) classes converge to Fchi. Every phi_n is C-infinity and compactly supported. The same sequence realizes all limits. Kprime need not equal K. No classical derivatives of rough v, real Hessian family, quantitative source complexity constant or weighted operator core is claimed.
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_smooth_graph {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) ∧
∃ vL FL : Lp ℝ 2 (volume : Measure E), ∃ gradL : Lp E 2 (volume : Measure E),
vL =ᵐ[volume] v ∧ FL =ᵐ[volume] Fχ ∧ gradL =ᵐ[volume] Gχ ∧
∃ K' : Set E, IsCompact K' ∧ ∃ φ : ℕ → SchwartzMap E ℝ,
(∀ n : ℕ, tsupport (φ n) ⊆ K') ∧
Filter.Tendsto (fun n : ℕ => (φ n).toLp 2 volume) Filter.atTop (𝓝 vL) ∧
∃ hφG : ∀ n : ℕ, MemLp (gradient (φ n : E → ℝ)) 2 volume,
Filter.Tendsto (fun n : ℕ => (hφG n).toLp (gradient (φ n : E → ℝ)))
Filter.atTop (𝓝 gradL) ∧
Filter.Tendsto (fun n : ℕ => (Laplacian.laplacian (φ n)).toLp 2 volume)
Filter.atTop (𝓝 FL)Proof roadmap
- 1Keep true augmentation and reflected source law
Consume ConditionalLocalizedResolvent with exact C2 curvature/eta-cap inputs. Retain actual common Markov/disintegrating kernels, reflection, C2 reflected potential and positive integrable partition; no RGO operator substitution.
- 2Keep original D before epsilon/f and one u before all chi
Preserve the actual dense closable original compact-smooth graph and closed closure. Extract ONE actual positive-epsilon resolvent u with all-domain variational and original ordinary weak/local facts before ALL real C2 compact cutoffs.
- 3Derive the real localized graph inputs from this same u
Extract all three true volumeL2 proofs and support inclusions plus all-C1 weak-gradient and all-C2 weakPoisson identities for actual v/Gchi/Fchi. Actual vL/FL/gradL quotient classes with AE links bind the limits; they add no mathematical premise.
- 4Construct the actual common compact smooth sequence
Apply the new shared producer at K=tsupport chi and every genuinely derived input. It constructs one real smooth sequence/common outer compact and all three ordinary-volume limits; source does not supply a graph-density or final approximation certificate.
- 5Exercise source consumer with a nonquadratic potential and non-smooth-all-orders cutoff
The Test uses V(x)=3x^2/8+sin(x)/8, curvature[1/2,1], eta in(0,1], true commonR/S/originalD/all epsilon/f. Its compact cutoff rho(x)*(x^2)^(5/2) is certified C2 and need not be C-infinity; extract the actual same-u localized equations and all three same-sequence limits from this consumer.
- 6Keep the original truth boundary
Approximation is ordinary volume on each fixed compact localization. No jointly measurable fiberwise sequence selector, weighted original D-domain/core, unlocalized generator/Bochner, BL/Poincare or full main/composition is inferred. TV proximity does not transfer unbounded expected cost.
Full assumptions and notation
All objects and hypotheses
- Same finite real Hilbert/Borel/canonical-volume structure including dimension zero. V is C2, alpha/beta NNReal, 0<alpha≤beta, all-point/all-vector alpha I≤Hess V≤beta I; eta>0 and beta*eta≤1.
- True augmentation J=(x,x+sqrt(eta)*xi)#(mu*standardGaussian), common actual disintegrating probability kernels R/S, S_y=(2x-y)#R_y=volume.tilted(-W_y), W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), and actual positive integrable partitions are derived from accepted parents. Reflected/RGO laws/operators and quarter Hessian/fourfold Dirichlet scaling remain distinct.
- Original dense closable compact-smooth gradient D_y with closed closure is fixed before epsilon/forcing. For every epsilon>0 and f in L2(S_y), choose ONE actual u before ALL C2 compact cutoffs chi. Derive the actual v=chi*u, Gchi=chi*D.closure(u)+u*gradientchi and Fchi=chi*r+2inner(gradientchi,D.closure(u))+u*Deltachi, r=epsilon*u+inner(gradientW,D.closure(u))-f; all required volumeL2/support/weak equations are genuine parent conclusions.
Mathematical proof
1. Keep true augmentation and reflected source law
Consume ConditionalLocalizedResolvent with exact C2 curvature/eta-cap inputs. Retain actual common Markov/disintegrating kernels, reflection, C2 reflected potential and positive integrable partition; no RGO operator substitution.
Corresponding Lean step
ConditionalLocalizedResolvent.conditional_localized_resolvent
2. Keep original D before epsilon/f and one u before all chi
Preserve the actual dense closable original compact-smooth graph and closed closure. Extract ONE actual positive-epsilon resolvent u with all-domain variational and original ordinary weak/local facts before ALL real C2 compact cutoffs.
Corresponding Lean step
hsolve; hu,huL,hGL,hd,hr2,hl,hp
3. Derive the real localized graph inputs from this same u
Extract all three true volumeL2 proofs and support inclusions plus all-C1 weak-gradient and all-C2 weakPoisson identities for actual v/Gchi/Fchi. Actual vL/FL/gradL quotient classes with AE links bind the limits; they add no mathematical premise.
Corresponding Lean step
hcut; hv,hg,hf,hvs,hgs,hfs,hfirst,hsecond; vL/FL/gradL with AE links
4. Construct the actual common compact smooth sequence
Apply the new shared producer at K=tsupport chi and every genuinely derived input. It constructs one real smooth sequence/common outer compact and all three ordinary-volume limits; source does not supply a graph-density or final approximation certificate.
Corresponding Lean step
CompactPoissonSmoothGraph.compact_weak_poisson_smooth_graph_approximation
5. Exercise source consumer with a nonquadratic potential and non-smooth-all-orders cutoff
The Test uses V(x)=3x^2/8+sin(x)/8, curvature[1/2,1], eta in(0,1], true commonR/S/originalD/all epsilon/f. Its compact cutoff rho(x)*(x^2)^(5/2) is certified C2 and need not be C-infinity; extract the actual same-u localized equations and all three same-sequence limits from this consumer.
Corresponding Lean step
Tests.CompactPoissonSmoothGraph.actual_c2_cutoff_smooth_graph
6. Keep the original truth boundary
Approximation is ordinary volume on each fixed compact localization. No jointly measurable fiberwise sequence selector, weighted original D-domain/core, unlocalized generator/Bochner, BL/Poincare or full main/composition is inferred. TV proximity does not transfer unbounded expected cost.
Corresponding Lean step
conditional_compact_smooth_graph
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_compact_smooth_graph
Keep true augmentation and reflected source law; Keep original D before epsilon/f and one u before all chi; Derive the real localized graph inputs from this same u; Construct the actual common compact smooth sequence; Exercise source consumer with a nonquadratic potential and non-smooth-all-orders cutoff; Keep the original truth 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_compact_smooth_graph {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) ∧
∃ vL FL : Lp ℝ 2 (volume : Measure E), ∃ gradL : Lp E 2 (volume : Measure E),
vL =ᵐ[volume] v ∧ FL =ᵐ[volume] Fχ ∧ gradL =ᵐ[volume] Gχ ∧
∃ K' : Set E, IsCompact K' ∧ ∃ φ : ℕ → SchwartzMap E ℝ,
(∀ n : ℕ, tsupport (φ n) ⊆ K') ∧
Filter.Tendsto (fun n : ℕ => (φ n).toLp 2 volume) Filter.atTop (𝓝 vL) ∧
∃ hφG : ∀ n : ℕ, MemLp (gradient (φ n : E → ℝ)) 2 volume,
Filter.Tendsto (fun n : ℕ => (hφG n).toLp (gradient (φ n : E → ℝ)))
Filter.atTop (𝓝 gradL) ∧
Filter.Tendsto (fun n : ℕ => (Laplacian.laplacian (φ n)).toLp 2 volume)
Filter.atTop (𝓝 FL) := 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,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,?_⟩
obtain ⟨K',hK',φ,hφs,hφv,hφG,hφgrad,hφF⟩ :=
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactPoissonSmoothGraph.compact_weak_poisson_smooth_graph_approximation
(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
exact ⟨hv.toLp _,hf.toLp _,hg.toLp _,hv.coeFn_toLp,hf.coeFn_toLp,hg.coeFn_toLp,
K',hK',φ,hφs,hφv,hφG,hφgrad,hφF⟩
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactSmoothGraphSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source C2 curvature-bounded reflected conditional route. | Same finite real Hilbert/Borel/canonical-volume structure including dimension zero. V is C2, alpha/beta NNReal, 0<alpha<=beta, all-point/all-vector alpha I<=Hess V<=beta I; eta>0 and beta*eta<=1. True augmentation J=(x,x+sqrt(eta)*xi)#(mu*standardGaussian), common actual disintegrating probability kernels R/S, S_y=(2x-y)#R_y=volume.tilted(-W_y), W_y(z)=V((y+z)/2)+norm(z-y)^2/(8eta), and actual positive integrable partitions are derived from accepted parents. Reflected/RGO laws/operators and quarter Hessian/fourfold Dirichlet scaling remain distinct. Original dense closable compact-smooth gradient D_y with closed closure is fixed before epsilon/forcing. For every epsilon>0 and f in L2(S_y), choose ONE actual u before ALL C2 compact cutoffs chi. Derive the actual v=chi*u, Gchi=chi*D.closure(u)+u*gradientchi and Fchi=chi*r+2inner(gradientchi,D.closure(u))+u*Deltachi, r=epsilon*u+inner(gradientW,D.closure(u))-f; all required volumeL2/support/weak equations are genuine parent conclusions. | source-implicit | Generic weak-gradient/PDE compact graph interface is disclosed; actual source V C2/curvature/eta and reflected law/ordinary volume retained including zero dimension. |
| Smooth-test/density analytic details omitted in AppendixC.1; no Laplacian graph sequence supplied. | Construct common R/S; for each y fix original D_y before epsilon/f, choose ONE u before ALL C2 compact chi. Retain original exact D graph, dense/closable/closed properties, all-domain positive-epsilon variational identity, ordinary locally integrable u/G, all-C1 compact directional weak-gradient identities, local squared-r integrability, compact-volumeL2 of u/G/r, original all-C2 PDE, and all actual localized volumeL2/support/first/second weak identities. The actual volumeL2 properties are retained; actual vL/FL/gradL quotient classes are returned with all three AE links and bind the simultaneous limits. For each cutoff apply the shared actual producer: Derive one real Schwartz sequence phi_n with one common outer compact Kprime containing every tsupport(phi_n), chosen before all n and all three limits. Actual volumeL2 classes of phi_n converge to v; actual classical gradient(phi_n) is MemLp2 and its class converges to the actual Gchi; actual Laplacian(phi_n) classes converge to Fchi. Every phi_n is C-infinity and compactly supported. The same sequence realizes all limits. Kprime need not equal K. No classical derivatives of rough v, real Hessian family, quantitative source complexity constant or weighted operator core is claimed. | source-implicit | Derive actual Bessel witness, chosen continuous spectral maps, original real-gradient identification and one common compact triple-limit sequence; no final approximation/core certificate assumed. |
| Poincare/macroscopic extension and SPHMC4.1 BL covariance bound. | Derive one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chi*u, g=chi*G+u*gradientchi, F=chi*r+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; TV never transfers unbounded cost. | unresolved | Fixed compact ordinary-volume graph approximation does not establish weighted generator domain/core, global cutoff removal/Bochner, epsilon0, source full4.1 or either main/composition. |
Derive one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chi*u, g=chi*G+u*gradientchi, F=chi*r+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; 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
- Derive one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chi*u, g=chi*G+u*gradientchi, F=chi*r+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; TV never transfers unbounded cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolvent.conditional_localized_resolventAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactPoissonSmoothGraph.compact_weak_poisson_smooth_graph_approximation
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
- PBPS AppendixC.1 authored analytic prerequisite — Derive one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chi*u, g=chi*G+u*gradientchi, F=chi*r+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; 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.