Samplinglib mathematical lesson

The actual PBPS conditional mean gradient on all of L2

AutoSamplingTheory.ExampleCases.ProximalBPS.RoughMeanGradient.actual_rough_mean_gradient · theorem · Teaching coverage

Read this first

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(Ḡ), ‖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.

\[\forall u\in L^2(\nu):\quad(Tu,Ku)\in\operatorname{graph}(\overline G),\quad Tu(y)=\int u(x)S_y(dx)\ (\nu\text{-a.e.}),\quad\eta\|Ku\|^2\le\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)}\bigl(\|u\|^2-\|Tu\|^2\bigr),\quad4\eta\|Ku\|^2\le\|u\|^2-\|Tu\|^2.\]

Lean statement · actual_rough_mean_gradient

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem 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

Exact module and namespace context

Proof 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 graphḠ; 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 domḠ for every core u. Restrict T to that domain and compose with the actual partial linear map Ḡ: Du=Ḡ(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 graphḠ 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. Ḡ 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.

\[\nu=J_2,\quad\Lambda_1=\Lambda_2=\nu,\quad S\circ\nu=\nu,\quad\overline{\operatorname{dom}G}=L^2(\nu);\qquad u=\varphi\ (\nu\text{-a.e.})\Rightarrow u=\varphi\ (S_y\text{-a.e.},\ \nu\text{-a.e. }y).\]

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 graphḠ; 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.

\[Tu=[T\varphi],\quad(Tu,v)\in\operatorname{graph}(\overline G),\quad\eta\|v\|^2\le c(\|u\|^2-\|Tu\|^2),\qquad c=\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)}.\]

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 domḠ for every core u. Restrict T to that domain and compose with the actual partial linear map Ḡ: Du=Ḡ(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.

\[D:\operatorname{dom}G\to L^2(\nu;E),\quad Du=\overline G(Tu),\quad(Tu,Du)\in\operatorname{graph}(\overline G),\quad\eta\|Du\|^2\le c(\|u\|^2-\|Tu\|^2).\]

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 graphḠ 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.

\[\|Du\|\le\sqrt{c/\eta}\|u\|,\quad K|_{\operatorname{dom}G}=D;\qquad\forall u\in L^2(\nu):\ (Tu,Ku)\in\operatorname{graph}(\overline G),\quad\eta\|Ku\|^2\le c(\|u\|^2-\|Tu\|^2).\]

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.

\[0\le\alpha\eta\le1,\quad0\le c\le\tfrac14,\quad\Delta_u=\|u\|^2-\|Tu\|^2\ge0,\quad\eta\|Ku\|^2\le c\Delta_u\le\tfrac14\Delta_u.\]

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.

\[\eta\|Ku-Kv\|^2\le c\|BM(u-v)\|^2,\quad4\eta\|Ku-Kv\|^2\le\|BM(u-v)\|^2;\qquad\alpha\eta=1\Rightarrow K=0,\ (Tu,0)\in\operatorname{graph}(\overline G).\]

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

Download module (.lean)

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

Exact module and namespace context

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

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.