OAI/Combinatorics/IndependentSets/Expansion/Profiles.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_edge_mean line 15
2. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeDensity_eq_card line 20
3. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeProfile_nonnegative line 28
4. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeProfile_le_one line 32
5. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeDensity_nonnegative line 40
6. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeDensity_le_one line 43
7. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeProfile_energy_le_density line 49
8. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeProfile_centered_energy line 56
9. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.returnMass_le_sharp line 65
10. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.returnMass_le line 81
11. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.adjacent_returnMass_le line 91
12. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.geometric_sum_le line 101
13. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.sum_returnMass_le line 114
14. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.triangular_returnMass_sum_le line 134
15. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.secondMoment_return_envelope line 152