ConjugatedWords.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Phase coefficients as sums of words in conjugated copies

Removing the first label gives an exact decomposition of a prescribed multiset fibre. The phase-coefficient recursion is therefore precisely the sum of interleaved projection words. A unitary moves every intervening factor to the left and conjugates each projection by its remaining power.

theorem OAI.KadisonKastler.prescribed_head_mem line 25
theorem OAI.KadisonKastler.prescribed_tail line 31
def OAI.KadisonKastler.prescribedTupleHeadEquiv line 47
Source documentation
Splitting off the first position marks a label once, even when that label occurs several times in the prescribed multiset.
```
def prescribedTupleHeadEquiv {r : ℕ} (s : Sym α (r + 1)) :
    PrescribedLabelTuple s ≃
      Σ a : {a : α // a ∈ s}, PrescribedLabelTuple (s.erase a.val a.property) where
…
```
Mentions: OAI.KadisonKastler.PrescribedLabelTuple

theorem OAI.KadisonKastler.sum_prescribedTuple_head line 63

Source documentation

Exact head-and-tail reindexing, with no multiplicity factor.

theorem sum_prescribedTuple_head {B : Type*} [AddCommMonoid B] {r : ℕ}
    (s : Sym α (r + 1)) (f : (Fin (r + 1) → α) → B) :
    (∑ t : PrescribedLabelTuple s, f t.val) =
      ∑ a : {a : α // a ∈ s}, ∑ t : PrescribedLabelTuple (s.erase a.val a.property),
        f (Fin.cons a.val t.val) := by
…

Mentions: OAI.KadisonKastler.PrescribedLabelTuple

def OAI.KadisonKastler.interleavedWord line 77

Source documentation

The word e₀ v e₁ v ... v eᵣ₋₁, with an empty-word convention.

def interleavedWord (e : α → A) (v : A) : (r : ℕ) → (Fin r → α) → A
  | 0, _ => 1
  | r + 1, t => e (t 0) * (if r = 0 then 1 else v) *
      interleavedWord e v r (Fin.tail t)

/-- Every phase coefficient is exactly the sum over its prescribed
multiset, including repeated labels. -/

theorem OAI.KadisonKastler.positivePhaseCoefficient_eq_sum_interleaved line 84
Source documentation
Every phase coefficient is exactly the sum over its prescribed multiset, including repeated labels.
```
theorem positivePhaseCoefficient_eq_sum_interleaved (e : α → A) (v : A)
    (r : ℕ) (s : Sym α r) :
    positivePhaseCoefficient e v r s =
      ∑ t : PrescribedLabelTuple s, interleavedWord e v r t.val := by
…
```
Mentions: OAI.KadisonKastler.positivePhaseCoefficient, OAI.KadisonKastler.PrescribedLabelTuple, OAI.KadisonKastler.interleavedWord
def OAI.KadisonKastler.conjugatedCopy line 105
def OAI.KadisonKastler.conjugatedProjectionWord line 109
Source documentation
The ith letter is conjugated by the power remaining to its right.
```
def conjugatedProjectionWord (e : α → A) (v : A) {r : ℕ} (t : Fin r → α) : A :=
…
```
theorem OAI.KadisonKastler.conjugatedProjectionWord_succ line 113
theorem OAI.KadisonKastler.interleavedWord_eq_unitary_mul_conjugated line 130
Source documentation
Moving the intervening unitary factors to the left produces words in the conjugated copies, with no approximation.
```
theorem interleavedWord_eq_unitary_mul_conjugated (e : α → A) (v : A)
    (hv : v ∈ unitary A) (r : ℕ) (t : Fin r → α) :
    interleavedWord e v r t = v ^ (r - 1) * conjugatedProjectionWord e v t := by
…
```
Mentions: OAI.KadisonKastler.interleavedWord, OAI.KadisonKastler.conjugatedProjectionWord
theorem OAI.KadisonKastler.positivePhaseCoefficient_eq_unitary_mul_sum_conjugated line 149
theorem OAI.KadisonKastler.norm_positivePhaseCoefficient_eq_sum_conjugated line 165
Source documentation
The coefficient has exactly the norm of the corresponding sum of projection words in conjugated copies.
```
theorem norm_positivePhaseCoefficient_eq_sum_conjugated (e : α → A) (v : A)
    (hv : v ∈ unitary A) (r : ℕ) (s : Sym α r) :
    ‖positivePhaseCoefficient e v r s‖ =
      ‖∑ t : PrescribedLabelTuple s, conjugatedProjectionWord e v t.val‖ := by
…
```
Mentions: OAI.KadisonKastler.positivePhaseCoefficient, OAI.KadisonKastler.PrescribedLabelTuple, OAI.KadisonKastler.conjugatedProjectionWord
theorem OAI.KadisonKastler.norm_negativePhaseCoefficient_eq_positive line 174
Source documentation
The negative coefficient uses an adjoint and a unitary factor, so its norm is exactly the positive coefficient norm.
```
theorem norm_negativePhaseCoefficient_eq_positive (e : α → A) (v : A)
    (hv : v ∈ unitary A) (r : ℕ) (s : Sym α r) :
    ‖negativePhaseCoefficient e v r s‖ = ‖positivePhaseCoefficient e v r s‖ := by
…
```
Mentions: OAI.KadisonKastler.negativePhaseCoefficient, OAI.KadisonKastler.positivePhaseCoefficient
theorem OAI.KadisonKastler.norm_negativePhaseCoefficient_eq_sum_conjugated line 179