Samplinglib mathematical lesson

Actual PBPS: the unique positive macroscopic defect root

AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicDefectRoot.actual_unique_positive_macroscopic_defect_root · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X~μ and Z~N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. These are probability laws. Put mY=comap(snd), H_P=L² classes measurable with respect to mY, P=i∘E[·|Y] and the canonical M:u↦u∘snd. Then H_P=ran(P), P is identity on H_P, and there exists an onto linear isometry e:L²(ν;ℝ)≃H_P with i e=M. There is a Markov kernel S whose every-state normalized law is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); Λ.IsCondKernel S and both Λ marginals equal ν. The same joint reflection F(x,y)=(x,2x−y) gives the involutive selfadjoint isometry U, with Uf=f∘F J-almost everywhere for every f. There is a bounded selfadjoint T on the full real L²(ν), with ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere for each u, and preserved integral. On H_P put A=PUP restricted via i and orthogonal projection, and B=(I_J−P)UPi:H_P→L²(J). Then A=eTe⁻¹ is selfadjoint and contractive, PB=0. There is a bounded positive real scalar Γ with Γ²=I−T². For the SAME transported Γ_P=eΓe⁻¹, positivity holds and Γ_P²=I_H_P−A²=B*B. Every f∈H_P satisfies ‖Bf‖=‖Γ_Pf‖ and ‖Γ_Pf‖²=‖f‖²−‖Af‖². EVERY bounded positive G on H_P whose square is I_H_P−A² equals Γ_P, independently of any energy premise. The genuine original-input consumer additionally derives ‖Γ_Pf‖≤‖f‖. Closedness/completeness, normalization, onto-M, positivity, roots and energy are internally derived; no caller certificate is assumed.

\[\Gamma_P=e\Gamma e^{-1}\ge0,\quad\Gamma_P^2=I_{H_P}-A^2=B^*B,\quad\|Bf\|=\|\Gamma_Pf\|,\quad\|\Gamma_Pf\|^2=\|f\|^2-\|Af\|^2.\]

