ThroughLabel.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Counting projection words containing one prescribed label

The labels form actual finite multisets (Sym). Distinct multisets containing one label are counted by a binomial coefficient. Repeated multisets admit a uniform bound of twice the appropriate power of the alphabet size.

abbrev OAI.KadisonKastler.ThroughLabel line 23
Source documentation
Multisets containing a prescribed label.
```
abbrev ThroughLabel (a : α) (r : ℕ) := {s : Sym α r // a ∈ s}
```
abbrev OAI.KadisonKastler.DistinctThroughLabel line 26
Source documentation
Multisets containing a prescribed label, with no repeated label.
```
abbrev DistinctThroughLabel (a : α) (r : ℕ) :=
…
```
abbrev OAI.KadisonKastler.RepeatedThroughLabel line 30
Source documentation
Multisets containing a prescribed label and at least one repetition.
```
abbrev RepeatedThroughLabel (a : α) (r : ℕ) :=
…
```
def OAI.KadisonKastler.throughLabelEquiv line 34
Source documentation
Erasing one occurrence of the prescribed label.
```
def throughLabelEquiv (a : α) (r : ℕ) : ThroughLabel a (r + 1) ≃ Sym α r where
…
```
Mentions: OAI.KadisonKastler.ThroughLabel
theorem OAI.KadisonKastler.card_throughLabel line 40
def OAI.KadisonKastler.distinctThroughLabelEquiv line 45
Source documentation
Distinct multisets are exactly finite subsets with the same cardinality.
```
def distinctThroughLabelEquiv (a : α) (r : ℕ) :
    DistinctThroughLabel a r ≃ {s : Finset α // a ∈ s ∧ s.card = r} where
…
```
Mentions: OAI.KadisonKastler.DistinctThroughLabel
theorem OAI.KadisonKastler.card_distinctThroughLabel line 58
theorem OAI.KadisonKastler.card_sym_le_pow line 74
Source documentation
Stars-and-bars is bounded by the count of all ordered words.
```
theorem card_sym_le_pow [Nonempty α] (r : ℕ) :
    Fintype.card (Sym α r) ≤ Fintype.card α ^ r := by
…
```

theorem OAI.KadisonKastler.exists_repeated_pair line 83

Source documentation

A repeated multiset can be written with a repeated pair at its front.

theorem exists_repeated_pair {r : ℕ} (s : Sym α (r + 2))
    (hs : ¬ (s : Multiset α).Nodup) :
    ∃ b : α, ∃ t : Sym α r, s = Sym.cons b (Sym.cons b t) := by
…

def OAI.KadisonKastler.repeatedThroughCode line 102

Source documentation

Every repeated multiset through a is either aa followed by a remainder, or abb followed by a remainder.

def repeatedThroughCode (a : α) (r : ℕ) :
    Sym α (r + 1) ⊕ (α × Sym α r) → RepeatedThroughLabel a (r + 3)
  | Sum.inl t => ⟨Sym.cons a (Sym.cons a t), by
      simp [Sym.coe_cons, Multiset.nodup_cons]⟩
  | Sum.inr (b, t) => ⟨Sym.cons a (Sym.cons b (Sym.cons b t)), by
      simp [Sym.coe_cons, Multiset.nodup_cons]⟩

Mentions: OAI.KadisonKastler.RepeatedThroughLabel

theorem OAI.KadisonKastler.repeatedThroughCode_surjective line 109
theorem OAI.KadisonKastler.card_repeatedThroughLabel_add_three line 132
Source documentation
The repeated contribution loses one degree compared with all words.
```
theorem card_repeatedThroughLabel_add_three (a : α) (r : ℕ) :
    Fintype.card (RepeatedThroughLabel a (r + 3)) ≤ 2 * Fintype.card α ^ (r + 1) := by
…
```
Mentions: OAI.KadisonKastler.RepeatedThroughLabel
theorem OAI.KadisonKastler.card_repeatedThroughLabel_two line 145
Source documentation
There is exactly one repeated two-letter multiset through a.
```
theorem card_repeatedThroughLabel_two (a : α) :
    Fintype.card (RepeatedThroughLabel a 2) = 1 := by
…
```
Mentions: OAI.KadisonKastler.RepeatedThroughLabel
theorem OAI.KadisonKastler.card_repeatedThroughLabel line 166
Source documentation
A uniform repeated-label bound, including the length-two endpoint.
```
theorem card_repeatedThroughLabel (a : α) (r : ℕ) (hr : 2 ≤ r) :
    Fintype.card (RepeatedThroughLabel a r) ≤ 2 * Fintype.card α ^ (r - 2) := by
…
```
Mentions: OAI.KadisonKastler.RepeatedThroughLabel