OAI/Computability/DirectedFeedback/Games/UpperMobius.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Appendix.UpperMobius.upperQuotientEquiv line 26
  2. def OAI.DFVSGames.Appendix.UpperMobius.dualSubspaceEquiv line 30
  3. theorem OAI.DFVSGames.Appendix.UpperMobius.quotient_comap_codim line 36
  4. theorem OAI.DFVSGames.Appendix.UpperMobius.upperQuotientEquiv_codim line 47
  5. def OAI.DFVSGames.Appendix.UpperMobius.upperDualSubspaceEquiv line 56
  6. theorem OAI.DFVSGames.Appendix.UpperMobius.upperDualSubspaceEquiv_codim line 62
  7. def OAI.DFVSGames.Appendix.UpperMobius.upperWeightedTotal line 73
  8. theorem OAI.DFVSGames.Appendix.UpperMobius.upperWeightedTotal_eq_dual line 78
  9. theorem OAI.DFVSGames.Appendix.UpperMobius.quotient_finrank_zero_iff line 92
  10. theorem OAI.DFVSGames.Appendix.UpperMobius.binary_upper_interval_mobius line 105
  11. theorem OAI.DFVSGames.Appendix.DyadicError.pow_le_one_aux_inline_DyadicError line 120
  12. theorem OAI.DFVSGames.Appendix.DyadicError.pow_antitone_aux_inline_DyadicError line 128
  13. theorem OAI.DFVSGames.Appendix.DyadicError.half_power_le_quarter line 139
  14. def OAI.DFVSGames.Appendix.DyadicError.quarterSum line 152
  15. theorem OAI.DFVSGames.Appendix.DyadicError.quarterSum_nonneg line 154
  16. theorem OAI.DFVSGames.Appendix.DyadicError.quarterSum_residual line 158
  17. theorem OAI.DFVSGames.Appendix.DyadicError.quarterSum_le line 168
  18. def OAI.DFVSGames.Appendix.DyadicError.quarterError line 173
  19. theorem OAI.DFVSGames.Appendix.DyadicError.quarterError_add_one line 177
  20. theorem OAI.DFVSGames.Appendix.DyadicError.quarterError_le_seven_ninths line 215
  21. def OAI.DFVSGames.Appendix.DyadicError.dyadicError line 223
  22. theorem OAI.DFVSGames.Appendix.DyadicError.dyadicError_le_quarterError line 227
  23. theorem OAI.DFVSGames.Appendix.DyadicError.dyadicError_le_seven_ninths line 239
  24. theorem OAI.DFVSGames.Appendix.DyadicError.finite_dyadic_error_le_one line 244
  25. def OAI.DFVSGames.Appendix.BadConvolution.Incidence line 263
  26. def OAI.DFVSGames.Appendix.BadConvolution.Bad line 266
  27. def OAI.DFVSGames.Appendix.BadConvolution.filteredCoefficient line 270
  28. def OAI.DFVSGames.Appendix.BadConvolution.mobius line 274
  29. def OAI.DFVSGames.Appendix.BadConvolution.pairDimension line 276
  30. def OAI.DFVSGames.Appendix.BadConvolution.pairWeight line 279
  31. def OAI.DFVSGames.Appendix.BadConvolution.signedWeight line 282
  32. def OAI.DFVSGames.Appendix.BadConvolution.pieceConvolution line 288
  33. def OAI.DFVSGames.Appendix.BadConvolution.badConvolution line 292
  34. theorem OAI.DFVSGames.Appendix.BadConvolution.sum_masked_eq_subtype_inline_BadConvolution line 296
  35. theorem OAI.DFVSGames.Appendix.BadConvolution.pairDimension_eq_zero_iff line 306
  36. theorem OAI.DFVSGames.Appendix.BadConvolution.pairDimension_pos_iff line 317
  37. theorem OAI.DFVSGames.Appendix.BadConvolution.lower_mobius_sum line 321
  38. theorem OAI.DFVSGames.Appendix.BadConvolution.upper_mobius_sum line 331
  39. theorem OAI.DFVSGames.Appendix.BadConvolution.triple_incidence_iff_inline_BadConvolution line 342
  40. theorem OAI.DFVSGames.Appendix.BadConvolution.triple_mobius_sum line 350
  41. theorem OAI.DFVSGames.Appendix.BadConvolution.signed_triple_sum line 375
  42. theorem OAI.DFVSGames.Appendix.BadConvolution.badConvolution_expansion line 401
  43. theorem OAI.DFVSGames.Appendix.BadConvolution.card_lower_rank_le line 432
  44. theorem OAI.DFVSGames.Appendix.BadConvolution.card_upper_codim_le line 452
  45. theorem OAI.DFVSGames.Appendix.BadConvolution.finite_pair_level_sum_inline_BadConvolution line 475
  46. theorem OAI.DFVSGames.Appendix.BadConvolution.incident_pair_weight_le_one line 532
  47. theorem OAI.DFVSGames.Appendix.BadConvolution.mobius_sq line 583
  48. theorem OAI.DFVSGames.Appendix.BadConvolution.twice_choose_two_le_square_inline_BadConvolution line 590
  49. theorem OAI.DFVSGames.Appendix.BadConvolution.mobius_pair_sq_le line 597
  50. theorem OAI.DFVSGames.Appendix.BadConvolution.mobius_pair_weight_le line 609
  51. theorem OAI.DFVSGames.Appendix.BadConvolution.exists_nonzero_term_inline_BadConvolution line 619
  52. theorem OAI.DFVSGames.Appendix.BadConvolution.filteredCoefficient_nonzero_dimensions line 629
  53. theorem OAI.DFVSGames.Appendix.BadConvolution.pieceConvolution_nonzero_dimensions line 651
  54. theorem OAI.DFVSGames.Appendix.BadConvolution.rank_add_le line 664
  55. theorem OAI.DFVSGames.Appendix.BadConvolution.badConvolution_eq_zero_of_large_rank line 672
  56. theorem OAI.DFVSGames.Appendix.BadConvolution.scaled_product_inline_BadConvolution line 700
  57. theorem OAI.DFVSGames.Appendix.BadConvolution.badConvolution_sq_le line 709
  58. theorem OAI.DFVSGames.Appendix.BadConvolution.badConvolution_sq_sum_le line 784
  59. def OAI.DFVSGames.Appendix.A1Reduction.weakFourthSum line 828
  60. theorem OAI.DFVSGames.Appendix.A1Reduction.weakFourthSum_nonneg line 836
  61. theorem OAI.DFVSGames.Appendix.A1Reduction.linearCoeff_weakProjector line 845
  62. theorem OAI.DFVSGames.Appendix.A1Reduction.piece_fourth_moment line 854
  63. theorem OAI.DFVSGames.Appendix.A1Reduction.actual_bad_cover line 864
  64. theorem OAI.DFVSGames.Appendix.A1Reduction.badConvolution_zero_of_degree_zero line 874
  65. theorem OAI.DFVSGames.Appendix.A1Reduction.badConvolution_energy_le_weakFourthSum line 891
  66. theorem OAI.DFVSGames.Appendix.A1Reduction.fourth_moment_le_two line 905
  67. theorem OAI.DFVSGames.Appendix.A1Reduction.degree_reduction line 917