Lean statement · actual_unique_positive_macroscopic_defect_root

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_unique_positive_macroscopic_defect_root
    {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 mY := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
    letI : MeasurableSpace (E × E) := Prod.instMeasurableSpace
    letI : Fact (mY ≤ (inferInstance : MeasurableSpace (E × E))) :=
      ⟨measurable_snd.comap_le⟩
    let HP := lpMeas ℝ ℝ mY 2 J
    let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
      HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
    let hp : MeasurePreserving (Prod.snd : E × E → E) J ν := ⟨measurable_snd,rfl⟩
    let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
    HP = P.toLinearMap.range ∧
    (∀ f : HP, P (f : Lp ℝ 2 J) = f) ∧
    ∃ 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 = ν ∧
      ∃ e : Lp ℝ 2 ν ≃ₗᵢ[ℝ] HP,
        (∀ u : Lp ℝ 2 ν, (e u : Lp ℝ 2 J) = M u) ∧
        ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
          (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
          Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
          ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
            IsSelfAdjoint T ∧
            (∀ u : Lp ℝ 2 ν,
              ‖T u‖ ≤ ‖u‖ ∧
              (T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
              (∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
            let A : HP →L[ℝ] HP :=
              HP.orthogonalProjectionOnto ∘L U.toContinuousLinearMap ∘L HP.subtypeL
            let B : HP →L[ℝ] Lp ℝ 2 J :=
              (((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P)*U.toContinuousLinearMap*P) ∘L HP.subtypeL
            A = e.conjStarAlgEquiv T ∧ IsSelfAdjoint A ∧
            (∀ f : HP, ‖A f‖ ≤ ‖f‖) ∧
            (∀ f : HP, P (B f) = 0) ∧
            ∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
              Γ.IsPositive ∧ Γ*Γ=(1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T ∧
              let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
              ΓP.IsPositive ∧ ΓP*ΓP=(1 : HP →L[ℝ] HP)-A*A ∧
              B.adjoint ∘L B = ΓP*ΓP ∧
              (∀ f : HP, ‖B f‖ = ‖ΓP f‖ ∧
                ‖ΓP f‖^2 = ‖f‖^2-‖A f‖^2) ∧
              (∀ G : HP →L[ℝ] HP,
                G.IsPositive → G*G=(1 : HP →L[ℝ] HP)-A*A → G=ΓP)

Exact module and namespace context

Proof roadmap

1Produce the actual probability laws and reflected conditional operator
Under the original C², both global Hessian bounds and capped positive η, the accepted actual centered-defect producer gives probability μ,J,ν, the every-y normalized reflected S, stationary disintegration, literal reflection U and selfadjoint contractive mean-preserving scalar T. Align independently produced pullbacks/reflections by their every-observable almost-everywhere action; no alternate kernel or operator is supplied.
2Identify the exact closed macro space and canonical onto isometry
The conditional projection equals the orthogonal projection onto H_P=lpMeas. Its range is H_P and it fixes every vector in H_P. The accepted actual range theorem identifies the SAME canonical M range with ran(P); restrict M to its range and use that equality to obtain the isometric equivalence e with inclusion i e=M. Ambient product measurability and completeness of the closed subspace are derived internally.
3Identify the same macroscopic reflected operator
The already proved pullback intertwining relation evaluated at e⁻¹f yields A=eTe⁻¹. Isometric conjugation preserves selfadjointness, and norm preservation transfers the scalar contraction to every macro f. The ambient operator A_J=PUP and the macro endomorphism A are kept separately typed.
4Restrict the correct full-joint Gram identity
Write B₀=(I_J−P)UP and B=B₀i. Projection idempotence gives PBf=0. The actual reflection block theorem gives B₀*B₀=P−A_J². Compose with i* and i; using Pi=i and iA=A_Ji, this becomes B*B=I_H_P−A². Replacing full-joint P by I_J would be false, including U=I with a nonidentity P.
5Transport the internally constructed positive real scalar root
The shared real L² root theorem produces Γ≥0 with Γ²=I−T². Define Γ_P by the SAME e-conjugation. Adjoint conjugation preserves positivity; the star-algebra equivalence preserves multiplication, subtraction and identity, so Γ_P²=I_H_P−A² and agrees with the preceding typed Gram operator. No real CFC or root witness is a public premise.
6Recover the macro norm and energy identities
Apply the scalar energy theorem to e⁻¹f and use the same isometry and A-conjugation to obtain macro energy. The adjoint inner-product identities for B and the positive selfadjoint Γ_P have equal squared norms since B*B=Γ_P²; nonnegative norms then give equality of norms.
7Prove uniqueness for every positive same-square macro alternative
For ANY positive G with G²=I_H_P−A², pull it back by e⁻¹. Its positivity and square are preserved, so the shared real scalar uniqueness theorem forces e⁻¹Ge=Γ. Conjugate back to obtain G=Γ_P. The universal alternative-root quantifier is outside the every-f energy conjunction and assumes no alternative energy identity.
8Exercise the original-input consumer without certificates
The Test takes the original potential and Hessian/step assumptions, invokes the actual macro theorem, and derives root contractivity from energy and the nonnegativity of ‖Af‖². It does not supply a probability kernel, onto map, defect, root or energy premise.

Full assumptions and notation

All objects and hypotheses

Original C² finite real Hilbert/Borel potential, 0<α≤β, both global Hessians, η>0, βη≤1. Rank-zero base extension and legal αη=1 remain explicit; L² is not assumed finite-dimensional.
The actual probability laws, normalized every-state kernel, canonical onto isometry, same reflected/conditional operators, positivity and roots/energy are conclusions, not caller certificates. Conditional actions are per-observable almost everywhere.
The macro domain is exactly the complete closed real HP=lpMeas=ran(P); full-joint P and identity on HP are kept distinct. L² need not be finite-dimensional. ALL positive same-square alternatives require no supplied energy identity and quantify outside every-f energy.

Mathematical proof

1. Produce the actual probability laws and reflected conditional operator

Under the original C², both global Hessian bounds and capped positive η, the accepted actual centered-defect producer gives probability μ,J,ν, the every-y normalized reflected S, stationary disintegration, literal reflection U and selfadjoint contractive mean-preserving scalar T. Align independently produced pullbacks/reflections by their every-observable almost-everywhere action; no alternate kernel or operator is supplied.

\[\Lambda\in\mathrm{CondKernel}(S),\quad\Lambda_1=\Lambda_2=\nu,\quad Uf=f\circ F\ (J\text{-a.e.}),\quad Tu(y)=\int u(x)S(y,dx)\ (\nu\text{-a.e.}).\]

Corresponding Lean step

  rcases CenteredDefectOperator.actual_centered_selfadjoint_defect hα hαβ hV hH hη hβη with
    ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hSs,U,hU,hUi,hUs,M0,hM0,T,hTs,hAll,
      q,hqa,hTq,hqi,hzero,hD,hDq,hDef,hRest⟩
  letI : IsProbabilityMeasure μ := hμ
  letI : IsProbabilityMeasure J := hJ
  letI : IsProbabilityMeasure ν := hν
  have hM0eq : M0 = M := by
    apply LinearIsometry.ext
    intro u
    apply Lp.ext
    exact (hM0 u).trans (Lp.coeFn_compMeasurePreserving u hp).symm
  subst M0