OAI/Combinatorics/IndependentSets/Expansion/LazySpectral.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySpectral.half_sum_sq_le line 16
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySpectral.lazy_energy_le_average line 19
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySpectral.lazy_energy_bound line 41
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySpectral.lazy_certificate_31_32 line 54
  5. abbrev OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.Vertex line 73
  6. abbrev OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.OverlayPort line 74
  7. abbrev OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.Port line 75
  8. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.degree line 77
  9. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.sizeFactor line 78
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.card_lazy_sum line 80
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.doubled_add line 85
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.degree_eq_card line 87
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.degree_positive line 96
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.sizeFactor_positive line 100
  15. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.paddedGraph line 105
  16. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.overlayExpander line 109
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.overlayExpander_certificate line 116
  18. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.overlayGraph line 120
  19. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.graph line 124
  20. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.portGraph line 128
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.graph_tail line 132
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.graph_reverse line 135
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.accepts_reverse line 139
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.portGraph_eq_lazyGraph line 144
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.overlayGraph_certificate line 148
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.spectral_certificate line 157
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.vertex_count_le line 163
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.dart_count line 173
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.dart_count_le line 178
  30. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.liftLabel line 186
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.lift_rejectionCount line 190
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.completeness line 201
  33. def OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.roundLabels line 208
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.soundness line 212
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.satisfiable_iff line 225
  36. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.gap_transfer line 237
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.Preprocessing.gap_transfer_real line 253