OAI/Computability/UniqueGames/Analysis/BadConvolution.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

The signed bad-convolution term of Appendix A.1. The selector here is the weak image/kernel selector, prior to its separate A.4 decomposition.

  1. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.Incidence line 25
  2. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.Bad line 28
  3. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.filteredCoefficient line 32
  4. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.mobius line 36
  5. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.pairDimension line 38
  6. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.pairWeight line 41
  7. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.signedWeight line 44
  8. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.pieceConvolution line 50
  9. def OAI.UniqueGamesTheorem.Appendix.BadConvolution.badConvolution line 54
  10. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.sum_masked_eq_subtype line 58
  11. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.pairDimension_eq_zero_iff line 68
  12. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.pairDimension_pos_iff line 79
  13. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.lower_mobius_sum line 83
  14. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.upper_mobius_sum line 93
  15. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.triple_incidence_iff line 105
  16. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.triple_mobius_sum line 113
  17. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.signed_triple_sum line 138
  18. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.badConvolution_expansion line 165

    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.UniqueGamesTheorem.Appendix.BadConvolution.badConvolution, OAI.UniqueGamesTheorem.Appendix.BadConvolution.Incidence, OAI.UniqueGamesTheorem.Appendix.BadConvolution.signedWeight, OAI.UniqueGamesTheorem.Appendix.BadConvolution.pieceConvolution

  19. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.card_lower_rank_le line 196
  20. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.card_upper_codim_le line 215
  21. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.finite_pair_level_sum line 238
  22. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.incident_pair_weight_le_one line 294
  23. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.mobius_sq line 345
  24. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.twice_choose_two_le_square line 352
  25. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.mobius_pair_sq_le line 359
  26. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.mobius_pair_weight_le line 371
  27. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.exists_nonzero_term line 381
  28. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.filteredCoefficient_nonzero_dimensions line 392
  29. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.pieceConvolution_nonzero_dimensions line 414
  30. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.rank_add_le line 428
  31. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.badConvolution_eq_zero_of_large_rank line 436
  32. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.scaled_product line 464
  33. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.badConvolution_sq_le line 473
  34. theorem OAI.UniqueGamesTheorem.Appendix.BadConvolution.badConvolution_sq_sum_le line 549

    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.UniqueGamesTheorem.Appendix.BadConvolution.badConvolution, OAI.UniqueGamesTheorem.Appendix.BadConvolution.pieceConvolution