OAI/Computability/MaxCut/Games/UpperMobius.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Appendix.UpperMobius.upperQuotientEquiv line 25
2. def OAI.MaxCutGames.Appendix.UpperMobius.dualSubspaceEquiv line 29
3. theorem OAI.MaxCutGames.Appendix.UpperMobius.quotient_comap_codim line 35
4. theorem OAI.MaxCutGames.Appendix.UpperMobius.upperQuotientEquiv_codim line 46
5. def OAI.MaxCutGames.Appendix.UpperMobius.upperDualSubspaceEquiv line 55
6. theorem OAI.MaxCutGames.Appendix.UpperMobius.upperDualSubspaceEquiv_codim line 61
7. def OAI.MaxCutGames.Appendix.UpperMobius.upperWeightedTotal line 72
8. theorem OAI.MaxCutGames.Appendix.UpperMobius.upperWeightedTotal_eq_dual line 77
9. theorem OAI.MaxCutGames.Appendix.UpperMobius.quotient_finrank_zero_iff line 91
10. theorem OAI.MaxCutGames.Appendix.UpperMobius.binary_upper_interval_mobius line 104
11. theorem OAI.MaxCutGames.Appendix.DyadicError.pow_le_one_aux_inline_DyadicError line 117
12. theorem OAI.MaxCutGames.Appendix.DyadicError.pow_antitone_aux_inline_DyadicError line 125
13. theorem OAI.MaxCutGames.Appendix.DyadicError.half_power_le_quarter line 136
14. def OAI.MaxCutGames.Appendix.DyadicError.quarterSum line 149
15. theorem OAI.MaxCutGames.Appendix.DyadicError.quarterSum_nonneg line 151
16. theorem OAI.MaxCutGames.Appendix.DyadicError.quarterSum_residual line 155
17. theorem OAI.MaxCutGames.Appendix.DyadicError.quarterSum_le line 165
18. def OAI.MaxCutGames.Appendix.DyadicError.quarterError line 170
19. theorem OAI.MaxCutGames.Appendix.DyadicError.quarterError_add_one line 174
20. theorem OAI.MaxCutGames.Appendix.DyadicError.quarterError_le_seven_ninths line 212
21. def OAI.MaxCutGames.Appendix.DyadicError.dyadicError line 220
22. theorem OAI.MaxCutGames.Appendix.DyadicError.dyadicError_le_quarterError line 224
23. theorem OAI.MaxCutGames.Appendix.DyadicError.dyadicError_le_seven_ninths line 236
24. theorem OAI.MaxCutGames.Appendix.DyadicError.finite_dyadic_error_le_one line 241
25. def OAI.MaxCutGames.Appendix.BadConvolution.Incidence line 262
26. def OAI.MaxCutGames.Appendix.BadConvolution.Bad line 265
27. def OAI.MaxCutGames.Appendix.BadConvolution.filteredCoefficient line 269
28. def OAI.MaxCutGames.Appendix.BadConvolution.mobius line 273
29. def OAI.MaxCutGames.Appendix.BadConvolution.pairDimension line 275
30. def OAI.MaxCutGames.Appendix.BadConvolution.pairWeight line 278
31. def OAI.MaxCutGames.Appendix.BadConvolution.signedWeight line 281
32. def OAI.MaxCutGames.Appendix.BadConvolution.pieceConvolution line 287
33. def OAI.MaxCutGames.Appendix.BadConvolution.badConvolution line 291
34. theorem OAI.MaxCutGames.Appendix.BadConvolution.sum_masked_eq_subtype_inline_BadConvolution line 295
35. theorem OAI.MaxCutGames.Appendix.BadConvolution.pairDimension_eq_zero_iff line 305
36. theorem OAI.MaxCutGames.Appendix.BadConvolution.pairDimension_pos_iff line 316
37. theorem OAI.MaxCutGames.Appendix.BadConvolution.lower_mobius_sum line 320
38. theorem OAI.MaxCutGames.Appendix.BadConvolution.upper_mobius_sum line 330
39. theorem OAI.MaxCutGames.Appendix.BadConvolution.triple_incidence_iff_inline_BadConvolution line 341
40. theorem OAI.MaxCutGames.Appendix.BadConvolution.triple_mobius_sum line 349
41. theorem OAI.MaxCutGames.Appendix.BadConvolution.signed_triple_sum line 374
42. theorem OAI.MaxCutGames.Appendix.BadConvolution.badConvolution_expansion line 401

    Source documentation

    Exact Möbius expansion; no degree or positivity assumption is used.

    theorem badConvolution_expansion (a : (W →ₗ[F2] V) → ℝ) (X : W →ₗ[F2] V) :
        badConvolution a X =
          ∑ p : Submodule F2 V × Submodule F2 W,
            if Incidence p.1 p.2 X then signedWeight p * pieceConvolution p.1 p.2 a X else 0 := by
    …

    Mentions: OAI.MaxCutGames.Appendix.BadConvolution.badConvolution, OAI.MaxCutGames.Appendix.BadConvolution.Incidence, OAI.MaxCutGames.Appendix.BadConvolution.signedWeight, OAI.MaxCutGames.Appendix.BadConvolution.pieceConvolution

