ThroughLabelBounds.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform square sums of projection-word bounds

def OAI.KadisonKastler.projectionWordWeight line 17
Source documentation
The two projection-word estimates, written with a square-root denominator.
```
def projectionWordWeight {r : ℕ} (C : ℝ) (s : Sym α r) : ℝ :=
…
```
theorem OAI.KadisonKastler.projectionWordWeight_sq line 21

theorem OAI.KadisonKastler.sum_throughLabel_ite line 34

Source documentation

Summing a constant over each of the distinct and repeated parts.

theorem sum_throughLabel_ite (a : α) (r : ℕ) (D R : ℝ) :
    (∑ s : ThroughLabel a r, if (s.val : Multiset α).Nodup then D else R) =
      (Fintype.card (DistinctThroughLabel a r) : ℝ) * D +
        (Fintype.card (RepeatedThroughLabel a r) : ℝ) * R := by
…

Mentions: OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.DistinctThroughLabel, OAI.KadisonKastler.RepeatedThroughLabel

theorem OAI.KadisonKastler.factorial_mul_card_distinctThroughLabel_le line 60
Source documentation
The distinct multisets use at most one unit of the factorial-normalized budget.
```
theorem factorial_mul_card_distinctThroughLabel_le (a : α) (r : ℕ) (hr : 1 ≤ r) :
    (r - 1).factorial * Fintype.card (DistinctThroughLabel a r) ≤ Fintype.card α ^ (r - 1) := by
…
```
Mentions: OAI.KadisonKastler.DistinctThroughLabel
theorem OAI.KadisonKastler.sum_projectionWordWeight_sq_le line 68
Source documentation
The entire through-label square sum is bounded by 49 + 2C²/d.
```
theorem sum_projectionWordWeight_sq_le (a : α) (r : ℕ) (hr : 2 ≤ r) (C : ℝ) :
    (∑ s : ThroughLabel a r, projectionWordWeight C s.val ^ 2) ≤
      49 + 2 * C ^ 2 / Fintype.card α := by
…
```
Mentions: OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.projectionWordWeight
theorem OAI.KadisonKastler.sum_projectionWordWeight_sq_le_64 line 102
Source documentation
A fixed margin of fifteen absorbs all repeated-label words.
```
theorem sum_projectionWordWeight_sq_le_64 (a : α) (r : ℕ) (hr : 2 ≤ r) (C : ℝ)
    (hC : 2 * C ^ 2 ≤ 15 * Fintype.card α) :
    (∑ s : ThroughLabel a r, projectionWordWeight C s.val ^ 2) ≤ 64 := by
…
```
Mentions: OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.projectionWordWeight
theorem OAI.KadisonKastler.sum_projectionWordWeight_sq_one line 112
Source documentation
The one-letter contribution is already below the uniform budget.
```
theorem sum_projectionWordWeight_sq_one (a : α) (C : ℝ) :
    (∑ s : ThroughLabel a 1, projectionWordWeight C s.val ^ 2) = 49 := by
…
```
Mentions: OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.projectionWordWeight
theorem OAI.KadisonKastler.exists_uniform_projectionWordWeight_threshold line 126
Source documentation
One matrix-size threshold works simultaneously for every word length up to a prescribed bound. The constants for repeated words can depend on length.
```
theorem exists_uniform_projectionWordWeight_threshold (N : ℕ) (C : ℕ → ℝ) :
    ∃ D : ℕ, 0 < D ∧ ∀ d : ℕ, D ≤ d → ∀ r : ℕ, 1 ≤ r → r ≤ N →
      ∀ a : Fin d, (∑ s : ThroughLabel a r, projectionWordWeight (C r) s.val ^ 2) ≤ 64 := by
…
```
Mentions: OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.projectionWordWeight