LabelCharacters.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Root-of-unity phases indexed by label multisets

The phase space is a finite product of cyclic groups. A multiset gives its character by pairing the phase coordinates with its multiplicities. If the word length is less than the root order, no multiplicity can wrap around, so distinct multisets give orthogonal characters.

def OAI.KadisonKastler.labelDot line 25
def OAI.KadisonKastler.multisetCharacter line 30
theorem OAI.KadisonKastler.labelDot_single line 35
theorem OAI.KadisonKastler.multisetCharacter_single line 40
theorem OAI.KadisonKastler.labelDot_zero line 46
theorem OAI.KadisonKastler.labelDot_cons line 50
theorem OAI.KadisonKastler.multisetCharacter_cons line 56
theorem OAI.KadisonKastler.multisetCharacter_eq_prod line 61
Source documentation
This is exactly the phase monomial, including label multiplicities.
```
theorem multisetCharacter_eq_prod (s : Multiset ι) (θ : ι → ZMod q) :
    multisetCharacter s θ = (s.map (fun a => ZMod.stdAddChar (θ a))).prod := by
…
```
Mentions: OAI.KadisonKastler.multisetCharacter
theorem OAI.KadisonKastler.multisetCharacter_injective line 68
Source documentation
A root order larger than the word length separates all label multisets.
```
theorem multisetCharacter_injective {r : ℕ} (hr : r < q) :
    Function.Injective (fun s : Sym ι r => multisetCharacter (q := q) (s : Multiset ι)) := by
…
```
Mentions: OAI.KadisonKastler.multisetCharacter
theorem OAI.KadisonKastler.multiset_phases_mean_square line 84

theorem OAI.KadisonKastler.negative_multiset_phases_mean_square line 92

Source documentation

The inverse characters implement the negative phase monomials.

theorem negative_multiset_phases_mean_square {H : Type*} [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] {r : ℕ} (hr : r < q) (v : Sym ι r → H) :
    (𝔼 θ : ι → ZMod q,
      ‖finitePhaseSum (fun s : Sym ι r =>
        ⇑((multisetCharacter (q := q) (s : Multiset ι))⁻¹ : AddChar (ι → ZMod q) ℂ)) v θ‖ ^ 2) =
…

Mentions: OAI.KadisonKastler.finitePhaseSum, OAI.KadisonKastler.multisetCharacter