OAI/Analysis/KadisonKastler/WordBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The uniform binomial estimate for free-word cuts

This supplies the numerical estimate used to sum the preservation cuts in §3 of the manuscript. Its bound is independent of the word length.

  1. theorem OAI.KadisonKastler.choose_monotone_to_half line 20
  2. theorem OAI.KadisonKastler.choose_two_le_interior line 27
  3. theorem OAI.KadisonKastler.inv_sqrt_choose_interior line 34
  4. theorem OAI.KadisonKastler.sum_split_four line 48
  5. theorem OAI.KadisonKastler.sum_inv_sqrt_choose_le_five line 60

    Source documentation

    The sum of the inverse square roots of one row of Pascal's triangle is at most five, uniformly in that row. This is the preservation-cut constant in the free projection-word estimate.

    theorem sum_inv_sqrt_choose_le_five (m : ℕ) :
    (∑ p ∈ range (m + 1), 1 / Real.sqrt (m.choose p : ℝ)) ≤ 5 := by
…