43. theorem OAI.MaxCutGames.Appendix.BadConvolution.card_lower_rank_le line 432
44. theorem OAI.MaxCutGames.Appendix.BadConvolution.card_upper_codim_le line 451
45. theorem OAI.MaxCutGames.Appendix.BadConvolution.finite_pair_level_sum_inline_BadConvolution line 474
46. theorem OAI.MaxCutGames.Appendix.BadConvolution.incident_pair_weight_le_one line 530
47. theorem OAI.MaxCutGames.Appendix.BadConvolution.mobius_sq line 581
48. theorem OAI.MaxCutGames.Appendix.BadConvolution.twice_choose_two_le_square_inline_BadConvolution line 588
49. theorem OAI.MaxCutGames.Appendix.BadConvolution.mobius_pair_sq_le line 595
50. theorem OAI.MaxCutGames.Appendix.BadConvolution.mobius_pair_weight_le line 607
51. theorem OAI.MaxCutGames.Appendix.BadConvolution.exists_nonzero_term_inline_BadConvolution line 617
52. theorem OAI.MaxCutGames.Appendix.BadConvolution.filteredCoefficient_nonzero_dimensions line 627
53. theorem OAI.MaxCutGames.Appendix.BadConvolution.pieceConvolution_nonzero_dimensions line 648
54. theorem OAI.MaxCutGames.Appendix.BadConvolution.rank_add_le line 661
55. theorem OAI.MaxCutGames.Appendix.BadConvolution.badConvolution_eq_zero_of_large_rank line 668
56. theorem OAI.MaxCutGames.Appendix.BadConvolution.scaled_product_inline_BadConvolution line 696
57. theorem OAI.MaxCutGames.Appendix.BadConvolution.badConvolution_sq_le line 705
58. theorem OAI.MaxCutGames.Appendix.BadConvolution.badConvolution_sq_sum_le line 781

    Source documentation

    The actual signed bad-convolution estimate of A.1.

    theorem badConvolution_sq_sum_le
        (a : (W →ₗ[F2] V) → ℝ) (d : ℕ) (hd : 1 ≤ d)
        (ha : ∀ Y, d < finrank F2 Y.range → a Y = 0) :
        (∑ X, badConvolution a X ^ 2) ≤
          ∑ p : Submodule F2 V × Submodule F2 W,
            if p ≠ (⊥,⊤) then (2:ℝ)^(7*d*(finrank F2 p.1 + finrank F2 (W ⧸ p.2))) *
              (∑ X, pieceConvolution p.1 p.2 a X ^ 2) else 0 := by
    …

    Mentions: OAI.MaxCutGames.Appendix.BadConvolution.badConvolution, OAI.MaxCutGames.Appendix.BadConvolution.pieceConvolution