Documentation

MIPRE.Background.Repetition.CommutingRepetition.VN.Modular.ModularGroup

The functions λ ↦ ((2−λ)/λ)^{it} #

source
noncomputable def CommutingRepetition.VN.Modular.θ (l : ℝ) :
ℝ

log((2−λ)/λ) on (0,2), 0 elsewhere.

Equations
Instances For
    source
    theorem CommutingRepetition.VN.Modular.measurable_θ :
    Measurable θ
    source
    theorem CommutingRepetition.VN.Modular.θ_one :
    θ 1 = 0
    source
    noncomputable def CommutingRepetition.VN.Modular.gDel (t l : ℝ) :
    ℂ

    ((2−λ)/λ)^{it} = exp(i t θ(λ)).

    Equations
    Instances For
      source
      theorem CommutingRepetition.VN.Modular.norm_gDel (t l : ℝ) :
      ‖gDel t l‖ = 1
      source
      theorem CommutingRepetition.VN.Modular.measurable_gDel (t : ℝ) :
      Measurable (gDel t)
      source
      theorem CommutingRepetition.VN.Modular.cbdd_gDel (t : ℝ) :
      BorelCalc.CBdd (gDel t)
      source
      theorem CommutingRepetition.VN.Modular.gDel_zero :
      gDel 0 = fun (x : ℝ) => 1
      source
      theorem CommutingRepetition.VN.Modular.gDel_add (s t : ℝ) :
      gDel (s + t) = gDel s * gDel t
      source
      theorem CommutingRepetition.VN.Modular.gDel_neg (t : ℝ) :
      gDel (-t) = fun (l : ℝ) => (starRingEnd ℂ) (gDel t l)
      source
      theorem CommutingRepetition.VN.Modular.gDel_apply_one (t : ℝ) :
      gDel t 1 = 1
      source
      theorem CommutingRepetition.VN.Modular.continuous_gDel (l : ℝ) :
      Continuous fun (t : ℝ) => gDel t l

      The modular group #

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

      Δ^{it} := ((2−R)/R)^{it} (RvD Definition 3.2).

      Equations
      Instances For
        source
        theorem CommutingRepetition.VN.Modular.Δit_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :
        Δit M Ω 0 = 1
        source
        theorem CommutingRepetition.VN.Modular.Δit_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (s t : ℝ) :
        Δit M Ω (s + t) = Δit M Ω s * Δit M Ω t
        source
        theorem CommutingRepetition.VN.Modular.Δit_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        star (Δit M Ω t) = Δit M Ω (-t)
        source
        theorem CommutingRepetition.VN.Modular.Δit_comm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (s t : ℝ) :
        Δit M Ω s * Δit M Ω t = Δit M Ω t * Δit M Ω s
        source
        theorem CommutingRepetition.VN.Modular.Δit_neg_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        Δit M Ω (-t) * Δit M Ω t = 1
        source
        theorem CommutingRepetition.VN.Modular.Δit_mul_neg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        Δit M Ω t * Δit M Ω (-t) = 1
        source
        theorem CommutingRepetition.VN.Modular.star_Δit_mul_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        star (Δit M Ω t) * Δit M Ω t = 1
        source
        theorem CommutingRepetition.VN.Modular.Δit_mul_star_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        Δit M Ω t * star (Δit M Ω t) = 1
        source
        theorem CommutingRepetition.VN.Modular.Δit_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        (Δit M Ω t) Ω = Ω

        Δ^{it} Ω = Ω (R Ω = Ω and ((2−1)/1)^{it} = 1).

        source
        theorem CommutingRepetition.VN.Modular.norm_Δit_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (ξ : K) :
        ‖(Δit M Ω t) ξ‖ = ‖ξ‖
        source
        theorem CommutingRepetition.VN.Modular.norm_Δit_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        ‖Δit M Ω t‖ ≤ 1
        source
        theorem CommutingRepetition.VN.Modular.Δit_commute_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) :
        Commute (Δit M Ω t) (R M Ω)
        source
        theorem CommutingRepetition.VN.Modular.continuous_Δit_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω ξ : K) :
        Continuous fun (t : ℝ) => (Δit M Ω t) ξ

        Strong continuity of t ↦ Δ^{it} ξ.