OAI/Computability/MaxCut/Games/SubmoduleInterval.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Actual reindexing of Appendix A.4 geometric witnesses by their raw triples. The original nonzero weak-pair condition is equivalent to positive total restriction order plus frequency rank.

  1. def OAI.MaxCutGames.Appendix.SubmoduleInterval.lowerIntervalEquiv line 10
  2. def OAI.MaxCutGames.Appendix.SubmoduleInterval.lowerIntervalSpaceEquiv line 39
  3. theorem OAI.MaxCutGames.Appendix.SubmoduleInterval.lowerInterval_finrank line 49
  4. theorem OAI.MaxCutGames.Appendix.SubmoduleInterval.sum_lowerInterval line 57
  5. def OAI.MaxCutGames.Appendix.SubmoduleInterval.lowerWeightedTotal line 69
  6. theorem OAI.MaxCutGames.Appendix.SubmoduleInterval.lowerWeightedTotal_eq line 74
  7. theorem OAI.MaxCutGames.Appendix.SubmoduleInterval.binary_lower_interval_mobius line 85
  8. abbrev OAI.MaxCutGames.Appendix.A13Index.Triple line 109
  9. def OAI.MaxCutGames.Appendix.A13Index.weakA line 111
  10. def OAI.MaxCutGames.Appendix.A13Index.weakB line 114
  11. theorem OAI.MaxCutGames.Appendix.A13Index.recover_weakA line 117
  12. theorem OAI.MaxCutGames.Appendix.A13Index.recover_weakB line 135
  13. theorem OAI.MaxCutGames.Appendix.A13Index.canonicalValid line 148
  14. theorem OAI.MaxCutGames.Appendix.A13Index.dim_weakA line 184
  15. theorem OAI.MaxCutGames.Appendix.A13Index.codim_weakB line 207
  16. def OAI.MaxCutGames.Appendix.A13Index.size line 222
  17. theorem OAI.MaxCutGames.Appendix.A13Index.weak_order line 225
  18. theorem OAI.MaxCutGames.Appendix.A13Index.order_eq_zero_iff line 233
  19. theorem OAI.MaxCutGames.Appendix.A13Index.valid_positive_iff line 248
  20. abbrev OAI.MaxCutGames.Appendix.A13Index.WeakPositive line 266
  21. abbrev OAI.MaxCutGames.Appendix.A13Index.PositiveWitness line 269
  22. abbrev OAI.MaxCutGames.Appendix.A13Index.PositiveTriple line 272
  23. abbrev OAI.MaxCutGames.Appendix.A13Index.BoundedPositiveTriple line 274
  24. def OAI.MaxCutGames.Appendix.A13Index.positiveMap line 277
  25. theorem OAI.MaxCutGames.Appendix.A13Index.positiveMap_injective line 281
  26. def OAI.MaxCutGames.Appendix.A13Index.positiveInverse line 301
  27. def OAI.MaxCutGames.Appendix.A13Index.positiveEquiv line 307
  28. theorem OAI.MaxCutGames.Appendix.A13Index.positiveMap_val line 314
  29. theorem OAI.MaxCutGames.Appendix.A13Index.positiveEquiv_val line 317
  30. def OAI.MaxCutGames.Appendix.A13Index.tripleFintype line 321
  31. def OAI.MaxCutGames.Appendix.A13Index.weakPositiveFintype line 337
  32. def OAI.MaxCutGames.Appendix.A13Index.geometricIndexFintype line 345
  33. def OAI.MaxCutGames.Appendix.A13Index.positiveWitnessFintype line 353
  34. def OAI.MaxCutGames.Appendix.A13Index.positiveTripleFintype line 361
  35. def OAI.MaxCutGames.Appendix.A13Index.boundedPositiveTripleFintype line 368
  36. def OAI.MaxCutGames.Appendix.TotalPredecessorCount.predecessorEnd line 384
  37. theorem OAI.MaxCutGames.Appendix.TotalPredecessorCount.predecessorEnd_recovery line 394
  38. theorem OAI.MaxCutGames.Appendix.TotalPredecessorCount.predecessorEnd_injective line 404
  39. theorem OAI.MaxCutGames.Appendix.TotalPredecessorCount.card_predecessors_le line 418
  40. theorem OAI.MaxCutGames.Fourier.MatrixProducts.linearTraceCharacter_re_add line 444

    Source documentation

    Multiplication of the real binary trace characters.

    theorem linearTraceCharacter_re_add (S T : F →ₗ[F2] E) (X : E →ₗ[F2] F) :
    (linearTraceCharacter (S + T) X).re =
      (linearTraceCharacter S X).re * (linearTraceCharacter T X).re := by
