PhaseCoefficients.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Actual coefficients of the finite phase words

The coefficients are indexed by label multisets, so words with the same phase monomial are grouped before applying Parseval. Their supports are the sums of precisely the projections whose labels occur in the multiset.

def OAI.KadisonKastler.markedSymEquiv line 24
Source documentation
Removing one marked label identifies marked multisets with a label and a multiset of one smaller cardinality. The mark has no multiplicity.
```
def markedSymEquiv (r : ℕ) :
    (Σ s : Sym ι (r + 1), {a : ι // a ∈ s}) ≃ (ι × Sym ι r) :=
…
```
theorem OAI.KadisonKastler.sum_markedSym line 41
def OAI.KadisonKastler.phaseSupport line 50

def OAI.KadisonKastler.positivePhaseCoefficient line 54

Source documentation

The degree-zero convention allows the positive coefficients to be defined by removing a first label.

def positivePhaseCoefficient (e : ι → A) (v : A) : (r : ℕ) → Sym ι r → A
  | 0, _ => 1
  | r + 1, s => ∑ a : {a : ι // a ∈ s},
      e a.1 * (if r = 0 then 1 else v) * positivePhaseCoefficient e v r (s.erase a.1 a.2)

def OAI.KadisonKastler.positivePhaseProduct line 59
theorem OAI.KadisonKastler.positivePhaseCoefficient_mem line 63
theorem OAI.KadisonKastler.positivePhaseProduct_succ line 79
def OAI.KadisonKastler.diagonalPhase line 90
theorem OAI.KadisonKastler.positivePhase_expansion line 93
theorem OAI.KadisonKastler.positivePhase_power_expansion line 136
theorem OAI.KadisonKastler.phaseSupport_mul_label line 145
theorem OAI.KadisonKastler.label_mul_phaseSupport line 152
theorem OAI.KadisonKastler.positivePhaseCoefficient_left_support line 159
theorem OAI.KadisonKastler.positivePhaseCoefficient_right_support_of_subset line 173

theorem OAI.KadisonKastler.positivePhaseCoefficient_right_support line 195

Source documentation

Every positive coefficient has right support in its label multiset.

theorem positivePhaseCoefficient_right_support (e : ι → A) (v : A)
    (hmul : ∀ a b, e a * e b = if a = b then e a else 0)
    (r : ℕ) (s : Sym ι (r + 1)) :
    positivePhaseCoefficient e v (r + 1) s * phaseSupport e (s : Multiset ι) =
      positivePhaseCoefficient e v (r + 1) s :=
…

Mentions: OAI.KadisonKastler.positivePhaseCoefficient, OAI.KadisonKastler.phaseSupport

theorem OAI.KadisonKastler.phaseSupport_star line 207
def OAI.KadisonKastler.negativePhaseCoefficient line 211
theorem OAI.KadisonKastler.negativePhase_power_expansion line 214

theorem OAI.KadisonKastler.negativePhaseCoefficient_right_support line 229

Source documentation

Taking the adjoint switches the positive left support into the negative right support.

theorem negativePhaseCoefficient_right_support (e : ι → A) (v : A)
    (he : ∀ a, star (e a) = e a)
    (hmul : ∀ a b, e a * e b = if a = b then e a else 0)
    (r : ℕ) (s : Sym ι (r + 1)) :
    negativePhaseCoefficient e v (r + 1) s * phaseSupport e (s : Multiset ι) =
      negativePhaseCoefficient e v (r + 1) s := by
…

Mentions: OAI.KadisonKastler.negativePhaseCoefficient, OAI.KadisonKastler.phaseSupport

theorem OAI.KadisonKastler.diagonalPhase_mem_unitary line 239

theorem OAI.KadisonKastler.positivePhaseCoefficient_column_norm line 268

Source documentation

The actual positive word coefficients form an isometric column.

theorem positivePhaseCoefficient_column_norm (e : ι → H →L[ℂ] H)
    (he : ∀ a, star (e a) = e a)
    (hmul : ∀ a b, e a * e b = if a = b then e a else 0)
    (hsum : ∑ a, e a = 1) (v : H →L[ℂ] H) (hv : v ∈ unitary (H →L[ℂ] H))
    (r : ℕ) (hr : r + 1 < q) (x : H) :
    ‖WithLp.toLp 2 (fun s : Sym ι (r + 1) => positivePhaseCoefficient e v (r + 1) s x)‖ =
      ‖x‖ := by
…

Mentions: OAI.KadisonKastler.positivePhaseCoefficient

theorem OAI.KadisonKastler.negativePhaseCoefficient_column_norm line 287

Source documentation

The inverse phase characters give the same isometric column for the negative powers.

theorem negativePhaseCoefficient_column_norm (e : ι → H →L[ℂ] H)
    (he : ∀ a, star (e a) = e a)
    (hmul : ∀ a b, e a * e b = if a = b then e a else 0)
    (hsum : ∑ a, e a = 1) (v : H →L[ℂ] H) (hv : v ∈ unitary (H →L[ℂ] H))
    (r : ℕ) (hr : r + 1 < q) (x : H) :
    ‖WithLp.toLp 2 (fun s : Sym ι (r + 1) => negativePhaseCoefficient e v (r + 1) s x)‖ =
      ‖x‖ := by
…

Mentions: OAI.KadisonKastler.negativePhaseCoefficient