OAI/Computability/DirectedFeedback/Analysis/MatrixEnergy.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.endomorphism_range_surjective line 61
  2. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.card_subspaces_le_endomorphisms line 67
  3. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.finite_color_space_inline_MatrixSubspaceCount line 79
  4. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.finite_endomorphisms_inline_MatrixSubspaceCount line 83
  5. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.finite_subspaces_inline_MatrixSubspaceCount line 87
  6. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.card_binary_subspaces_le line 91
  7. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.card_binary_subspaces_le_of_finrank_le line 98
  8. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.card_admissible_subspaces_le line 103
  9. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.card_color_admissible_subspaces_le line 109
  10. theorem OAI.DFVSGames.Fourier.MatrixSubspaceCount.card_color_admissible_subspaces_le_of_finrank_le line 115
  11. def OAI.DFVSGames.Fourier.MatrixEnergy.energy line 135
  12. def OAI.DFVSGames.Fourier.MatrixEnergy.cutoffEnergy line 138
  13. def OAI.DFVSGames.Fourier.MatrixEnergy.spectralEnergy line 143
  14. theorem OAI.DFVSGames.Fourier.MatrixEnergy.energy_nonneg line 146
  15. theorem OAI.DFVSGames.Fourier.MatrixEnergy.cutoffEnergy_nonneg line 151
  16. theorem OAI.DFVSGames.Fourier.MatrixEnergy.cutoffEnergy_le_energy line 165
  17. theorem OAI.DFVSGames.Fourier.MatrixEnergy.energy_split line 176
  18. theorem OAI.DFVSGames.Fourier.MatrixEnergy.spectralEnergy_le_cutoff_add line 190
  19. theorem OAI.DFVSGames.Fourier.MatrixEnergy.cutoffEnergy_gt_half line 221
  20. theorem OAI.DFVSGames.Fourier.MatrixEnergy.cutoffEnergy_le_twice_difference_add line 233
  21. theorem OAI.DFVSGames.Fourier.MatrixEnergy.deleted_energy_gt_eighth line 260
  22. theorem OAI.DFVSGames.Fourier.MatrixEnergy.boolean_energy_eq_mass line 269
  23. theorem OAI.DFVSGames.Fourier.MatrixEnergy.weighted_union_bound line 280
  24. theorem OAI.DFVSGames.Fourier.MatrixEnergy.exists_fixed_event line 304
  25. theorem OAI.DFVSGames.Fourier.MatrixEnergy.exists_fixed_event_scaled line 317
  26. def OAI.DFVSGames.Fourier.MatrixEnergy.linearRankOn line 341
  27. theorem OAI.DFVSGames.Fourier.MatrixEnergy.linearRankOn_top line 346
  28. theorem OAI.DFVSGames.Fourier.MatrixEnergy.linearRankOn_range line 362
  29. def OAI.DFVSGames.Fourier.MatrixEnergy.rankProjection line 380
  30. theorem OAI.DFVSGames.Fourier.MatrixEnergy.linearCoeff_sub line 388
  31. theorem OAI.DFVSGames.Fourier.MatrixEnergy.linearCoeff_rankProjection line 392
  32. theorem OAI.DFVSGames.Fourier.MatrixEnergy.rankProjection_parseval line 402
  33. theorem OAI.DFVSGames.Fourier.MatrixEnergy.rankProjection_contraction line 413
  34. theorem OAI.DFVSGames.Fourier.MatrixEnergy.rankProjection_orthogonal line 424
  35. theorem OAI.DFVSGames.Fourier.MatrixEnergy.linear_energy_parseval line 434
  36. theorem OAI.DFVSGames.Fourier.MatrixEnergy.linear_difference_energy_parseval line 439
  37. theorem OAI.DFVSGames.Fourier.MatrixEnergy.linear_deleted_energy_gt_eighth line 445
  38. def OAI.DFVSGames.Fourier.MatrixEnergy.colorIndicator line 459
  39. theorem OAI.DFVSGames.Fourier.MatrixEnergy.colorIndicator_partition line 463
  40. theorem OAI.DFVSGames.Fourier.MatrixEnergy.colorIndicator_parseval line 468
  41. def OAI.DFVSGames.Fourier.MatrixEnergy.labelingCoeff line 476
  42. theorem OAI.DFVSGames.Fourier.MatrixEnergy.labelingCoeff_energy_one line 480
  43. theorem OAI.DFVSGames.Fourier.MatrixEnergy.labeling_lowRank_energy line 493
  44. theorem OAI.DFVSGames.Fourier.MatrixEnergy.dependent_linear_energy_parseval line 523
  45. theorem OAI.DFVSGames.Fourier.MatrixEnergy.dependent_remainder_cutoff_le_eighth line 534
  46. theorem OAI.DFVSGames.Fourier.MatrixEnergy.dependent_deleted_energy_from_level line 562
  47. def OAI.DFVSGames.Fourier.MatrixEnergy.boolReal line 582
  48. theorem OAI.DFVSGames.Fourier.MatrixEnergy.boolReal_sq line 584
  49. theorem OAI.DFVSGames.Fourier.MatrixEnergy.boolReal_le_one line 587
  50. def OAI.DFVSGames.Fourier.MatrixEnergy.labelBool line 590
  51. theorem OAI.DFVSGames.Fourier.MatrixEnergy.labelBool_real line 594
  52. theorem OAI.DFVSGames.Fourier.MatrixEnergy.removed_boolReal line 599
  53. theorem OAI.DFVSGames.Fourier.MatrixEnergy.removed_difference_sq line 608
  54. def OAI.DFVSGames.Fourier.MatrixEnergy.questionEventMass line 619
  55. theorem OAI.DFVSGames.Fourier.MatrixEnergy.dependent_removed_union_bound line 624
  56. theorem OAI.DFVSGames.Fourier.MatrixEnergy.fixed_target_of_removed_mass line 660
  57. theorem OAI.DFVSGames.Fourier.MatrixEnergy.boolean_subpartition_energy_le_one line 676
  58. theorem OAI.DFVSGames.Fourier.MatrixEnergy.remainder_subpartition_energy_le_one line 704
  59. theorem OAI.DFVSGames.Fourier.MatrixEnergy.fixed_badRow_target_of_removed_mass line 727