Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Exact centered squared-defect coercivity and bounded inverse

Attributed ASTIS background completion/consumer of Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang Appendix B/D. This is a scoped squared-defect result; it is not the printed Γ theorem or a main mixing theorem.

arXiv:2609.06905v1; Lean4.33.0/fixedMathlib · PBPS2609.06905v1 AppendixB B1-B5, D1-D2 real L2 stationarity/centering, C4/B15 squared-defect precursor; exact31regions/54items source inventory independently covered. · faithful paraphrase

Complete source statement (Samplinglib restatement)

E is a finite-dimensional real Hilbert Borel space with canonical volume; rank zero is an explicit extension of the source Euclidean convention. V:E→ℝ is C²; 0<α≤β; α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v; η>0 and βη≤1. μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), and ν=J.snd. Finite dimensionality of E does not imply finite dimensionality of L²(ν). There exist a selfadjoint bounded operator T on L²(ν) with the literal ν-a.e. action Tu(y)=∫u(x)S(y,dx), where S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); a class q=1 ν-a.e. with ⟨q,u⟩=∫u dν for all u; and the actual selfadjoint restriction T₀ to H₀=ker⟨q,·⟩. Set ρ=(1−αη)/(1+αη) and δ=4αη/(1+αη)². The squared defect D₀=I_H₀−T₀² is positive. For every u∈H₀, T₀u=Tu as an ambient class, ‖T₀u‖≤ρ‖u‖, ⟨D₀u,u⟩=‖u‖²−‖T₀u‖² and δ‖u‖²≤⟨D₀u,u⟩. D₀ is a unit in the algebra of bounded continuous linear endomorphisms of H₀; hence it has a bounded inverse on this exact centered space. The original hypotheses force δ>0 and include αη=1. No full-space inverse or positive square root is claimed.

  • The complete potential, curvature, initialization law and step conditions are stated above. No operator, probability, stationarity, mean-zero preservation or coercivity certificate is supplied by the caller.
  • L² consists of AE classes; finite dimension of E does not make L² finite dimensional. The whole closed mean-zero subspace is used.
  • Zero-dimensional E is explicitly included as an extension of the source Euclidean convention; αη=1 is retained.

Exact centered squared-defect coercivity and bounded inverse

\[\rho=\frac{1-\alpha\eta}{1+\alpha\eta},\quad\delta=\frac{4\alpha\eta}{(1+\alpha\eta)^2}>0,\quad\|T_0u\|\le\rho\|u\|,\quad\langle D_0u,u\rangle\ge\delta\|u\|^2,\quad D_0\in\operatorname{GL}(H_0).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Exact centered squared-defect coercivity and bounded inverse

Tests.ProximalBPSCenteredDefect.actual_centered_defect_coercive_and_unit · theorem · Teaching coverage

Read this first

Mathematical statement

E is a finite-dimensional real Hilbert Borel space with canonical volume; rank zero is an explicit extension of the source Euclidean convention. V:E→ℝ is C²; 0<α≤β; α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v; η>0 and βη≤1. μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), and ν=J.snd. Finite dimensionality of E does not imply finite dimensionality of L²(ν). There exist a selfadjoint bounded operator T on L²(ν) with the literal ν-a.e. action Tu(y)=∫u(x)S(y,dx), where S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); a class q=1 ν-a.e. with ⟨q,u⟩=∫u dν for all u; and the actual selfadjoint restriction T₀ to H₀=ker⟨q,·⟩. Set ρ=(1−αη)/(1+αη) and δ=4αη/(1+αη)². The squared defect D₀=I_H₀−T₀² is positive. For every u∈H₀, T₀u=Tu as an ambient class, ‖T₀u‖≤ρ‖u‖, ⟨D₀u,u⟩=‖u‖²−‖T₀u‖² and δ‖u‖²≤⟨D₀u,u⟩. D₀ is a unit in the algebra of bounded continuous linear endomorphisms of H₀; hence it has a bounded inverse on this exact centered space. The original hypotheses force δ>0 and include αη=1. No full-space inverse or positive square root is claimed.

\[\rho=\frac{1-\alpha\eta}{1+\alpha\eta},\quad\delta=\frac{4\alpha\eta}{(1+\alpha\eta)^2}>0,\quad\|T_0u\|\le\rho\|u\|,\quad\langle D_0u,u\rangle\ge\delta\|u\|^2,\quad D_0\in\operatorname{GL}(H_0).\]
Lean statement · actual_centered_defect_coercive_and_unit