…
  41. theorem OAI.MaxCutGames.Fourier.MatrixProducts.linearCoeff_mul_character line 454

    Source documentation

    Multiplication by a trace character translates frequency.

    theorem linearCoeff_mul_character (f : (E →ₗ[F2] F) → ℝ)
    (S T : F →ₗ[F2] E) :
    linearCoeff (fun X => f X * (linearTraceCharacter T X).re) S =
      linearCoeff f (S + T) := by
…
  42. theorem OAI.MaxCutGames.Fourier.MatrixProducts.linearCoeff_mul line 468

    Source documentation

    Products transform to counting-measure convolution of normalized coefficients.

    theorem linearCoeff_mul (f g : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) :
    linearCoeff (fun X => f X * g X) S =
      ∑ T : F →ₗ[F2] E, linearCoeff f T * linearCoeff g (S + T) := by
…
  43. def OAI.MaxCutGames.Fourier.MatrixProducts.coefficientConvolution line 490

    Source documentation

    Frequency convolution, with counting measure on the frequency space.

    def coefficientConvolution (f g : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) : ℝ :=
…
  44. theorem OAI.MaxCutGames.Fourier.MatrixProducts.expect_fourth_eq_sum_convolution_sq line 494

    Source documentation

    The actual fourth moment equals the squared coefficient-convolution mass.

    theorem expect_fourth_eq_sum_convolution_sq (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, f X ^ 4) =
      ∑ S : F →ₗ[F2] E, coefficientConvolution f f S ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Fourier.MatrixProducts.coefficientConvolution

  45. def OAI.MaxCutGames.Appendix.F1Energy.rank line 520
  46. def OAI.MaxCutGames.Appendix.F1Energy.Good line 522
  47. abbrev OAI.MaxCutGames.Appendix.F1Energy.BoundedSplit line 525
  48. theorem OAI.MaxCutGames.Appendix.F1Energy.add_self_cancel line 528
  49. def OAI.MaxCutGames.Appendix.F1Energy.translate line 531
  50. theorem OAI.MaxCutGames.Appendix.F1Energy.rank_le_of_rankBelow line 537
  51. theorem OAI.MaxCutGames.Appendix.F1Energy.boundedSplit_rank line 541
  52. theorem OAI.MaxCutGames.Appendix.F1Energy.good_of_trivial_intersections line 553

    Source documentation

    The checked geometric cover supplies exactly the F1 witness condition.

    theorem good_of_trivial_intersections (X Y : G)
    (hi : (X.range ⊓ Y.range) ⊓ (X+Y).range = ⊥)
    (hk : X.ker ⊔ Y.ker ⊔ (X+Y).ker = ⊤) : Good X Y := by
