Actual PBPS squared defect: positive complex lift

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 with, for every y, S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), Λ.IsCondKernel S, Λ.fst=ν and Λ.snd=ν. There exists a selfadjoint bounded T on L²(ν;ℝ) such that for every u, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere, and ∫Tu dν=∫u dν. Set D=I−T²; this exact full-domain squared defect is positive. Define the actual quotient maps ιu=u+0i, Rg=Re g, Qg=Im g and Cg=conj(g). Then ι preserves norm, Cg=g iff g=ιu for some real u, and there exists a bounded complex-linear positive Dc on L²(ν;ℂ) such that Dc g=ιD(Rg)+iιD(Qg), Dc(ιu)=ι(Du), and C(Dc g)=Dc(Cg), universally on their displayed domains. The operator T, positivity, kernel/law certificates and Dc are produced conclusions. No real Γ/root/descent/inverse is asserted.

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.

theorem actual_positive_defect_complex_lift
    {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 ι : Lp ℝ 2 ν →L[ℝ] Lp ℂ 2 ν := Complex.ofRealCLM.compLpL 2 ν
    let R : Lp ℂ 2 ν →L[ℝ] Lp ℝ 2 ν := Complex.reCLM.compLpL 2 ν
    let Q : Lp ℂ 2 ν →L[ℝ] Lp ℝ 2 ν := Complex.imCLM.compLpL 2 ν
    let C : Lp ℂ 2 ν →L[ℝ] Lp ℂ 2 ν := Complex.conjCLE.toContinuousLinearMap.compLpL 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 ∧
        (∀ u : Lp ℝ 2 ν, ‖ι u‖ = ‖u‖) ∧
        (∀ g : Lp ℂ 2 ν, C g = g ↔ ∃ u : Lp ℝ 2 ν, ι u = g) ∧
        ∃ Dc : Lp ℂ 2 ν →L[ℂ] Lp ℂ 2 ν,
          Dc.IsPositive ∧
          (∀ g : Lp ℂ 2 ν, Dc g =
            ι (((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) (R g)) +
            Complex.I • ι (((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) (Q g))) ∧
          (∀ u : Lp ℝ 2 ν, Dc (ι u) = ι (((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) u)) ∧
          (∀ g : Lp ℂ 2 ν, C (Dc g) = Dc (C g))

Exact module and namespace context