E is a finite-dimensional real Hilbert Borel space with canonical volume; rank zero is an explicit extension of the source Euclidean convention. V:E→ℝ is C²; 0<α≤β; α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v; η>0 and βη≤1. μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), and ν=J.snd. Finite dimensionality of E does not imply finite dimensionality of L²(ν). There exist a selfadjoint bounded operator T on L²(ν) with the literal ν-a.e. action Tu(y)=∫u(x)S(y,dx), where S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); a class q=1 ν-a.e. with ⟨q,u⟩=∫u dν for all u; and the actual selfadjoint restriction T₀ to H₀=ker⟨q,·⟩. Set ρ=(1−αη)/(1+αη) and δ=4αη/(1+αη)². The squared defect D₀=I_H₀−T₀² is positive. For every u∈H₀, T₀u=Tu as an ambient class, ‖T₀u‖≤ρ‖u‖, ⟨D₀u,u⟩=‖u‖²−‖T₀u‖² and δ‖u‖²≤⟨D₀u,u⟩. D₀ is a unit in the algebra of bounded continuous linear endomorphisms of H₀; hence it has a bounded inverse on this exact centered space. The original hypotheses force δ>0 and include αη=1. No full-space inverse or positive square root 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.

Download module (.lean)
theorem actual_centered_defect_coercive_and_unit
    {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
    ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
      IsSelfAdjoint T ∧
      (∀ u : Lp ℝ 2 ν, (T u : E → ℝ) =ᵐ[ν]
        (fun y => ∫ x, u x ∂((volume : Measure E).tilted
          (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))))) ∧
      ∃ q : Lp ℝ 2 ν,
        (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧
        (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
        ∃ T0 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker),
          (∀ u : ((innerSL ℝ q).ker), (T0 u : Lp ℝ 2 ν) = T u) ∧
          IsSelfAdjoint T0 ∧ ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0).IsPositive ∧
          (∀ u : ((innerSL ℝ q).ker),
            ‖T0 u‖ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ ∧
            inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u = ‖u‖^2-‖T0 u‖^2 ∧
            (4*(α : ℝ)*η/(1+(α : ℝ)*η)^2)*‖u‖^2 ≤
              inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u) ∧
          IsUnit ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0)

Exact module and namespace context

Proof roadmap

  1. 1Use the same actual reflection and actual pullback

    Compare the AE reflection actions to identify the operator U in the verified macroscopic contraction. For the actual M from the producer, PM=M gives macro-range membership. Its AE action Mu(x,y)=u(y) and the actual marginal ν=J.snd give mean transport directly, so centered u yields a centered macro input. No extra onto witness or copied Poincare proof is needed.

  2. 2Transport the exact sharp contraction

    Apply the verified sharp macro contraction to Mu. The actual identity MT=PUPM and the isometry transfer the constant without changing laws or operators.

  3. 3Derive the positive coercivity constant

    Square the contraction and use the actual quadratic defect identity. Since 0<αη≤1, the exact scalar identity yields a strictly positive lower bound, including the endpoint αη=1.

  4. 4Obtain a bounded inverse on the centered space

    The centered kernel is a complete Hilbert space because it is closed in L². Apply the fixed Mathlib coercivity-to-unit theorem to D₀ with δ. IsUnit means that an inverse exists in the algebra of bounded continuous linear endomorphisms of this same centered space. In the norm hypothesis, nonnegativity of the quadratic form follows directly from the already proved δ gap.

Full assumptions and notation

All objects and hypotheses

  • The complete potential, curvature, initialization law and step conditions are stated above. No operator, probability, stationarity, mean-zero preservation or coercivity certificate is supplied by the caller.
  • L² consists of AE classes; finite dimension of E does not make L² finite dimensional. The whole closed mean-zero subspace is used.
  • Zero-dimensional E is explicitly included as an extension of the source Euclidean convention; αη=1 is retained.

Mathematical proof

1. Use the same actual reflection and actual pullback

Compare the AE reflection actions to identify the operator U in the verified macroscopic contraction. For the actual M from the producer, PM=M gives macro-range membership. Its AE action Mu(x,y)=u(y) and the actual marginal ν=J.snd give mean transport directly, so centered u yields a centered macro input. No extra onto witness or copied Poincare proof is needed.

