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

Actual centered selfadjoint operator and positive squared defect

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²(ν). Let Λ be the law of (Y,2X−Y) under J, F(x,y)=(x,2x−y), and P the L²(J) conditional-expectation orthogonal projection onto the second-coordinate sigma algebra. The laws μ,J,ν are probabilities. There exist a Markov kernel S with, for every y, S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), Λ disintegrated by S and both marginals equal to ν; an involutive selfadjoint linear isometry U with Ug=g∘F J-a.e.; an isometric pullback M with Mu=u∘snd J-a.e.; and a selfadjoint T on L²(ν) such that for every u, PMu=Mu, MTu=PUPMu, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-a.e. and ∫Tu dν=∫u dν. There is a constant class q=1 ν-a.e. with Tq=q and ⟨q,u⟩=∫u dν for all u. Its exact closed orthogonal kernel H₀ is all of L²₀(ν). The full defect D=I−T² is positive, Dq=0 and ⟨Du,u⟩=‖u‖²−‖Tu‖² for all u. The actual restriction T₀:H₀→H₀ agrees with T on every u∈H₀, is selfadjoint and contractive. D₀=I_H₀−T₀² is positive, agrees with D as an ambient L² class on H₀, and satisfies ⟨D₀u,u⟩=‖u‖²−‖T₀u‖² for all u∈H₀.

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

Actual centered selfadjoint operator and positive squared defect

\[H_0=\ker\langle1,\cdot\rangle=L^2_0(\nu),\quad T_0=T|_{H_0},\quad D=I-T^2\ge0,\quad D_0=D|_{H_0},\quad\langle D_0u,u\rangle=\|u\|^2-\|T_0u\|^2.\]

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

Actual centered selfadjoint operator and positive squared defect

AutoSamplingTheory.ExampleCases.ProximalBPS.CenteredDefectOperator.actual_centered_selfadjoint_defect · 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²(ν). Let Λ be the law of (Y,2X−Y) under J, F(x,y)=(x,2x−y), and P the L²(J) conditional-expectation orthogonal projection onto the second-coordinate sigma algebra. The laws μ,J,ν are probabilities. There exist a Markov kernel S with, for every y, S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), Λ disintegrated by S and both marginals equal to ν; an involutive selfadjoint linear isometry U with Ug=g∘F J-a.e.; an isometric pullback M with Mu=u∘snd J-a.e.; and a selfadjoint T on L²(ν) such that for every u, PMu=Mu, MTu=PUPMu, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-a.e. and ∫Tu dν=∫u dν. There is a constant class q=1 ν-a.e. with Tq=q and ⟨q,u⟩=∫u dν for all u. Its exact closed orthogonal kernel H₀ is all of L²₀(ν). The full defect D=I−T² is positive, Dq=0 and ⟨Du,u⟩=‖u‖²−‖Tu‖² for all u. The actual restriction T₀:H₀→H₀ agrees with T on every u∈H₀, is selfadjoint and contractive. D₀=I_H₀−T₀² is positive, agrees with D as an ambient L² class on H₀, and satisfies ⟨D₀u,u⟩=‖u‖²−‖T₀u‖² for all u∈H₀.

