OAI/Analysis/KadisonKastler/FactorialCuts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Summing the factorial factors in the preservation cuts

  1. theorem OAI.KadisonKastler.sqrt_factorial_product_eq_div_sqrt_choose line 11
  2. theorem OAI.KadisonKastler.sum_sqrt_factorial_products line 28
  3. theorem OAI.KadisonKastler.sum_sqrt_factorial_products_le_five line 39