\[PMu=Mu,\quad\int Mu\,dJ=\int u\,d\nu=0.\]
Corresponding Lean step

hSameU; hAll; hM; integral_congr_ae; integral_map

2. Transport the exact sharp contraction

Apply the verified sharp macro contraction to Mu. The actual identity MT=PUPM and the isometry transfer the constant without changing laws or operators.

\[\|T_0u\|\le\rho\|u\|,\quad\rho=\frac{1-\alpha\eta}{1+\alpha\eta}\in[0,1).\]
Corresponding Lean step

hSharp; hCon; M.norm_map; hT0

3. Derive the positive coercivity constant

Square the contraction and use the actual quadratic defect identity. Since 0<αη≤1, the exact scalar identity yields a strictly positive lower bound, including the endpoint αη=1.

\[\delta=1-\rho^2=\frac{4\alpha\eta}{(1+\alpha\eta)^2}>0,\quad\delta\|u\|^2\le\langle D_0u,u\rangle.\]
Corresponding Lean step

hδ; hρ; hDef0; hGap; field_simp; ring

4. Obtain a bounded inverse on the centered space

The centered kernel is a complete Hilbert space because it is closed in L². Apply the fixed Mathlib coercivity-to-unit theorem to D₀ with δ. IsUnit means that an inverse exists in the algebra of bounded continuous linear endomorphisms of this same centered space. In the norm hypothesis, nonnegativity of the quadratic form follows directly from the already proved δ gap.

\[D_0=I_{H_0}-T_0^2\in\operatorname{GL}(H_0).\]
Corresponding Lean step

ContinuousLinearMap.completeSpace_ker; isUnit_of_forall_le_norm_inner_map; hUnit

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · actual_centered_defect_coercive_and_unit

