OAI/Combinatorics/IndependentSets/Expansion/SpectralReturn.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean line 14
  2. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.energy line 16
  3. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.correlation line 18
  4. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.averagingOperator line 21
  5. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.iterateOperator line 24
  6. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeProfile line 29
  7. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.edgeDensity line 32
  8. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.markedStep line 35
  9. def OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.returnMass line 39
  10. structure OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.SpectralCertificate line 43
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_eq_sum_div_card line 54
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_equiv line 58
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_prod line 62
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_const line 67
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_add line 70
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_sub line 74
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_mul_left line 78
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_mul_right line 82
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_nonnegative line 86
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_mono line 89
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.energy_nonnegative line 92
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.correlation_sq_le line 95
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.energy_sub_const line 99
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.correlation_sub_const line 108
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_operator line 124
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.operator_sub_const line 134
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_iterate line 142
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.iterate_sub_const line 148
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.mean_markedStep line 155
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.returnMass_eq_correlation line 183
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.iterate_energy_bound line 190
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.zero_mean_correlation_bound line 205
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.SpectralReturn.correlation_centered line 220