\[H_0=\ker\langle1,\cdot\rangle=L^2_0(\nu),\quad T_0=T|_{H_0},\quad D=I-T^2\ge0,\quad D_0=D|_{H_0},\quad\langle D_0u,u\rangle=\|u\|^2-\|T_0u\|^2.\]
Lean statement · actual_centered_selfadjoint_defect

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²(ν). Let Λ be the law of (Y,2X−Y) under J, F(x,y)=(x,2x−y), and P the L²(J) conditional-expectation orthogonal projection onto the second-coordinate sigma algebra. The laws μ,J,ν are probabilities. There exist a Markov kernel S with, for every y, S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), Λ disintegrated by S and both marginals equal to ν; an involutive selfadjoint linear isometry U with Ug=g∘F J-a.e.; an isometric pullback M with Mu=u∘snd J-a.e.; and a selfadjoint T on L²(ν) such that for every u, PMu=Mu, MTu=PUPMu, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-a.e. and ∫Tu dν=∫u dν. There is a constant class q=1 ν-a.e. with Tq=q and ⟨q,u⟩=∫u dν for all u. Its exact closed orthogonal kernel H₀ is all of L²₀(ν). The full defect D=I−T² is positive, Dq=0 and ⟨Du,u⟩=‖u‖²−‖Tu‖² for all u. The actual restriction T₀:H₀→H₀ agrees with T on every u∈H₀, is selfadjoint and contractive. D₀=I_H₀−T₀² is positive, agrees with D as an ambient L² class on H₀, and satisfies ⟨D₀u,u⟩=‖u‖²−‖T₀u‖² for all u∈H₀.

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_selfadjoint_defect
    {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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
    let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
    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
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
    ∃ S : Kernel E E, IsMarkovKernel S ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
      Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
      ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
        (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
        Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
        ∃ M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J,
          (∀ u : Lp ℝ 2 ν, (M u : E × E → ℝ) =ᵐ[J] u ∘ Prod.snd) ∧
          ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
            IsSelfAdjoint T ∧
            (∀ u : Lp ℝ 2 ν,
              P (M u) = M u ∧
              M (T u) = (P * U.toContinuousLinearMap * P) (M u) ∧
              ‖T u‖ ≤ ‖u‖ ∧
              (T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
              (∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
            ∃ q : Lp ℝ 2 ν,
              (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧ T q = q ∧
              (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
              (∀ u : Lp ℝ 2 ν, u ∈ ((innerSL ℝ q).ker) ↔ (∫ y, u y ∂ν) = 0) ∧
              ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T).IsPositive ∧ ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) q = 0 ∧
              (∀ u : Lp ℝ 2 ν,
                inner ℝ (((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) u) u = ‖u‖^2-‖T u‖^2) ∧
              ∃ T0 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker),
                (∀ u : ((innerSL ℝ q).ker), (T0 u : Lp ℝ 2 ν) = T u) ∧
                IsSelfAdjoint T0 ∧ (∀ u : ((innerSL ℝ q).ker), ‖T0 u‖ ≤ ‖u‖) ∧
                ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0).IsPositive ∧
                (∀ u : ((innerSL ℝ q).ker), (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u : Lp ℝ 2 ν) = ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) u) ∧
                (∀ u : ((innerSL ℝ q).ker),
                  inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u = ‖u‖^2-‖T0 u‖^2)

Exact module and namespace context

Proof roadmap

  1. 1Recover the actual kernel and Hilbert operators

    Reuse the compiled actual Gaussian augmentation, reflected conditional kernel S, isometric reflection U, second-coordinate pullback M, and operator T. The kernel has the literal normalized density exp(−V((y+x)/2)−‖y−x‖²/(8η)); its stationary law and probability normalization are conclusions, not supplied premises.

  2. 2Transport selfadjointness

    The actual conditional expectation P is an orthogonal projection and U is selfadjoint. Move P across the inner product and use PM=M; the isometry M transfers the resulting symmetry to T.

  3. 3Prove mean preservation with the actual joint law

    The reflected joint law Λ disintegrates as ν⊗S and has second marginal ν. Each L² function is integrable because ν is a probability. The actual AE formula for T and Fubini therefore give mean preservation.

  4. 4Identify the constant and the entire centered space

    Take the canonical L² constant q=1. Its inner product is the mean. Selfadjointness and mean preservation imply Tq=q. The kernel of the continuous functional inner(q,·) is exactly all mean-zero classes, is closed, and is preserved by T.

  5. 5Restrict the actual operator

    Restrict T to the closed invariant subspace H₀. Its action as an ambient L² class is exactly T; symmetry and the norm bound transfer to this same restriction T₀.

  6. 6Compute both squared defects

    For either selfadjoint contraction, move one copy of T across the inner product. The result is nonnegative, so D=I−T² and D₀=I−T₀² are positive. Dq=0, and the centered defect is the actual restriction of D.

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. Recover the actual kernel and Hilbert operators

Reuse the compiled actual Gaussian augmentation, reflected conditional kernel S, isometric reflection U, second-coordinate pullback M, and operator T. The kernel has the literal normalized density exp(−V((y+x)/2)−‖y−x‖²/(8η)); its stationary law and probability normalization are conclusions, not supplied premises.

\[Tu(y)=\int u(x)\,S(y,dx),\quad MT=PUPM.\]
Corresponding Lean step

L2MacroscopicMean.actual_macroscopic_l2_mean; hBase

2. Transport selfadjointness

The actual conditional expectation P is an orthogonal projection and U is selfadjoint. Move P across the inner product and use PM=M; the isometry M transfers the resulting symmetry to T.

\[\langle Tu,v\rangle=\langle PUPMu,Mv\rangle=\langle Mu,PUPMv\rangle=\langle u,Tv\rangle.\]
Corresponding Lean step

hPs; M.inner_map_map; hTs

3. Prove mean preservation with the actual joint law

The reflected joint law Λ disintegrates as ν⊗S and has second marginal ν. Each L² function is integrable because ν is a probability. The actual AE formula for T and Fubini therefore give mean preservation.

\[\int Tu\,d\nu=\int u(x)\,d(\nu\otimes S)(y,x)=\int u\,d\nu.\]
Corresponding Lean step

Measure.disintegrate; integral_compProd; integral_map; hPreserve

4. Identify the constant and the entire centered space

Take the canonical L² constant q=1. Its inner product is the mean. Selfadjointness and mean preservation imply Tq=q. The kernel of the continuous functional inner(q,·) is exactly all mean-zero classes, is closed, and is preserved by T.

\[q=1,\quad Tq=q,\quad H_0=\ker\langle q,\cdot\rangle=L^2_0(\nu).\]
Corresponding Lean step

L2Expectation.one; inner_one_eq_integral; hTq; hH0

5. Restrict the actual operator

Restrict T to the closed invariant subspace H₀. Its action as an ambient L² class is exactly T; symmetry and the norm bound transfer to this same restriction T₀.

\[T_0u=Tu,\quad T_0=T_0^*,\quad\|T_0u\|\le\|u\|.\]
Corresponding Lean step

codRestrict; hInv; hT0; hT0s; hT0n

6. Compute both squared defects

For either selfadjoint contraction, move one copy of T across the inner product. The result is nonnegative, so D=I−T² and D₀=I−T₀² are positive. Dq=0, and the centered defect is the actual restriction of D.

\[\langle (I-T^2)u,u\rangle=\|u\|^2-\|Tu\|^2\ge0,\quad Dq=0,\quad D_0u=Du.\]
Corresponding Lean step

hDef; hD; hDef0; hD0

Lean verification

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

Lean proof · actual_centered_selfadjoint_defect

Recover the actual kernel and Hilbert operators; Transport selfadjointness; Prove mean preservation with the actual joint law; Identify the constant and the entire centered space; Restrict the actual operator; Compute both squared defects

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_selfadjoint_defect
    {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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
    let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
    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
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
    ∃ S : Kernel E E, IsMarkovKernel S ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
      Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
      ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
        (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
        Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
        ∃ M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J,
          (∀ u : Lp ℝ 2 ν, (M u : E × E → ℝ) =ᵐ[J] u ∘ Prod.snd) ∧
          ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
            IsSelfAdjoint T ∧
            (∀ u : Lp ℝ 2 ν,
              P (M u) = M u ∧
              M (T u) = (P * U.toContinuousLinearMap * P) (M u) ∧
              ‖T u‖ ≤ ‖u‖ ∧
              (T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
              (∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
            ∃ q : Lp ℝ 2 ν,
              (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧ T q = q ∧
              (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
              (∀ u : Lp ℝ 2 ν, u ∈ ((innerSL ℝ q).ker) ↔ (∫ y, u y ∂ν) = 0) ∧
              ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T).IsPositive ∧ ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) q = 0 ∧
              (∀ u : Lp ℝ 2 ν,
                inner ℝ (((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) u) u = ‖u‖^2-‖T u‖^2) ∧
              ∃ T0 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker),
                (∀ u : ((innerSL ℝ q).ker), (T0 u : Lp ℝ 2 ν) = T u) ∧
                IsSelfAdjoint T0 ∧ (∀ u : ((innerSL ℝ q).ker), ‖T0 u‖ ≤ ‖u‖) ∧
                ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0).IsPositive ∧
                (∀ u : ((innerSL ℝ q).ker), (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u : Lp ℝ 2 ν) = ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) u) ∧
                (∀ u : ((innerSL ℝ q).ker),
                  inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u = ‖u‖^2-‖T0 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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
  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
  have hBase := L2MacroscopicMean.actual_macroscopic_l2_mean hα hαβ hV hH hη hβη
  rcases hBase with ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hSs,U,hU,hUi,hUs,M,hM,T,hAll⟩
  letI : IsProbabilityMeasure μ := hμ
  letI : IsProbabilityMeasure J := hJ
  letI : IsProbabilityMeasure ν := hν
  letI : IsMarkovKernel S := hS
  letI : Λ.IsCondKernel S := hSc
  have hPs (f g : Lp ℝ 2 J) : inner ℝ (P f) g = inner ℝ f (P g) :=
    inner_condExpL2_left_eq_right measurable_snd.comap_le
  have hTs : IsSelfAdjoint T := by
    apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
    intro u v
    change inner ℝ (T u) v = inner ℝ u (T v)
    rw [← M.inner_map_map (T u) v, ← M.inner_map_map u (T v)]
    rw [(hAll u).2.1, (hAll v).2.1]
    change inner ℝ (P (U (P (M u)))) (M v) =
      inner ℝ (M u) (P (U (P (M v))))
    rw [hPs, (hAll u).1, (hAll v).1]
    calc
      inner ℝ (U (M u)) (M v) = inner ℝ (M u) (U (M v)) :=
        hUs.isSymmetric (M u) (M v)
      _ = inner ℝ (M u) (P (U (M v))) := by
        rw [← hPs, (hAll u).1]
  have hcompS : ν ⊗ₘ S = Λ := by
    calc
      ν ⊗ₘ S = Λ.fst ⊗ₘ S := congrArg (fun ρ => ρ ⊗ₘ S) hSf.symm
      _ = Λ := Measure.disintegrate Λ S
  have hPreserve (u : Lp ℝ 2 ν) : (∫ y, T u y ∂ν)=∫ y, u y ∂ν := by
    have hi : Integrable (fun p : E × E => u p.2) (ν ⊗ₘ S) := by
      rw [hcompS]
      exact ((Lp.memLp u).comp_measurePreserving
        (show MeasurePreserving (Prod.snd : E × E → E) Λ ν from
          ⟨measurable_snd,hSs⟩)).integrable (by norm_num)
    rw [integral_congr_ae (hAll u).2.2.2.1, ← Measure.integral_compProd hi, hcompS]
    calc
      (∫ p : E × E, u p.2 ∂Λ) = ∫ y, u y ∂Λ.snd :=
        (integral_map (μ:=Λ) measurable_snd.aemeasurable
          (Lp.stronglyMeasurable u).aestronglyMeasurable).symm
      _ = ∫ y, u y ∂ν := by rw [hSs]
  let q : Lp ℝ 2 ν := AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation.one ν
  have hq (u : Lp ℝ 2 ν) : inner ℝ q u = ∫ y, u y ∂ν :=
    AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation.inner_one_eq_integral ν u
  have hTq : T q=q := by
    apply ext_inner_right ℝ
    intro u
    calc
      inner ℝ (T q) u = inner ℝ q (T u) := hTs.isSymmetric q u
      _ = ∫ y, T u y ∂ν := hq _
      _ = ∫ y, u y ∂ν := hPreserve u
      _ = inner ℝ q u := (hq _).symm
  let H0 : Submodule ℝ (Lp ℝ 2 ν) := (innerSL ℝ q).ker
  have hH0 (u : Lp ℝ 2 ν) : u ∈ H0 ↔ (∫ y, u y ∂ν)=0 := by
    change inner ℝ q u = 0 ↔ _
    rw [hq]
  have hInv (u : H0) : T u ∈ H0 :=
    (hH0 _).mpr ((hPreserve u).trans ((hH0 _).mp u.property))
  let T0 : H0 →L[ℝ] H0 := (T.comp H0.subtypeL).codRestrict H0 hInv
  have hT0 (u : H0) : (T0 u : Lp ℝ 2 ν)=T u := rfl
  have hT0s : IsSelfAdjoint T0 := by
    apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
    intro u v
    exact hTs.isSymmetric (u : Lp ℝ 2 ν) (v : Lp ℝ 2 ν)
  have hTn (u : Lp ℝ 2 ν) : ‖T u‖ ≤ ‖u‖ := (hAll u).2.2.1
  have hT0n (u : H0) : ‖T0 u‖ ≤ ‖u‖ := hTn u
  have hDef (u : Lp ℝ 2 ν) : inner ℝ (((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) u) u = ‖u‖^2-‖T u‖^2 := by
    simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.one_apply,
      ContinuousLinearMap.mul_apply, inner_sub_left]
    have hs : inner ℝ (T (T u)) u = inner ℝ (T u) (T u) := hTs.isSymmetric (T u) u
    rw [hs, real_inner_self_eq_norm_sq, real_inner_self_eq_norm_sq]
  have hD : ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T).IsPositive := by
    apply (ContinuousLinearMap.isPositive_iff' _).mpr
    refine ⟨((IsSelfAdjoint.one (Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)).sub (by simpa only [pow_two] using hTs.pow 2)),?_⟩
    intro u
    rw [hDef]
    exact sub_nonneg.mpr ((sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mpr (hTn u))
  have hDef0 (u : H0) : inner ℝ (((1 : H0 →L[ℝ] H0)-T0*T0) u) u = ‖u‖^2-‖T0 u‖^2 := by
    simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.one_apply,
      ContinuousLinearMap.mul_apply, inner_sub_left]
    have hs : inner ℝ (T0 (T0 u)) u = inner ℝ (T0 u) (T0 u) := hT0s.isSymmetric (T0 u) u
    rw [hs, real_inner_self_eq_norm_sq, real_inner_self_eq_norm_sq]
  have hD0 : ((1 : H0 →L[ℝ] H0)-T0*T0).IsPositive := by
    apply (ContinuousLinearMap.isPositive_iff' _).mpr
    refine ⟨(IsSelfAdjoint.one (H0 →L[ℝ] H0)).sub (by simpa only [pow_two] using hT0s.pow 2),?_⟩
    intro u
    rw [hDef0]
    exact sub_nonneg.mpr ((sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mpr (hT0n u))
  have hqa : (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) :=
    Lp.coeFn_const (α:=E) (μ:=ν) (p:=(2 : ℝ≥0∞)) (c:=(1 : ℝ))
  refine ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hSs,U,hU,hUi,hUs,M,hM,T,hTs,?_,
    q,hqa,hTq,hq,?_⟩
  · intro u
    exact ⟨(hAll u).1,(hAll u).2.1,hTn u,(hAll u).2.2.2.1,hPreserve u⟩
  · refine ⟨hH0,hD,?_,hDef,T0,hT0,hT0s,hT0n,hD0,?_,hDef0⟩
    · simp only [ContinuousLinearMap.sub_apply,ContinuousLinearMap.one_apply,
        ContinuousLinearMap.mul_apply,hTq,sub_self]
    · intro u
      rfl

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.CenteredDefectOperator

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.CenteredDefectOperator.actual_centered_selfadjoint_defect

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.0.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.0.review.json
  • conclusion: Actual selfadjointness/means/constant/closed restriction and positive scalar squared defects complete source background; not printed joint B5 identity. — Independent native source-implicit nonblocking classification retained in runs/20261007-companion-priority/pbps-centered-defect59/source-review59/source.0.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.0.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)

  • inner_condExpL2_left_eq_right
  • LinearIsometry.inner_map_map
  • Measure.disintegrate
  • Measure.integral_compProd
  • integral_map
  • ContinuousLinearMap.isPositive_iff'
  • ContinuousLinearMap.completeSpace_ker

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 Actual centered selfadjoint operator and positive squared defect
  • TODO — not closed by these contributions Γ/root/polar/fullH1/dynamics/main/errors/cost/composition remain open