Documentation

MIPRE.Background.Repetition.CommutingRepetition.VN.Modular.ModularOperator

Real-linear operators commuting with i are complex-linear #

source
noncomputable def CommutingRepetition.VN.Modular.complexify {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (T : K →L[ℝ] K) (hT : ∀ (x : K), T (Complex.I • x) = Complex.I • T x) :
K →L[ℂ] K

A bounded real-linear operator commuting with multiplication by i, as a complex-linear operator.

Equations
Instances For
    source
    theorem CommutingRepetition.VN.Modular.complexify_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (T : K →L[ℝ] K) (hT : ∀ (x : K), T (Complex.I • x) = Complex.I • T x) (x : K) :
    (complexify T hT) x = T x
    source
    theorem CommutingRepetition.VN.Modular.inner_eq_of_re_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {A : K →L[ℂ] K} (h : ∀ (x y : K), (inner ℂ (A x) y).re = (inner ℂ x (A y)).re) (x y : K) :
    inner ℂ (A x) y = inner ℂ x (A y)

    A complex-linear operator whose real quadratic form is symmetric is symmetric.

    source
    theorem CommutingRepetition.VN.Modular.inner_I_smul_I_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a b : K) :
    inner ℝ (Complex.I • a) (Complex.I • b) = inner ℝ a b

    The real projections P and Q #

    source
    noncomputable def CommutingRepetition.VN.Modular.Pre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
    K →L[ℝ] K

    The real orthogonal projection onto 𝒦.

    Equations
    Instances For
      source
      noncomputable def CommutingRepetition.VN.Modular.Qre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
      K →L[ℝ] K

      The real orthogonal projection onto i𝒦.

      Equations
      Instances For
        source
        theorem CommutingRepetition.VN.Modular.Pre_apply_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Pre M Ω) x ∈ Kre M Ω
        source
        theorem CommutingRepetition.VN.Modular.Qre_apply_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Qre M Ω) x ∈ (Kre M Ω).mulI
        source
        theorem CommutingRepetition.VN.Modular.Pre_eq_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} (hx : x ∈ Kre M Ω) :
        (Pre M Ω) x = x
        source
        theorem CommutingRepetition.VN.Modular.Qre_eq_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} (hx : x ∈ (Kre M Ω).mulI) :
        (Qre M Ω) x = x
        source
        theorem CommutingRepetition.VN.Modular.Pre_Pre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Pre M Ω) ((Pre M Ω) x) = (Pre M Ω) x
        source
        theorem CommutingRepetition.VN.Modular.Qre_Qre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Qre M Ω) ((Qre M Ω) x) = (Qre M Ω) x
        source
        theorem CommutingRepetition.VN.Modular.inner_Pre_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x y : K) :
        inner ℝ ((Pre M Ω) x) y = inner ℝ x ((Pre M Ω) y)
        source
        theorem CommutingRepetition.VN.Modular.inner_Qre_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x y : K) :
        inner ℝ ((Qre M Ω) x) y = inner ℝ x ((Qre M Ω) y)
        source
        theorem CommutingRepetition.VN.Modular.inner_Pre_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        inner ℝ ((Pre M Ω) x) x = ‖(Pre M Ω) x‖ ^ 2
        source
        theorem CommutingRepetition.VN.Modular.inner_Qre_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        inner ℝ ((Qre M Ω) x) x = ‖(Qre M Ω) x‖ ^ 2
        source
        theorem CommutingRepetition.VN.Modular.norm_Pre_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        ‖(Pre M Ω) x‖ ≤ ‖x‖
        source
        theorem CommutingRepetition.VN.Modular.norm_Qre_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        ‖(Qre M Ω) x‖ ≤ ‖x‖
        source
        theorem CommutingRepetition.VN.Modular.Pre_eq_zero_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} :
        (Pre M Ω) x = 0 ↔ x ∈ (↑(Kre M Ω))ᗮ
        source
        theorem CommutingRepetition.VN.Modular.Qre_eq_zero_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} :
        (Qre M Ω) x = 0 ↔ x ∈ (↑(Kre M Ω).mulI)ᗮ
        source
        theorem CommutingRepetition.VN.Modular.Pre_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
        (Pre M Ω) Ω = Ω
        source
        theorem CommutingRepetition.VN.Modular.Qre_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
        (Qre M Ω) Ω = 0
        source
        theorem CommutingRepetition.VN.Modular.Qre_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Qre M Ω) x = Complex.I • (Pre M Ω) (-Complex.I • x)

        Q = i P i⁻¹.

        source
        theorem CommutingRepetition.VN.Modular.Pre_I_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Pre M Ω) (Complex.I • x) = Complex.I • (Qre M Ω) x
        source
        theorem CommutingRepetition.VN.Modular.Qre_I_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Qre M Ω) (Complex.I • x) = Complex.I • (Pre M Ω) x
        source
        theorem CommutingRepetition.VN.Modular.Pre_sub_Qre_I_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Pre M Ω - Qre M Ω) (Complex.I • x) = -Complex.I • (Pre M Ω - Qre M Ω) x

        P − Q is conjugate-linear.

        The operator R = P + Q #

        source
        theorem CommutingRepetition.VN.Modular.Pre_add_Qre_I_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
        (Pre M Ω + Qre M Ω) (Complex.I • x) = Complex.I • (Pre M Ω + Qre M Ω) x
        source
        noncomputable def CommutingRepetition.VN.Modular.R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
        K →L[ℂ] K

        R = P + Q, complex-linear (RvD Prop. 3.1).

        Equations
        Instances For
          source
          theorem CommutingRepetition.VN.Modular.R_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
          (R M Ω) x = (Pre M Ω) x + (Qre M Ω) x
          source
          theorem CommutingRepetition.VN.Modular.re_inner_R_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x y : K) :
          (inner ℂ ((R M Ω) x) y).re = (inner ℂ x ((R M Ω) y)).re
          source
          theorem CommutingRepetition.VN.Modular.inner_R_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x y : K) :
          inner ℂ ((R M Ω) x) y = inner ℂ x ((R M Ω) y)
          source
          theorem CommutingRepetition.VN.Modular.R_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
          IsSelfAdjoint (R M Ω)
          source
          theorem CommutingRepetition.VN.Modular.re_inner_R_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
          (inner ℂ ((R M Ω) x) x).re = ‖(Pre M Ω) x‖ ^ 2 + ‖(Qre M Ω) x‖ ^ 2
          source
          theorem CommutingRepetition.VN.Modular.im_inner_R_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
          (inner ℂ ((R M Ω) x) x).im = 0
          source
          theorem CommutingRepetition.VN.Modular.inner_R_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
          inner ℂ ((R M Ω) x) x = ↑(‖(Pre M Ω) x‖ ^ 2 + ‖(Qre M Ω) x‖ ^ 2)
          source
          theorem CommutingRepetition.VN.Modular.R_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
          0 ≤ R M Ω

          0 ≤ R (RvD Prop. 2.2(1)).

          source
          theorem CommutingRepetition.VN.Modular.inner_two_sub_R_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) :
          inner ℂ ((2 - R M Ω) x) x = ↑(2 * ‖x‖ ^ 2 - ‖(Pre M Ω) x‖ ^ 2 - ‖(Qre M Ω) x‖ ^ 2)
          source
          theorem CommutingRepetition.VN.Modular.R_le_two {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
          R M Ω ≤ 2

          R ≤ 2 (RvD Prop. 2.2(1)).

          source
          theorem CommutingRepetition.VN.Modular.R_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
          (R M Ω) Ω = Ω

          Injectivity of R and 2 − R (RvD Prop. 2.2(1)) #

          source
          theorem CommutingRepetition.VN.Modular.R_eq_zero_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hc : IsCyclic (↑M) Ω) {x : K} :
          (R M Ω) x = 0 ↔ x = 0

          R is injective: R x = 0 forces x ⊥ 𝒦 and x ⊥ i𝒦, and 𝒦 + i𝒦 is dense.

          source
          theorem CommutingRepetition.VN.Modular.two_sub_R_eq_zero_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) {x : K} :
          (2 - R M Ω) x = 0 ↔ x = 0

          2 − R is injective: (2 − R) x = 0 forces x ∈ 𝒦 ∩ i𝒦 = 0.