Use the same actual reflection and actual pullback; Transport the exact sharp contraction; Derive the positive coercivity constant; Obtain a bounded inverse on the centered space

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_centered_defect_coercive_and_unit
    {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
    ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
      IsSelfAdjoint T ∧
      (∀ u : Lp ℝ 2 ν, (T u : E → ℝ) =ᵐ[ν]
        (fun y => ∫ x, u x ∂((volume : Measure E).tilted
          (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))))) ∧
      ∃ q : Lp ℝ 2 ν,
        (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧
        (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
        ∃ T0 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker),
          (∀ u : ((innerSL ℝ q).ker), (T0 u : Lp ℝ 2 ν) = T u) ∧
          IsSelfAdjoint T0 ∧ ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0).IsPositive ∧
          (∀ u : ((innerSL ℝ q).ker),
            ‖T0 u‖ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ ∧
            inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u = ‖u‖^2-‖T0 u‖^2 ∧
            (4*(α : ℝ)*η/(1+(α : ℝ)*η)^2)*‖u‖^2 ≤
              inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u) ∧
          IsUnit ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) := 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 P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
    (lpMeas ℝ ℝ (MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E))
      2 J).subtypeL ∘L condExpL2 ℝ ℝ measurable_snd.comap_le
  obtain ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hSs,U,hU,hUi,hUs,M,hM,T,hTs,hAll,
    q,hq,hTq,hPair,hH0,hD,hDq,hDef,T0,hT0,hT0s,hT0n,hD0,hD0sub,hDef0⟩ :=
    CenteredDefectOperator.actual_centered_selfadjoint_defect hα hαβ hV hH hη hβη
  letI : IsProbabilityMeasure J := hJ
  letI : IsProbabilityMeasure ν := hν
  let H0 : Submodule ℝ (Lp ℝ 2 ν) := (innerSL ℝ q).ker
  have hLiteral (u : Lp ℝ 2 ν) : (T u : E → ℝ) =ᵐ[ν]
      (fun y => ∫ x, u x ∂((volume : Measure E).tilted
        (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η)))) := by
    filter_upwards [(hAll u).2.2.2.1] with y hy
    exact hy.trans (congrArg (fun m : Measure E => ∫ x, u x ∂m) (hSd y))
  have h58 := ProximalBPSMacroscopicRange.actual_centered_macro_contraction_and_defect_gap
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  dsimp only at h58
  obtain ⟨U58,hU58,hUi58,hUs58,hSharp⟩ := h58
  have hSameU : U58=U := LinearIsometry.ext (fun f =>
    Lp.ext ((hU58 f).trans (hU f).symm))
  subst U58
  have hCon (u : H0) : ‖T0 u‖ ≤
      ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ := by
    have hu : (∫ y, (u : Lp ℝ 2 ν) y ∂ν)=0 := (hH0 _).mp u.property
    have hr : M (u : Lp ℝ 2 ν) ∈ P.toLinearMap.range :=
      ⟨M u,(hAll (u : Lp ℝ 2 ν)).1⟩
    have hc : (∫ p, (M (u : Lp ℝ 2 ν)) p ∂J)=0 := by
      calc
        (∫ p, (M (u : Lp ℝ 2 ν)) p ∂J) = ∫ p : E × E, (u : Lp ℝ 2 ν) p.2 ∂J :=
          integral_congr_ae (hM (u : Lp ℝ 2 ν))
        _ = ∫ y, (u : Lp ℝ 2 ν) y ∂ν :=
          (integral_map (μ:=J) measurable_snd.aemeasurable
            (Lp.stronglyMeasurable (u : Lp ℝ 2 ν)).aestronglyMeasurable).symm
        _ = 0 := hu
    calc
      ‖T0 u‖ = ‖(T0 u : Lp ℝ 2 ν)‖ := rfl
      _ = ‖T (u : Lp ℝ 2 ν)‖ := congrArg norm (hT0 u)
      _ = ‖M (T (u : Lp ℝ 2 ν))‖ := (M.norm_map _).symm
      _ = ‖(P * U.toContinuousLinearMap * P) (M (u : Lp ℝ 2 ν))‖ :=
        congrArg norm ((hAll (u : Lp ℝ 2 ν)).2.1)
      _ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖M (u : Lp ℝ 2 ν)‖ :=
        (hSharp (M (u : Lp ℝ 2 ν)) hr hc).1
      _ = ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ :=
        congrArg (fun r : ℝ => ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*r) (M.norm_map _)
  let δ : ℝ := 4*(α : ℝ)*η/(1+(α : ℝ)*η)^2
  have ha0 : 0 < (α : ℝ)*η := mul_pos hα hη
  have ha1 : (α : ℝ)*η ≤ 1 :=
    (mul_le_mul_of_nonneg_right (by exact_mod_cast hαβ) hη.le).trans hβη
  have hd : 0 < 1+(α : ℝ)*η := by positivity
  have hρ : 0 ≤ (1-(α : ℝ)*η)/(1+(α : ℝ)*η) :=
    div_nonneg (sub_nonneg.mpr ha1) hd.le
  have hδ : 0 < δ := by dsimp [δ]; positivity
  have hGap (u : H0) : δ*‖u‖^2 ≤ inner ℝ (((1 : H0 →L[ℝ] H0)-T0*T0) u) u := by
    have hs : ‖T0 u‖^2 ≤ (((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖)^2 :=
      (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hρ (norm_nonneg _))).mpr (hCon u)
    have hr : δ = 1-((1-(α : ℝ)*η)/(1+(α : ℝ)*η))^2 := by
      dsimp [δ]
      field_simp [ne_of_gt hd]
      ring
    rw [hDef0,hr]
    nlinarith [hs]
  have hUnit : IsUnit ((1 : H0 →L[ℝ] H0)-T0*T0) := by
    apply ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map
      ((1 : H0 →L[ℝ] H0)-T0*T0) (c:=⟨δ,hδ.le⟩) (by exact hδ)
    intro u
    change ‖u‖^2*δ ≤ ‖inner ℝ (((1 : H0 →L[ℝ] H0)-T0*T0) u) u‖
    have hnn : 0 ≤ inner ℝ (((1 : H0 →L[ℝ] H0)-T0*T0) u) u :=
      (mul_nonneg hδ.le (sq_nonneg ‖u‖)).trans (hGap u)
    rw [Real.norm_eq_abs,abs_of_nonneg hnn,mul_comm]
    exact hGap u
  refine ⟨T,hTs,hLiteral,q,hq,hPair,T0,hT0,hT0s,hD0,?_,hUnit⟩
  intro u
  exact ⟨hCon u,hDef0 u,hGap u⟩

end
end Tests.ProximalBPSCenteredDefect

#print axioms Tests.ProximalBPSCenteredDefect.actual_centered_defect_coercive_and_unit

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Finite Euclidean real base and source standing C2, global lower/upper Hessian bounds and positive capped η.E is a finite-dimensional real Hilbert Borel space with canonical volume; rank zero is an explicit extension of the source Euclidean convention. V:E→ℝ is C²; 0<α≤β; α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v; η>0 and βη≤1. μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), and ν=J.snd. Finite dimensionality of E does not imply finite dimensionality of L²(ν).generalizationOriginal analytic/step hypotheses retained. Finite real Hilbert/Borel formulation and rank-zero extension are explicit; no finite-dimensional L2 or Nontrivial premise.
Actual normalized augmentation and reflected conditional kernel/operator.μ,J,ν,Λ,S,U,M,T and all Markov/disintegration/stationarity witnesses are produced under original inputs; S has the every-y displayed normalized density.sameNo supplied law/operator certificates; measurability, integrability and normalization come from actual55 and true marginal/disintegration.
Constant/mean-zero real L2 domain and squared defect precursor to Γ.q is AE1, the full H0 is ker inner(q); T0 is the actual restriction and D0 the restricted squared defect. The consumer proves exact rho/delta and IsUnit D0 on H0.sameA background completion for the actual paper consumer. Closedness/completeness and δ>0 are derived internally; no new public regularity/centering/coercivity premise.
Ordinary let abbreviation H0 and operator identity notation.Explicit typed operator identities and exact inline ker inner(q) in public header; local H0 remains that definition in proof.API-limitationTwo separately reviewed definitionally equal syntax overlays fix Lean elaboration. Complete rfl equivalences and inverse byte reconstruction; no source/math correction.
Positive Γ/root and inverse/polar, weakH1, dynamics, mixing, implementation errors, costs and composition.SAME actual55 T on L2(nu), selfadjoint/mean preserving/constant fixed, exact complete mean-zero restriction T0, full and centered positive squared defects; real Test uses actual58 rho/delta to prove IsUnit centered squared defect. No Gamma/root/polar/full weakH1/hypocoercivity/dynamics/main/implementation error/cost/composition/fullpaper/Goal admission.unresolvedIsUnit of the centered squared defect is not construction of Γ or proof of any main theorem or query-cost statement.

