OAI/Computability/DirectedFeedback/Games/SubmoduleInterval.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Appendix.SubmoduleInterval.lowerIntervalEquiv line 10
  2. def OAI.DFVSGames.Appendix.SubmoduleInterval.lowerIntervalSpaceEquiv line 39
  3. theorem OAI.DFVSGames.Appendix.SubmoduleInterval.lowerInterval_finrank line 49
  4. theorem OAI.DFVSGames.Appendix.SubmoduleInterval.sum_lowerInterval line 57
  5. def OAI.DFVSGames.Appendix.SubmoduleInterval.lowerWeightedTotal line 69
  6. theorem OAI.DFVSGames.Appendix.SubmoduleInterval.lowerWeightedTotal_eq line 74
  7. theorem OAI.DFVSGames.Appendix.SubmoduleInterval.binary_lower_interval_mobius line 85
  8. abbrev OAI.DFVSGames.Appendix.A13Index.Triple line 105
  9. def OAI.DFVSGames.Appendix.A13Index.weakA line 107
  10. def OAI.DFVSGames.Appendix.A13Index.weakB line 110
  11. theorem OAI.DFVSGames.Appendix.A13Index.recover_weakA line 113
  12. theorem OAI.DFVSGames.Appendix.A13Index.recover_weakB line 131
  13. theorem OAI.DFVSGames.Appendix.A13Index.canonicalValid line 144
  14. theorem OAI.DFVSGames.Appendix.A13Index.dim_weakA line 180
  15. theorem OAI.DFVSGames.Appendix.A13Index.codim_weakB line 203
  16. def OAI.DFVSGames.Appendix.A13Index.size line 218
  17. theorem OAI.DFVSGames.Appendix.A13Index.weak_order line 221
  18. theorem OAI.DFVSGames.Appendix.A13Index.order_eq_zero_iff line 229
  19. theorem OAI.DFVSGames.Appendix.A13Index.valid_positive_iff line 244
  20. abbrev OAI.DFVSGames.Appendix.A13Index.WeakPositive line 262
  21. abbrev OAI.DFVSGames.Appendix.A13Index.PositiveWitness line 265
  22. abbrev OAI.DFVSGames.Appendix.A13Index.PositiveTriple line 268
  23. abbrev OAI.DFVSGames.Appendix.A13Index.BoundedPositiveTriple line 270
  24. def OAI.DFVSGames.Appendix.A13Index.positiveMap line 273
  25. theorem OAI.DFVSGames.Appendix.A13Index.positiveMap_injective line 277
  26. def OAI.DFVSGames.Appendix.A13Index.positiveInverse line 297
  27. def OAI.DFVSGames.Appendix.A13Index.positiveEquiv line 303
  28. theorem OAI.DFVSGames.Appendix.A13Index.positiveMap_val line 310
  29. theorem OAI.DFVSGames.Appendix.A13Index.positiveEquiv_val line 313
  30. def OAI.DFVSGames.Appendix.A13Index.tripleFintype line 317
  31. def OAI.DFVSGames.Appendix.A13Index.weakPositiveFintype line 333
  32. def OAI.DFVSGames.Appendix.A13Index.geometricIndexFintype line 341
  33. def OAI.DFVSGames.Appendix.A13Index.positiveWitnessFintype line 349
  34. def OAI.DFVSGames.Appendix.A13Index.positiveTripleFintype line 357
  35. def OAI.DFVSGames.Appendix.A13Index.boundedPositiveTripleFintype line 364
  36. def OAI.DFVSGames.Appendix.TotalPredecessorCount.predecessorEnd line 380
  37. theorem OAI.DFVSGames.Appendix.TotalPredecessorCount.predecessorEnd_recovery line 390
  38. theorem OAI.DFVSGames.Appendix.TotalPredecessorCount.predecessorEnd_injective line 400
  39. theorem OAI.DFVSGames.Appendix.TotalPredecessorCount.card_predecessors_le line 414
  40. theorem OAI.DFVSGames.Fourier.MatrixProducts.linearTraceCharacter_re_add line 437
  41. theorem OAI.DFVSGames.Fourier.MatrixProducts.linearCoeff_mul_character line 446
  42. theorem OAI.DFVSGames.Fourier.MatrixProducts.linearCoeff_mul line 459
  43. def OAI.DFVSGames.Fourier.MatrixProducts.coefficientConvolution line 480
  44. theorem OAI.DFVSGames.Fourier.MatrixProducts.expect_fourth_eq_sum_convolution_sq line 483
  45. def OAI.DFVSGames.Appendix.F1Energy.rank line 508
  46. def OAI.DFVSGames.Appendix.F1Energy.Good line 510
  47. abbrev OAI.DFVSGames.Appendix.F1Energy.BoundedSplit line 513
  48. theorem OAI.DFVSGames.Appendix.F1Energy.add_self_cancel line 516
  49. def OAI.DFVSGames.Appendix.F1Energy.translate line 519
  50. theorem OAI.DFVSGames.Appendix.F1Energy.rank_le_of_rankBelow line 525
  51. theorem OAI.DFVSGames.Appendix.F1Energy.boundedSplit_rank line 529
  52. theorem OAI.DFVSGames.Appendix.F1Energy.good_of_trivial_intersections line 541
  53. theorem OAI.DFVSGames.Appendix.F1Energy.sum_translate line 575
  54. theorem OAI.DFVSGames.Appendix.F1Energy.card_bounded_splits_le line 579
  55. theorem OAI.DFVSGames.Appendix.F1Energy.card_predecessors_cast_le line 599
  56. def OAI.DFVSGames.Appendix.F1Energy.predecessorCoefficient line 608
  57. def OAI.DFVSGames.Appendix.F1Energy.gram line 611
  58. def OAI.DFVSGames.Appendix.F1Energy.predecessorEnergy line 614
  59. def OAI.DFVSGames.Appendix.F1Energy.goodConvolution line 617
  60. theorem OAI.DFVSGames.Appendix.F1Energy.predecessorCoefficient_nonneg line 621
  61. theorem OAI.DFVSGames.Appendix.F1Energy.gram_nonneg line 627
  62. theorem OAI.DFVSGames.Appendix.F1Energy.predecessorCoefficient_sq line 632
  63. theorem OAI.DFVSGames.Appendix.F1Energy.predecessor_energy_eq line 639
  64. theorem OAI.DFVSGames.Appendix.F1Energy.predecessor_energy_nonneg line 658
  65. theorem OAI.DFVSGames.Appendix.F1Energy.predecessor_energy_le line 662
  66. theorem OAI.DFVSGames.Appendix.F1Energy.goodConvolution_nonneg line 674
  67. theorem OAI.DFVSGames.Appendix.F1Energy.good_term_le line 680
  68. theorem OAI.DFVSGames.Appendix.F1Energy.goodConvolution_le_gram line 728
  69. theorem OAI.DFVSGames.Appendix.F1Energy.goodConvolution_sq_le line 744
  70. theorem OAI.DFVSGames.Appendix.F1Energy.split_gram_energy_le line 766
  71. theorem OAI.DFVSGames.Appendix.F1Energy.goodConvolution_energy_le line 783
  72. theorem OAI.DFVSGames.Appendix.F1Energy.abs_complement_sum_le line 806
  73. theorem OAI.DFVSGames.Appendix.F1Energy.convolution_split_square_le line 821
  74. theorem OAI.DFVSGames.Appendix.F1Energy.convolution_energy_le line 842
  75. theorem OAI.DFVSGames.Appendix.F1Energy.fourier_goodConvolution_energy_le line 862
  76. theorem OAI.DFVSGames.Appendix.F1Energy.fourth_moment_le_good_bad line 868