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

Actual PBPS squared defect: positive real root and energy

AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot.actual_positive_real_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², let 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∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. The laws μ,J,ν are probabilities. There exists a Markov kernel S whose every-state normalized density is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), with Λ.IsCondKernel S and Λ.fst=Λ.snd=ν. There exists a bounded selfadjoint T on the actual real L²(ν) such that for every u, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere, and ∫Tu dν=∫u dν. Its full scalar defect D=I−T² is positive. There exists a bounded positive REAL Γ with Γ²=D and for EVERY scalar u, ‖Γu‖²=‖u‖²−‖Tu‖². Probability, kernel, T, D positivity and Γ are conclusions; no supplied CFC/root/commutation or finite-dimensional L² certificate is assumed. This is the scalar precursor to the printed joint/macro root and B.11, which remain separate.

\[D=I-T^2\ge0,\quad\Gamma\ge0,\quad\Gamma^2=I-T^2,\quad\forall u\in L^2(\nu;\mathbb R),\ \|\Gamma u\|^2=\|u\|^2-\|Tu\|^2.\]
Lean statement · actual_positive_real_defect_root

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 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∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. The laws μ,J,ν are probabilities. There exists a Markov kernel S whose every-state normalized density is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), with Λ.IsCondKernel S and Λ.fst=Λ.snd=ν. There exists a bounded selfadjoint T on the actual real L²(ν) such that for every u, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere, and ∫Tu dν=∫u dν. Its full scalar defect D=I−T² is positive. There exists a bounded positive REAL Γ with Γ²=D and for EVERY scalar u, ‖Γu‖²=‖u‖²−‖Tu‖². Probability, kernel, T, D positivity and Γ are conclusions; no supplied CFC/root/commutation or finite-dimensional L² certificate is assumed. This is the scalar precursor to the printed joint/macro root and B.11, which remain separate.

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_positive_real_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))
    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 = ν ∧
      ∃ 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 ∂ν) ∧
        ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T).IsPositive ∧
        ∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
          Γ.IsPositive ∧ Γ*Γ = ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) ∧
          ∀ u : Lp ℝ 2 ν, ‖Γ u‖^2 = ‖u‖^2-‖T u‖^2

Exact module and namespace context

Proof roadmap

  1. 1Produce the genuine reflected kernel and scalar defect

    The independently verified centered-defect producer under the displayed original potential and step assumptions supplies probability μ,J,ν, the every-state normalized Markov S, genuine disintegration with both stationary marginals, and the same selfadjoint contractive mean-preserving T with AE conditional action. It proves D=I−T² positive internally, including the nontrivial constant mode; no caller operator or positivity certificate is used.

  2. 2Apply the shared real-root theorem to that same defect

    Apply the generic theorem to the actual marginal ν and the produced D. Its internally constructed positive real Γ satisfies Γ²=I−T². This supplies the real scalar root even when L² is infinite-dimensional and includes rank-zero base geometry and the legal αη=1 endpoint.

  3. 3Identify the scalar norm defect

    For every scalar observable u, root energy equals ⟨(I−T²)u,u⟩. Selfadjointness of the same T gives ⟨T²u,u⟩=‖Tu‖²; thus ‖Γu‖²=‖u‖²−‖Tu‖². The anonymous actual-input Test also checks ‖Γu‖≤‖u‖. This is a scalar B.11 precursor. Printed joint ΓP still requires the same onto M, restriction to ran(P) and the typed B*B identity; no full-space inverse is claimed.

Full assumptions and notation

All objects and hypotheses

  • Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 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∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J.
  • The normalized S, probability laws, same actual T and positive D and REAL Γ are produced conclusions. Finite E does not imply finite L²; rank-zero E and αη=1 remain permitted.
  • Pointwise conjugation is antiunitary on complex L² and differs from operator adjoint; its root-preservation and the descent are proved internally.

Mathematical proof

1. Produce the genuine reflected kernel and scalar defect

The independently verified centered-defect producer under the displayed original potential and step assumptions supplies probability μ,J,ν, the every-state normalized Markov S, genuine disintegration with both stationary marginals, and the same selfadjoint contractive mean-preserving T with AE conditional action. It proves D=I−T² positive internally, including the nontrivial constant mode; no caller operator or positivity certificate is used.

\[S(y,dx)\propto\exp\!\left[-V\!\left(\frac{y+x}{2}\right)-\frac{\|y-x\|^2}{8\eta}\right]dx,\quad Tu(y)=\int u(x)S(y,dx),\quad D=I-T^2\ge0.\]
Corresponding Lean step

CenteredDefectOperator.actual_centered_selfadjoint_defect; hBase; hAll; hD

2. Apply the shared real-root theorem to that same defect

Apply the generic theorem to the actual marginal ν and the produced D. Its internally constructed positive real Γ satisfies Γ²=I−T². This supplies the real scalar root even when L² is infinite-dimensional and includes rank-zero base geometry and the legal αη=1 endpoint.

\[\Gamma\ge0,\quad\Gamma^2=I-T^2\quad\text{on actual }L^2(\nu;\mathbb R).\]
Corresponding Lean step

L2RealSquareRoot.exists_positive_real_square_root; hΓ; hΓSq

3. Identify the scalar norm defect

For every scalar observable u, root energy equals ⟨(I−T²)u,u⟩. Selfadjointness of the same T gives ⟨T²u,u⟩=‖Tu‖²; thus ‖Γu‖²=‖u‖²−‖Tu‖². The anonymous actual-input Test also checks ‖Γu‖≤‖u‖. This is a scalar B.11 precursor. Printed joint ΓP still requires the same onto M, restriction to ran(P) and the typed B*B identity; no full-space inverse is claimed.

\[\|\Gamma u\|^2=\|u\|^2-\|Tu\|^2,\quad\|\Gamma u\|\le\|u\|.\]
Corresponding Lean step

hEnergy; hTs.isSymmetric; hs; real_inner_self_eq_norm_sq

Lean verification

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

Lean proof · actual_positive_real_defect_root

Produce the genuine reflected kernel and scalar defect; Apply the shared real-root theorem to that same defect; Identify the scalar norm defect

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_positive_real_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))
    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 = ν ∧
      ∃ 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 ∂ν) ∧
        ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T).IsPositive ∧
        ∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
          Γ.IsPositive ∧ Γ*Γ = ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) ∧
          ∀ u : Lp ℝ 2 ν, ‖Γ 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
  have hBase := CenteredDefectOperator.actual_centered_selfadjoint_defect
    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,hTs,hAll,
    q,hq,hTq,hqi,hzero,hD,hRest⟩
  obtain ⟨Γ,hΓ,hΓSq,hEnergy⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRoot.exists_positive_real_square_root
      ν ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) hD
  refine ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hSs,T,hTs,?_,hD,Γ,hΓ,hΓSq,?_⟩
  · intro u
    exact (hAll u).2.2
  · intro u
    rw [hEnergy]
    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]

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot.actual_positive_real_defect_root

Exact module and namespace context

Scope and omitted-condition boundaries
  • REAL scalar positive root and scalar energy only. Generic real uniqueness, canonical joint GammaP / P U blocks / onto transport / typed B*B, centered root order/inverse/polar, weakH1,dynamics,hypocoercivity,main,error,cost,composition remain separate; paper/Goal open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • ContinuousLinearMap.sub_apply
  • ContinuousLinearMap.mul_apply
  • IsSelfAdjoint.isSymmetric
  • real_inner_self_eq_norm_sq

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.