PrescribedWordBounds.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual free-word bounds with the prescribed-multiset indexing

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_prescribed_projectionWords_le line 22
Source documentation
Both cases of the prescribed-multiset word estimate, with the factorial counting proved for the actual indexing type.
```
theorem norm_prescribed_projectionWords_le (M : FreeDiagonalModel ι α H)
    {r : ℕ} (hr : 1 ≤ r) (hd : freeWordThreshold r ≤ Fintype.card α)
    (s : Sym α r) (position : Fin r → ι) (hposition : Function.Injective position) :
    ‖∑ t : PrescribedLabelTuple s, M.projectionWord position t.val‖ ≤
      projectionWordWeight (freeWordC r) s := by
…
```
Mentions: OAI.KadisonKastler.FreeDiagonalModel, OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.PrescribedLabelTuple, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC
theorem OAI.KadisonKastler.exists_uniform_freeProjection_threshold line 40
Source documentation
One threshold supplies both all word estimates and the through-label square-sum estimate for the finitely many lengths in the application.
```
theorem exists_uniform_freeProjection_threshold (N : ℕ) :
    ∃ D : ℕ, 0 < D ∧ ∀ d : ℕ, D ≤ d → ∀ r : ℕ, 1 ≤ r → r ≤ N →
      freeWordThreshold r ≤ d ∧
        ∀ a : Fin d, (∑ s : ThroughLabel a r, projectionWordWeight (freeWordC r) s.val ^ 2) ≤ 64 := by
…
```
Mentions: OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC