The actual PBPS conditional mean gradient on all of L2
AutoSamplingTheory.ExampleCases.ProximalBPS.RoughMeanGradient.actual_rough_mean_gradient · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero. Let V:E→ℝ be C2, 0<α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v, η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), ν=J.snd and EVERY-y S_y=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)). Then ν is a probability. There is a densely defined closable real linear gradient G:L²(ν)⇀L²(ν;E), whose graph consists exactly of AE classes (φ,∇φ) for smooth compactly supported φ, and whose closure has closed graph. There are one bounded linear T:L²(ν)→L²(ν) and one bounded linear K:L²(ν)→L²(ν;E), both chosen before all arbitrary rough u∈L²(ν). For every u, (Tu,Ku)∈graph(Ḡ), ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S_y(dx) AE ν, and u,u² are integrable under S_y for AE y. With c=(1−αη)²/[4(1+αη)], η‖Ku‖²≤c(‖u‖²−‖Tu‖²) and 4η‖Ku‖²≤‖u‖²−‖Tu‖². No compactness, centering, extra moment, supplied kernel/operator/domain or convergence certificate is assumed for rough u. This is the closed compact-gradient formulation of the source density/closedness passage and sharp estimate; a separately defined weak-H1 equivalence and full Gamma/B13 identity are not claimed.
Lean statement · actual_rough_mean_gradient
Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero. Let V:E→ℝ be C2, 0<α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v, η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), ν=J.snd and EVERY-y S_y=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)). Then ν is a probability. There is a densely defined closable real linear gradient G:L²(ν)⇀L²(ν;E), whose graph consists exactly of AE classes (φ,∇φ) for smooth compactly supported φ, and whose closure has closed graph. There are one bounded linear T:L²(ν)→L²(ν) and one bounded linear K:L²(ν)→L²(ν;E), both chosen before all arbitrary rough u∈L²(ν). For every u, (Tu,Ku)∈graph(Ḡ), ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S_y(dx) AE ν, and u,u² are integrable under S_y for AE y. With c=(1−αη)²/[4(1+αη)], η‖Ku‖²≤c(‖u‖²−‖Tu‖²) and 4η‖Ku‖²≤‖u‖²−‖Tu‖². No compactness, centering, extra moment, supplied kernel/operator/domain or convergence certificate is assumed for rough u. This is the closed compact-gradient formulation of the source density/closedness passage and sharp estimate; a separately defined weak-H1 equivalence and full Gamma/B13 identity are not 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 actual_rough_mean_gradient
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
(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 := (μ.prod (stdGaussian E)).map
(fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
let ν := J.snd
let S := fun y : E => (volume : Measure E).tilted
(fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))
IsProbabilityMeasure ν ∧
∃ G : Lp ℝ 2 ν →ₗ.[ℝ] Lp E 2 ν,
Dense (G.domain : Set (Lp ℝ 2 ν)) ∧ G.IsClosable ∧ G.closure.IsClosed ∧
(∀ (u : Lp ℝ 2 ν) (v : Lp E 2 ν), (u,v) ∈ G.graph ↔
∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
u =ᵐ[ν] φ ∧ v =ᵐ[ν] gradient φ) ∧
∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
∃ K : Lp ℝ 2 ν →L[ℝ] Lp E 2 ν,
∀ u : Lp ℝ 2 ν,
(T u,K u) ∈ G.closure.graph ∧ ‖T u‖ ≤ ‖u‖ ∧
(T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
(∀ᵐ y ∂ν, Integrable (u : E → ℝ) (S y) ∧
Integrable (fun x => (u x)^2) (S y)) ∧
η*‖K u‖^2 ≤
(1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) * (‖u‖^2-‖T u‖^2) ∧
4*η*‖K u‖^2 ≤ ‖u‖^2-‖T u‖^2Proof roadmap
- 1Use the actual source laws, dense core and bounded mean
The three admitted parents supply the same μ,J,ν: the actual all-L2 source mean T and contraction; a genuine dense closable compact-gradient core G with closed graph closure; and the sharp compact gradient energy. The actual conditional S is stationary under ν because it disintegrates the reflected joint law Λ and both Λ marginals are ν. Thus u=φ AE ν also holds AE S_y for AE y. This fiber fact is derived from the actual stationary law, not assumed by a caller.
- 2Match compact representatives and the sharp energy on the same law
For u in domG take its genuine smooth compact representative φ. The compact parent produces Tf(y)=∫φ dS_y and an actual pair ([Tf],[∇Tf]) in graphḠ; Tf need not be compactly supported. The fiber equality, exact every-y kernel tilt, and AE uniqueness identify Tu=[Tf]. The actual macroscopic energy parent supplies η∫‖∇Tf‖²dν≤c‖Bg‖² for g=φ∘snd, and the real block identity gives ‖Bg‖²=∫φ²dν−∫(Tf)²dν. Canonical L2 norm/integral identities match these exact classes.
- 3Construct a genuine linear derivative on the dense core
The previous step proves Tu belongs to domḠ for every core u. Restrict T to that domain and compose with the actual partial linear map Ḡ: Du=Ḡ(Tu). This is a real linear map on domG. Single-valued graph uniqueness identifies Du with the compact derivative witness, so it retains the sharp estimate. Linearity is derived through the genuine gradient graph, not chosen separately for each observer.
- 4Extend the bounded derivative and preserve graph and sharp defect
Since c≥0 and η>0, the sharp core estimate implies ‖Du‖≤√(c/η)‖u‖. The actual inclusion domG→L²(ν) has dense range; vector L2 is complete. Mathlib extendOfNorm therefore constructs one bounded linear K on full L2 agreeing with D on the core. The preimage of closed graphḠ under u↦(Tu,Ku) is closed, and so is the sharp-inequality set. Density extends both to every rough u. This uses the repaired source prerequisite path core gradient→linear norm bound→bounded extension; no limit or closed-domain premise is imported.
- 5Recover the source coefficient without a singular endpoint division
The original α≤β and βη≤1 give 0≤αη≤1. Hence 0≤c≤1/4. Since T is contractive, Δ=‖u‖²−‖Tu‖²≥0, and η‖Ku‖²≤cΔ≤Δ/4. The literal AE source mean and AE fiber L1/squareL1 are retained from the true all-L2 mean producer. The proof never divides by 1−αη, so the allowed αη=1 endpoint is included.
- 6Exercise the actual joint block and the allowed endpoint
The genuine joint-space Test obtains actual U,M and B=(I−P)UP from the same source mean parent. AE uniqueness of both literal source conditional means identifies the T from this theorem with that parent T. For arbitrary rough u−v, the parent defect and linearity give η‖Ku−Kv‖²≤c‖BM(u−v)‖² and the source4η version; PM(u−v)=M(u−v) and M(Tu−Tv)=PUPM(u−v). A separate endpoint Test uses αη=1 to force the full bounded gradient operator K=0 and retains (Tu,0) in the same closed graph. The endpoint equality is a Test specialization, not an added public theorem premise.
Full assumptions and notation
All objects and hypotheses
- Finite real Hilbert/Borel E and canonical volume; rank zero explicitly extends the source Euclidean presentation.
- V is C2, α>0, α≤β, both global Hessian bounds; η>0 and βη≤1.
- Every u is an arbitrary real square-integrable AE class under actual ν. No centering, compact support, extra moment, pointwise smoothness or caller normalization/operator/domain/convergence premise.
- One G,T,K produced uniformly before u; only AE ν rough mean/fiber integrability. Ḡ is the closure of the exact compact-gradient graph, with no unstated weak-Sobolev convention.
Mathematical proof
1. Use the actual source laws, dense core and bounded mean
The three admitted parents supply the same μ,J,ν: the actual all-L2 source mean T and contraction; a genuine dense closable compact-gradient core G with closed graph closure; and the sharp compact gradient energy. The actual conditional S is stationary under ν because it disintegrates the reflected joint law Λ and both Λ marginals are ν. Thus u=φ AE ν also holds AE S_y for AE y. This fiber fact is derived from the actual stationary law, not assumed by a caller.
Corresponding Lean step
L2MacroscopicMean.actual_macroscopic_l2_mean; SourceMeanGradientDomain.literal_source_mean_in_closed_gradient; MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks; Measure.disintegrate; Measure.ae_ae_of_ae_comp
2. Match compact representatives and the sharp energy on the same law
For u in domG take its genuine smooth compact representative φ. The compact parent produces Tf(y)=∫φ dS_y and an actual pair ([Tf],[∇Tf]) in graphḠ; Tf need not be compactly supported. The fiber equality, exact every-y kernel tilt, and AE uniqueness identify Tu=[Tf]. The actual macroscopic energy parent supplies η∫‖∇Tf‖²dν≤c‖Bg‖² for g=φ∘snd, and the real block identity gives ‖Bg‖²=∫φ²dν−∫(Tf)²dν. Canonical L2 norm/integral identities match these exact classes.
Corresponding Lean step
hCore; hTu; hSame; hUn; hTn′; hGradn; hBlock₁; L2.inner_def; integral_congr_ae
3. Construct a genuine linear derivative on the dense core
The previous step proves Tu belongs to domḠ for every core u. Restrict T to that domain and compose with the actual partial linear map Ḡ: Du=Ḡ(Tu). This is a real linear map on domG. Single-valued graph uniqueness identifies Du with the compact derivative witness, so it retains the sharp estimate. Linearity is derived through the genuine gradient graph, not chosen separately for each observer.
Corresponding Lean step
hDom; q; LinearMap.codRestrict; G.closure.toFun.comp; hDpair; LinearPMap.mem_graph_snd_inj; hDsharp
4. Extend the bounded derivative and preserve graph and sharp defect
Since c≥0 and η>0, the sharp core estimate implies ‖Du‖≤√(c/η)‖u‖. The actual inclusion domG→L²(ν) has dense range; vector L2 is complete. Mathlib extendOfNorm therefore constructs one bounded linear K on full L2 agreeing with D on the core. The preimage of closed graphḠ under u↦(Tu,Ku) is closed, and so is the sharp-inequality set. Density extends both to every rough u. This uses the repaired source prerequisite path core gradient→linear norm bound→bounded extension; no limit or closed-domain premise is imported.
Corresponding Lean step
hNormBound; hRange; LinearMap.extendOfNorm; LinearMap.extendOfNorm_eq; hPairAll; hSharpAll; Dense.induction; isClosed_le
5. Recover the source coefficient without a singular endpoint division
The original α≤β and βη≤1 give 0≤αη≤1. Hence 0≤c≤1/4. Since T is contractive, Δ=‖u‖²−‖Tu‖²≥0, and η‖Ku‖²≤cΔ≤Δ/4. The literal AE source mean and AE fiber L1/squareL1 are retained from the true all-L2 mean producer. The proof never divides by 1−αη, so the allowed αη=1 endpoint is included.
Corresponding Lean step
haη; haη1; hcCap; hNonneg; hSharpAll; hAll; hSd
6. Exercise the actual joint block and the allowed endpoint
The genuine joint-space Test obtains actual U,M and B=(I−P)UP from the same source mean parent. AE uniqueness of both literal source conditional means identifies the T from this theorem with that parent T. For arbitrary rough u−v, the parent defect and linearity give η‖Ku−Kv‖²≤c‖BM(u−v)‖² and the source4η version; PM(u−v)=M(u−v) and M(Tu−Tv)=PUPM(u−v). A separate endpoint Test uses αη=1 to force the full bounded gradient operator K=0 and retains (Tu,0) in the same closed graph. The endpoint equality is a Test specialization, not an added public theorem premise.
Corresponding Lean step
Tests.ProximalBPSRoughMeanGradient.actual_joint_block_rough_difference; actual_sharp_endpoint_zero_gradient
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_rough_mean_gradient
Use the actual source laws, dense core and bounded mean; Match compact representatives and the sharp energy on the same law; Construct a genuine linear derivative on the dense core; Extend the bounded derivative and preserve graph and sharp defect; Recover the source coefficient without a singular endpoint division; Exercise the actual joint block and the allowed endpoint
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 actual_rough_mean_gradient
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
(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 := (μ.prod (stdGaussian E)).map
(fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
let ν := J.snd
let S := fun y : E => (volume : Measure E).tilted
(fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))
IsProbabilityMeasure ν ∧
∃ G : Lp ℝ 2 ν →ₗ.[ℝ] Lp E 2 ν,
Dense (G.domain : Set (Lp ℝ 2 ν)) ∧ G.IsClosable ∧ G.closure.IsClosed ∧
(∀ (u : Lp ℝ 2 ν) (v : Lp E 2 ν), (u,v) ∈ G.graph ↔
∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
u =ᵐ[ν] φ ∧ v =ᵐ[ν] gradient φ) ∧
∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
∃ K : Lp ℝ 2 ν →L[ℝ] Lp E 2 ν,
∀ u : Lp ℝ 2 ν,
(T u,K u) ∈ G.closure.graph ∧ ‖T u‖ ≤ ‖u‖ ∧
(T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
(∀ᵐ y ∂ν, Integrable (u : E → ℝ) (S y) ∧
Integrable (fun x => (u x)^2) (S y)) ∧
η*‖K u‖^2 ≤
(1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) * (‖u‖^2-‖T u‖^2) ∧
4*η*‖K u‖^2 ≤ ‖u‖^2-‖T u‖^2 := by
classical
dsimp only
let μ := (volume : Measure E).tilted (fun x => -V x)
let J := (μ.prod (stdGaussian E)).map
(fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
let ν := J.snd
let S := fun y : E => (volume : Measure E).tilted
(fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))
let c := (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η))
obtain ⟨hμ,hJ,hν,S₀,hS₀,hSd,hSc,hSf,hSs,U,hU,hUi,hUs,M,hM,T,hAll⟩ :=
L2MacroscopicMean.actual_macroscopic_l2_mean hα hαβ hV hH hη hβη
let : IsProbabilityMeasure μ := hμ
let : IsProbabilityMeasure J := hJ
let : IsProbabilityMeasure ν := hν
let : IsMarkovKernel S₀ := hS₀
let Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
let : Λ.IsCondKernel S₀ := hSc
have hstation : S₀ ∘ₘ ν = ν := by
rw [← Measure.snd_compProd]
have hc : ν ⊗ₘ S₀ = Λ := by
have hfirst : Λ.fst = ν := hSf
rw [← hfirst]
exact Measure.disintegrate Λ S₀
rw [hc]
exact hSs
obtain ⟨_,G,hDense,hClose,hClosed,hGraph,hMean⟩ :=
SourceMeanGradientDomain.literal_source_mean_in_closed_gradient hα hαβ hV hH hη hβη
obtain ⟨_,_,_,R₁,S₁,hR₁,hS₁,hRc₁,hSr₁,hSd₁,hSc₁,hSf₁,
U₁,hU₁,hUi₁,hUs₁,hBB₁,hBD₁,hBlock₁,hEnergy⟩ :=
MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks hα hαβ hV hH hη hβη
have hn (u : Lp ℝ 2 ν) : ‖u‖^2 = ∫ y, (u y)^2 ∂ν := by
rw [← real_inner_self_eq_norm_sq, L2.inner_def]
simp only [real_inner_self_eq_norm_sq,Real.norm_eq_abs,sq_abs]
have hnE (v : Lp E 2 ν) : ‖v‖^2 = ∫ y, ‖v y‖^2 ∂ν := by
rw [← real_inner_self_eq_norm_sq,L2.inner_def]
simp only [real_inner_self_eq_norm_sq]
have hFiberEq (u : Lp ℝ 2 ν) (f : E → ℝ) (hf : u =ᵐ[ν] f) :
∀ᵐ y ∂ν, (u : E → ℝ) =ᵐ[S₀ y] f := by
have hcomp : (u : E → ℝ) =ᵐ[S₀ ∘ₘ ν] f := by rw [hstation]; exact hf
exact Measure.ae_ae_of_ae_comp hcomp
have hCore (u : G.domain) :
∃ v : Lp E 2 ν, (T u,v) ∈ G.closure.graph ∧
η*‖v‖^2 ≤ c*(‖(u : Lp ℝ 2 ν)‖^2-‖T u‖^2) := by
obtain ⟨f,hf,hfc,huf,_⟩ := (hGraph u (G u)).mp (G.mem_graph u)
let Tf := fun y : E => ∫ x, f x ∂S y
obtain ⟨hTf,hGrad,hPair⟩ := hMean f hf hfc
obtain ⟨_,_,hTn,hSource,hFib,_,_,_⟩ := hAll u
have hTu : T u = hTf.toLp Tf := by
apply Lp.ext
filter_upwards [hSource,hFiberEq u f huf,hTf.coeFn_toLp] with y hy heq ht
exact hy.trans ((integral_congr_ae heq).trans
((congrArg (fun m : Measure E => ∫ x, f x ∂m) (hSd y)).trans ht.symm))
obtain ⟨_,_,_,_,_,g,hg,hPg,hAg,hgn,hAgn,hvb,hSharp⟩ := hEnergy f hf hfc
have hSame : (fun y : E => ∫ x, f x ∂S₁ y) = Tf := by
funext y
exact congrArg (fun m : Measure E => ∫ x, f x ∂m) (hSd₁ y)
have hUn : ‖(u : Lp ℝ 2 ν)‖^2 = ∫ y, (f y)^2 ∂ν := by
rw [hn]
exact integral_congr_ae (Filter.EventuallyEq.fun_comp huf (fun t : ℝ => t^2))
have hTn' : ‖T u‖^2 = ∫ y, (Tf y)^2 ∂ν := by
rw [hTu,hn]
exact integral_congr_ae (Filter.EventuallyEq.fun_comp hTf.coeFn_toLp (fun t : ℝ => t^2))
have hGradn : ‖hGrad.toLp (gradient Tf)‖^2 = ∫ y, ‖gradient Tf y‖^2 ∂ν := by
rw [hnE]
exact integral_congr_ae (Filter.EventuallyEq.fun_comp hGrad.coeFn_toLp (fun t : E => ‖t‖^2))
have hDef := hBlock₁ g hPg
rw [hDef,hgn,hAgn] at hSharp
rw [hSame] at hSharp
refine ⟨hGrad.toLp (gradient Tf),?_,?_⟩
· rw [hTu]
exact hPair
· rw [hGradn,hUn,hTn']
exact hSharp
have hDom (u : G.domain) : T u ∈ G.closure.domain :=
G.closure.mem_domain_of_mem_graph (hCore u).choose_spec.1
let q : G.domain →ₗ[ℝ] G.closure.domain :=
(T.toLinearMap.comp G.domain.subtype).codRestrict G.closure.domain hDom
let D : G.domain →ₗ[ℝ] Lp E 2 ν := G.closure.toFun.comp q
have hDpair (u : G.domain) : (T u,D u) ∈ G.closure.graph :=
G.closure.mem_graph (q u)
have hDsharp (u : G.domain) :
η*‖D u‖^2 ≤ c*(‖(u : Lp ℝ 2 ν)‖^2-‖T u‖^2) := by
obtain ⟨v,hv,hvSharp⟩ := hCore u
have hDv : D u = v := G.closure.mem_graph_snd_inj (hDpair u) hv rfl
rw [hDv]
exact hvSharp
have hc : 0 ≤ c := div_nonneg (sq_nonneg _) (by positivity)
have hNormBound (u : G.domain) : ‖D u‖ ≤ Real.sqrt (c/η)*‖(u : Lp ℝ 2 ν)‖ := by
have hSq : ‖D u‖^2 ≤ (c/η)*‖(u : Lp ℝ 2 ν)‖^2 := by
calc
‖D u‖^2 ≤ (c*‖(u : Lp ℝ 2 ν)‖^2)/η := (le_div_iff₀ hη).mpr (by
have he := hDsharp u
have he' := mul_nonneg hc (sq_nonneg ‖T u‖)
nlinarith)
_ = (c/η)*‖(u : Lp ℝ 2 ν)‖^2 := by ring
apply (sq_le_sq₀ (norm_nonneg _) (mul_nonneg (Real.sqrt_nonneg _) (norm_nonneg _))).mp
rw [mul_pow,Real.sq_sqrt (div_nonneg hc hη.le)]
exact hSq
have hRange : DenseRange (G.domain.subtype : G.domain →ₗ[ℝ] Lp ℝ 2 ν) := by
change Dense (Set.range (Subtype.val : G.domain → Lp ℝ 2 ν))
have hr : Set.range (Subtype.val : G.domain → Lp ℝ 2 ν) =
(G.domain : Set (Lp ℝ 2 ν)) := by
ext x
constructor
· rintro ⟨v,rfl⟩
exact v.property
· intro hx
exact ⟨⟨x,hx⟩,rfl⟩
rw [hr]
exact hDense
let K : Lp ℝ 2 ν →L[ℝ] Lp E 2 ν := D.extendOfNorm G.domain.subtype
have hKcore (u : G.domain) : K u = D u :=
LinearMap.extendOfNorm_eq hRange ⟨Real.sqrt (c/η),hNormBound⟩ u
have hPairAll (u : Lp ℝ 2 ν) : (T u,K u) ∈ G.closure.graph := by
exact hDense.induction (P := fun v => (T v,K v) ∈ G.closure.graph)
(fun v hv => by rw [hKcore ⟨v,hv⟩]; exact hDpair ⟨v,hv⟩)
(hClosed.preimage (T.continuous.prodMk K.continuous)) u
have hSharpAll (u : Lp ℝ 2 ν) :
η*‖K u‖^2 ≤ c*(‖u‖^2-‖T u‖^2) := by
exact hDense.induction (P := fun v => η*‖K v‖^2 ≤ c*(‖v‖^2-‖T v‖^2))
(fun v hv => by rw [hKcore ⟨v,hv⟩]; exact hDsharp ⟨v,hv⟩)
(isClosed_le (by fun_prop) (by fun_prop)) u
have haη : 0 ≤ (α : ℝ)*η := mul_nonneg hα.le hη.le
have haη1 : (α : ℝ)*η ≤ 1 := le_trans
(mul_le_mul_of_nonneg_right (show (α : ℝ) ≤ (β : ℝ) from by exact_mod_cast hαβ) hη.le) hβη
have hcCap : c ≤ 1/4 := by
dsimp only [c]
apply (div_le_iff₀ (by positivity : 0 < 4*(1+(α : ℝ)*η))).mpr
nlinarith [mul_nonneg haη (show 0 ≤ 1-(α : ℝ)*η by linarith)]
refine ⟨hν,G,hDense,hClose,hClosed,hGraph,T,K,?_⟩
intro u
obtain ⟨_,_,hTn,hSource,hFib,_,_,_⟩ := hAll u
have hNonneg : 0 ≤ ‖u‖^2-‖T u‖^2 := by
have hs := (sq_le_sq₀ (norm_nonneg (T u)) (norm_nonneg u)).mpr hTn
linarith
refine ⟨hPairAll u,hTn,?_,?_,hSharpAll u,?_⟩
· filter_upwards [hSource] with y hy
exact hy.trans (congrArg (fun m : Measure E => ∫ x, u x ∂m) (hSd y))
· filter_upwards [hFib] with y hy
simpa only [hSd y] using hy
· have hSharp := hSharpAll u
have hCap := mul_le_mul_of_nonneg_right hcCap hNonneg
nlinarith
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.RoughMeanGradientSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Original C2 potential, both positive α≤β Hessian bounds, η>0 and βη≤1. | Exact source hypotheses retained; finite real Hilbert/Borel/rank0 explicitly extends Euclidean presentation. | same | No extra regularity, centering, compact input, moment, kernel/operator/domain/convergence premise. |
| C.1 genuine dense compact-gradient core and closure; C.2 rough conditional mean-gradient and sharp norm defect. | SAME actual mu/J/nu and EVERY-y literal source S; one dense closable genuine compact-gradient core G, one actual bounded T and one bounded K chosen BEFORE every u in full L2(nu). T is the AE source conditional mean; (T u,K u) lies in G.closure.graph; sharp coefficient c=(1-alpha*eta)^2/[4(1+alpha*eta)] and source4eta inequality. | same | Actual graph semantics advertised explicitly and all same-law core/mean/energy and bounded extension constructed internally. |
| Rough conditional means and fiber integrability are only AE; density/closedness passage concerns gradient closure. | Every-y literal S law, AE source mean/fiber L1/squareL1, actual compact-gradient closure image for all rough inputs. | same | No every-y rough smoothness or identification with an arbitrary Sobolev convention inferred. |
| Weak-H1 identification/full B13 Gamma norm identity and algorithm/main results. | One genuine dense closable compact-gradient G, one bounded actual conditional mean T and one bounded vector-L2 gradient K are chosen before all rough L2(ν) inputs. (Tu,Ku) lies in the actual closed compact-gradient graph; the sharp c=(1−αη)²/[4(1+αη)] norm defect and source4η bound hold. Original C2/two Hessian bounds/positive capped step retained. Finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Every-y literal kernel law is distinct from AE rough mean/fiber L1 and squareL1. Separately defined weak-H1 equivalence, full B13/Gamma/dynamics/main/error/cost/composition remain open. | unresolved | Source closed-gradient formulation and sharp defect provide a genuine consumer edge. Separate weak-H1/Gamma/dynamics/errors/cost/composition remain open. |
One genuine dense closable compact-gradient G, one bounded actual conditional mean T and one bounded vector-L2 gradient K are chosen before all rough L2(ν) inputs. (Tu,Ku) lies in the actual closed compact-gradient graph; the sharp c=(1−αη)²/[4(1+αη)] norm defect and source4η bound hold. Original C2/two Hessian bounds/positive capped step retained. Finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Every-y literal kernel law is distinct from AE rough mean/fiber L1 and squareL1. Separately defined weak-H1 equivalence, full B13/Gamma/dynamics/main/error/cost/composition remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: Finite real Hilbert/Borel including rank0 extends the printed Euclidean presentation explicitly. — Independent source review classification: explicit-attributed-background-extension; nonblocking.
- scopes: Accepted exact graph-closure all-L2 image and sharp defect; weak-H1 equivalence and full B13/Gamma are outside this declaration, not silently discharged. — Independent source review classification: explicit-scoped-authored-integration; nonblocking.
- objects: Candidate S_y is source p_y; source residual S_source=U_perpP is realized by genuine joint B M u. — Independent source review classification: notation-resolution; nonblocking.
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
- One genuine dense closable compact-gradient G, one bounded actual conditional mean T and one bounded vector-L2 gradient K are chosen before all rough L2(ν) inputs. (Tu,Ku) lies in the actual closed compact-gradient graph; the sharp c=(1−αη)²/[4(1+αη)] norm defect and source4η bound hold. Original C2/two Hessian bounds/positive capped step retained. Finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Every-y literal kernel law is distinct from AE rough mean/fiber L1 and squareL1. Separately defined weak-H1 equivalence, full B13/Gamma/dynamics/main/error/cost/composition remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.SourceMeanGradientDomain.literal_source_mean_in_closed_gradientAutoSamplingTheory.ExampleCases.ProximalBPS.L2MacroscopicMean.actual_macroscopic_l2_meanAutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks
Mathlib API called (external library)
- Measure.disintegrate
- Measure.ae_ae_of_ae_comp
- Lp.ext
- L2.inner_def
- LinearMap.codRestrict
- LinearPMap.mem_graph_snd_inj
- LinearMap.extendOfNorm
- LinearMap.extendOfNorm_eq
- Dense.induction
- isClosed_le
Mathematical sources
- Fixed PBPS2609.06905v1 C.1 density/closedness passage and C.2 sharp compact estimate toward B.13; actual rough-input conditional mean in the SAME canonical closed-gradient graph and sharp energy estimate. Source C2/two Hessian/positive capped eta retained. — One genuine dense closable compact-gradient G, one bounded actual conditional mean T and one bounded vector-L2 gradient K are chosen before all rough L2(ν) inputs. (Tu,Ku) lies in the actual closed compact-gradient graph; the sharp c=(1−αη)²/[4(1+αη)] norm defect and source4η bound hold. Original C2/two Hessian bounds/positive capped step retained. Finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Every-y literal kernel law is distinct from AE rough mean/fiber L1 and squareL1. Separately defined weak-H1 equivalence, full B13/Gamma/dynamics/main/error/cost/composition remain open.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.