SAME actual55 T on L2(nu), selfadjoint/mean preserving/constant fixed, exact complete mean-zero restriction T0, full and centered positive squared defects; real Test uses actual58 rho/delta to prove IsUnit centered squared defect. No Gamma/root/polar/full weakH1/hypocoercivity/dynamics/main/implementation error/cost/composition/fullpaper/Goal admission.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Finite real Hilbert/Borel model is explicit Euclidean elaboration; rank-zero case is a disclosed ASTIS extension, not claimed source text. L2 may be infinite-dimensional. — Independent native generalization nonblocking classification retained in runs/20261007-companion-priority/pbps-centered-defect59/source-review59/source.1.review.json
  • objects: Explicit operator identity domains and exact inline kernel are definition notation only. Current entire statement independently checked; old syntax acceptance is not a source verdict substitute. — Independent native API-limitation nonblocking classification retained in runs/20261007-companion-priority/pbps-centered-defect59/source-review59/source.1.review.json
  • conclusion: Centered squared-defect IsUnit is an ASTIS complete-Hilbert coercivity consequence of actual58 sharp C4 and actual59 defect. It is not printed Gamma/root/polar theorem. — Independent native source-implicit nonblocking classification retained in runs/20261007-companion-priority/pbps-centered-defect59/source-review59/source.1.review.json
  • scopes: Gamma positive root/Loewner inverse/polar/fullweakH1/dynamics/main/errors/cost/composition remain outside admitted scope. Printed B5 source edges retained independently; pending whole-paper obligations are not failures of this scoped background statement. — Independent native unresolved nonblocking classification retained in runs/20261007-companion-priority/pbps-centered-defect59/source-review59/source.1.review.json

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
  • SAME actual55 T on L2(nu), selfadjoint/mean preserving/constant fixed, exact complete mean-zero restriction T0, full and centered positive squared defects; real Test uses actual58 rho/delta to prove IsUnit centered squared defect. No Gamma/root/polar/full weakH1/hypocoercivity/dynamics/main/implementation error/cost/composition/fullpaper/Goal admission.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • LinearIsometry.ext
  • Lp.ext
  • integral_congr_ae
  • integral_map
  • LinearIsometry.norm_map
  • sq_le_sq₀
  • ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Exact centered squared-defect coercivity and bounded inverse
  • TODO — not closed by these contributions Γ/root/polar/fullH1/dynamics/main/errors/cost/composition remain open