L2RealComplexOperator: mathematical reading route

Mathematical statement

Let Ω be an arbitrary measurable space, μ any measure, and D a bounded positive real-linear endomorphism of L²(μ;ℝ). Positivity includes selfadjointness. Define the actual quotient maps ιu=u+0i, Rg=Re g, Qg=Im g and Cg=conj(g) via Mathlib compLpL. The embedding preserves norm: ‖ιu‖=‖u‖ for every u, and its full range is exactly the fixed space of C: Cg=g iff there exists u with ιu=g. There exists a bounded complex-linear positive operator Dc on L²(μ;ℂ), with for every g, Dc g=ιD(Rg)+iιD(Qg), for every real u, Dc(ιu)=ι(Du), and for every complex g, C(Dc g)=Dc(Cg). No root or inverse is asserted.

theorem exists_positive_complex_lift
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hD : D.IsPositive) :
    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 μ
    (∀ 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 = ι (D (R g)) + Complex.I • ι (D (Q g))) ∧
      (∀ u : Lp ℝ 2 μ, Dc (ι u) = ι (D u)) ∧
      (∀ g : Lp ℂ 2 μ, C (Dc g) = Dc (C g))

Proof roadmap

1. 1Construct the actual quotient maps

   The scalar maps ofReal, Re, Im and conjugation are bounded real-linear maps. compLpL carries them to the same AE quotient spaces. Its AE representative formula proves Rι=I, Qι=0 and ιRg+iιQg=g. No representative is chosen as an additional input.

2. 2Identify the real subspace and its norm

   Integrating the pointwise inner products gives ⟨ιu,ιv⟩ℂ=⟨u,v⟩ℝ. Thus ι preserves norm. The equality Cg=g implies Im g=0 almost everywhere, so g=ιRg; the converse follows from conjugating a real value. This proves the exact fixed range for arbitrary μ.

3. 3Build a bounded complex-linear operator

   First form the bounded real-linear map Dc g=ιD(Rg)+iιD(Qg). The identities R(ig)=−Qg and Q(ig)=Rg show Dc(ig)=iDc g. Writing c=Re c+i Im c upgrades real linearity to complex linearity, while preserving the already proved continuity.

4. 4Cancel the imaginary cross terms

   Expand the complex inner product at g=ιa+iιb, where a=Rg,b=Qg. Real selfadjointness gives ⟨Db,a⟩ℝ=⟨Da,b⟩ℝ, cancelling the imaginary cross terms. The remaining two real quadratic forms are nonnegative by the original positivity of D.

5. 5Prove both compatibility identities

   On real inputs, Rι=I and Qι=0 give Dcι=ιD. Conjugation preserves the real part and negates the imaginary part; substituting into the literal formula gives CDc=DcC. Operator adjoint and pointwise conjugation are distinct operations.