OAI/Combinatorics/IndependentSets/Expansion/Indicators.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.indicator line 15
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.mean_indicator line 17
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.energy_indicator line 25
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.indicator_nonnegative line 33
  5. def OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.cut line 40
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.cut_density_eq line 47
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.cut_density_ge_variance line 69
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.cut_density_ge_quarter line 88
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree line 104
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.degree_mul_card_le_four_cut line 121
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree_of_card_le_half line 130
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralCut.cut_card_ge_twice line 137