OAI/InformationTheory/Entanglement/CombinatorialNumbers.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteConstruction.Q line 9
  2. def OAI.FiniteConstruction.K line 10
  3. def OAI.FiniteConstruction.κ line 11
  4. def OAI.FiniteConstruction.L line 14
  5. lemma OAI.FiniteConstruction.L_def line 15
  6. def OAI.FiniteConstruction.D line 16
  7. def OAI.FiniteConstruction.m line 17
  8. lemma OAI.FiniteConstruction.base_card line 19
  9. lemma OAI.FiniteConstruction.b_pos line 34
  10. lemma OAI.FiniteConstruction.a₀_pos line 35
  11. lemma OAI.FiniteConstruction.choose_le_of_le_half line 42
  12. lemma OAI.FiniteConstruction.a₀_upper line 49
  13. lemma OAI.FiniteConstruction.central_eq line 56
  14. lemma OAI.FiniteConstruction.b_lower line 63
  15. lemma OAI.FiniteConstruction.binomial_term line 75
  16. lemma OAI.FiniteConstruction.arithmetic_gap line 85
  17. lemma OAI.FiniteConstruction.a₀_scaled_bound line 90
  18. lemma OAI.FiniteConstruction.strict_natural_gap line 95
  19. lemma OAI.FiniteConstruction.strict_gap line 113