OAI/Computability/BinPacking/Expanders/PreprocessingTableSpectral.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.PCP.LazySpectral.half_sum_sq_le line 14
2. theorem OAI.BinPackingGames.Foundations.PCP.LazySpectral.lazy_energy_le_average line 17
3. theorem OAI.BinPackingGames.Foundations.PCP.LazySpectral.lazy_energy_bound line 39
4. theorem OAI.BinPackingGames.Foundations.PCP.LazySpectral.lazy_certificate_31_32 line 52
5. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.portGraph_ext line 70
6. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.materialize_portGraph line 78
7. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.overlay_portGraph line 88
8. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.overlay_rotation_eq line 98
9. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.lazy_portGraph line 107
10. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.lazy_rotation_eq line 115
11. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.overlay_certificate_seven_eighths line 123
12. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTableSpectral.lazy_certificate_31_32 line 139