…

    Mentions: OAI.MaxCutGames.Appendix.F1Energy.Good

  53. theorem OAI.MaxCutGames.Appendix.F1Energy.sum_translate line 587
  54. theorem OAI.MaxCutGames.Appendix.F1Energy.card_bounded_splits_le line 591
  55. theorem OAI.MaxCutGames.Appendix.F1Energy.card_predecessors_cast_le line 611
  56. def OAI.MaxCutGames.Appendix.F1Energy.predecessorCoefficient line 620
  57. def OAI.MaxCutGames.Appendix.F1Energy.gram line 623
  58. def OAI.MaxCutGames.Appendix.F1Energy.predecessorEnergy line 626
  59. def OAI.MaxCutGames.Appendix.F1Energy.goodConvolution line 629
  60. theorem OAI.MaxCutGames.Appendix.F1Energy.predecessorCoefficient_nonneg line 633
  61. theorem OAI.MaxCutGames.Appendix.F1Energy.gram_nonneg line 639
  62. theorem OAI.MaxCutGames.Appendix.F1Energy.predecessorCoefficient_sq line 644
  63. theorem OAI.MaxCutGames.Appendix.F1Energy.predecessor_energy_eq line 651
  64. theorem OAI.MaxCutGames.Appendix.F1Energy.predecessor_energy_nonneg line 670
  65. theorem OAI.MaxCutGames.Appendix.F1Energy.predecessor_energy_le line 674
  66. theorem OAI.MaxCutGames.Appendix.F1Energy.goodConvolution_nonneg line 686
  67. theorem OAI.MaxCutGames.Appendix.F1Energy.good_term_le line 694

    Source documentation

    Each supported good term has a bounded split witness. Its summand is counted with shared residual C=Y+R; all other summands are nonnegative.

    theorem good_term_le (a : G → ℝ) (d : ℕ)
    (hdegree : ∀ Y, d < rank Y → a Y = 0) (X Y : G) :
    (if Good X Y then |a Y| * |a (X+Y)| else 0) ≤
      ∑ R : BoundedSplit d X,
        predecessorCoefficient a R.val (Y+R.val) *
          predecessorCoefficient a (X+R.val) (Y+R.val) := by
…

    Mentions: OAI.MaxCutGames.Appendix.F1Energy.rank, OAI.MaxCutGames.Appendix.F1Energy.Good, OAI.MaxCutGames.Appendix.F1Energy.BoundedSplit, OAI.MaxCutGames.Appendix.F1Energy.predecessorCoefficient

  68. theorem OAI.MaxCutGames.Appendix.F1Energy.goodConvolution_le_gram line 742
  69. theorem OAI.MaxCutGames.Appendix.F1Energy.goodConvolution_sq_le line 758
  70. theorem OAI.MaxCutGames.Appendix.F1Energy.split_gram_energy_le line 780
  71. theorem OAI.MaxCutGames.Appendix.F1Energy.goodConvolution_energy_le line 797
  72. theorem OAI.MaxCutGames.Appendix.F1Energy.abs_complement_sum_le line 821

    Source documentation

    The complement of any bad event covered by Good is bounded without changing the signs of the coefficients in the bad part.

    theorem abs_complement_sum_le (a : G → ℝ) (X : G) (bad : G → Prop)
    (hcover : ∀ Y, ¬ bad Y → Good X Y) :
    |∑ Y, if bad Y then 0 else a Y * a (X+Y)| ≤ goodConvolution a X := by
…

    Mentions: OAI.MaxCutGames.Appendix.F1Energy.Good, OAI.MaxCutGames.Appendix.F1Energy.goodConvolution

  73. theorem OAI.MaxCutGames.Appendix.F1Energy.convolution_split_square_le line 836
  74. theorem OAI.MaxCutGames.Appendix.F1Energy.convolution_energy_le line 857
  75. theorem OAI.MaxCutGames.Appendix.F1Energy.fourier_goodConvolution_energy_le line 877
  76. theorem OAI.MaxCutGames.Appendix.F1Energy.fourth_moment_le_good_bad line 885

    Source documentation

    The actual fourth-moment identity reduced to the remaining signed bad convolution. Its geometric cover is supplied by good_of_trivial_intersections.

    theorem fourth_moment_le_good_bad (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y : F →ₗ[F2] E, d < rank Y → linearCoeff f Y = 0)
    (bad : (F →ₗ[F2] E) → (F →ₗ[F2] E) → Prop)
    (hcover : ∀ X Y, ¬ bad X Y → Good X Y) :
    (𝔼 X, f X^4) ≤ 2 * ((2:ℝ)^(6*d^2) * (𝔼 X, f X^2)^2) +
      2 * ∑ X, (∑ Y, if bad X Y then linearCoeff f Y * linearCoeff f (X+Y) else 0)^2 := by
…

    Mentions: OAI.MaxCutGames.Appendix.F1Energy.rank, OAI.MaxCutGames.Appendix.F1Energy.Good