PhaseWordDrift.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Phase averaging of the actual word commutators

The commutator applied to a vector is linear in its algebra argument. Consequently the exact multiset expansion and finite Parseval identity identify the word's root-mean-square drift with its coefficient-column norm.

def OAI.KadisonKastler.commutatorVector line 24

Source documentation

A represented commutator tested on one vector.

def commutatorVector (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H) (z : H) :
    A →ₗ[ℂ] H where
…

theorem OAI.KadisonKastler.positive_phase_word_drift line 36

Source documentation

Exact positive-word drift identity, before taking a sequence limit.

theorem positive_phase_word_drift
    (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H) (z : H)
    (e : ι → A) (v : A) (r : ℕ) (hr : r + 1 < q) :
    finiteRMS (fun θ : ι → ZMod q =>
      (T * ρ ((diagonalPhase e θ * v) ^ r * diagonalPhase e θ) -
        ρ ((diagonalPhase e θ * v) ^ r * diagonalPhase e θ) * T) z) =
      ‖WithLp.toLp 2 (fun s : Sym ι (r + 1) =>
        (T * ρ (positivePhaseCoefficient e v (r + 1) s) -
          ρ (positivePhaseCoefficient e v (r + 1) s) * T) z)‖ := by
…

Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.diagonalPhase, OAI.KadisonKastler.positivePhaseCoefficient

theorem OAI.KadisonKastler.negative_phase_word_drift line 62

Source documentation

The inverse characters give the negative-word drift identity.

theorem negative_phase_word_drift
    (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H) (z : H)
    (e : ι → A) (v : A) (r : ℕ) (hr : r + 1 < q) :
    finiteRMS (fun θ : ι → ZMod q =>
      (T * ρ ((star v * star (diagonalPhase e θ)) ^ (r + 1)) -
        ρ ((star v * star (diagonalPhase e θ)) ^ (r + 1)) * T) z) =
      ‖WithLp.toLp 2 (fun s : Sym ι (r + 1) =>
        (T * ρ (negativePhaseCoefficient e v (r + 1) s) -
          ρ (negativePhaseCoefficient e v (r + 1) s) * T) z)‖ := by
…

Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.diagonalPhase, OAI.KadisonKastler.negativePhaseCoefficient