OAI/Combinatorics/IndependentSets/Expansion/PoweringGap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringGap.gain_nonneg line 14
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringGap.uniform_count_gap line 23
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.Alphabet line 81
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.card_alphabet line 83
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.card_alphabet_eq_final line 86
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.center_eq line 89
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.walkLength_eq line 95
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.spectral_denominator_eq line 101
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.gain_eq line 105
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.gain_card_eq line 123
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.scaled_bound_eq line 129
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringFinalConstants.composed_scaled_gap line 139