OAI/Computability/UniqueGames/Analysis/A13IndexLemmas.lean

GitHub source file

63 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. abbrev OAI.UniqueGamesTheorem.Appendix.A13Index.Triple line 32
  2. def OAI.UniqueGamesTheorem.Appendix.A13Index.weakA line 34
  3. def OAI.UniqueGamesTheorem.Appendix.A13Index.weakB line 37
  4. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.recover_weakA line 40
  5. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.recover_weakB line 58
  6. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.canonicalValid line 71
  7. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.dim_weakA line 107
  8. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.codim_weakB line 130
  9. def OAI.UniqueGamesTheorem.Appendix.A13Index.size line 145
  10. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.weak_order line 148
  11. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.order_eq_zero_iff line 156
  12. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.valid_positive_iff line 171
  13. abbrev OAI.UniqueGamesTheorem.Appendix.A13Index.WeakPositive line 189
  14. abbrev OAI.UniqueGamesTheorem.Appendix.A13Index.PositiveWitness line 192
  15. abbrev OAI.UniqueGamesTheorem.Appendix.A13Index.PositiveTriple line 195
  16. abbrev OAI.UniqueGamesTheorem.Appendix.A13Index.BoundedPositiveTriple line 197
  17. def OAI.UniqueGamesTheorem.Appendix.A13Index.positiveMap line 200
  18. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.positiveMap_injective line 204
  19. def OAI.UniqueGamesTheorem.Appendix.A13Index.positiveInverse line 224
  20. def OAI.UniqueGamesTheorem.Appendix.A13Index.positiveEquiv line 230
  21. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.positiveMap_val line 237
  22. theorem OAI.UniqueGamesTheorem.Appendix.A13Index.positiveEquiv_val line 240
  23. def OAI.UniqueGamesTheorem.Appendix.A13Index.tripleFintype line 244
  24. def OAI.UniqueGamesTheorem.Appendix.A13Index.weakPositiveFintype line 260
  25. def OAI.UniqueGamesTheorem.Appendix.A13Index.geometricIndexFintype line 268
  26. def OAI.UniqueGamesTheorem.Appendix.A13Index.positiveWitnessFintype line 276
  27. def OAI.UniqueGamesTheorem.Appendix.A13Index.positiveTripleFintype line 284
  28. def OAI.UniqueGamesTheorem.Appendix.A13Index.boundedPositiveTripleFintype line 291
  29. def OAI.UniqueGamesTheorem.Appendix.LevelInequality.IsBoolean line 319
  30. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_nonneg line 322
  31. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_sq line 326
  32. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_positive_moment line 329
  33. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_squared_norm_eq_density line 335
  34. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_four_thirds_moment line 339
  35. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_holder_fourth line 345
  36. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.fourth_power_le_implies_le line 377

    Source documentation

    The fourth-root conversion used in the final displayed inequality. This is an elementary real estimate, independent of Fourier analysis.

    theorem fourth_power_le_implies_le {a b : ℝ} (_ha : 0 ≤ a) (hb : 0 ≤ b)
    (h : a ^ 4 ≤ b ^ 4) : a ≤ b := by
…
  37. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_level_bound_of_fourth_moment line 387

    Source documentation

    Once the genuine fourth-moment estimate has been established, this proves the final Boolean Hölder implication. The fourth-moment estimate is an explicit hypothesis here; this lemma itself is not Theorem 2.3.

    theorem boolean_level_bound_of_fourth_moment {f h : α → ℝ}
    (hf : IsBoolean f) (d : ℕ) (η : ℝ) (hη : 0 ≤ η)
    (hprojection : (𝔼 x, h x ^ 2) = 𝔼 x, h x * f x)
    (hfourth : (𝔼 x, h x ^ 4) ≤ (2 : ℝ) ^ (113 * d * d) * η * (𝔼 x, f x)) :
    (𝔼 x, h x ^ 2) ≤
      (2 : ℝ) ^ (30 * d * d) * η ^ ((1 : ℝ) / 4) * (𝔼 x, f x ^ 2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.LevelInequality.IsBoolean

  38. def OAI.UniqueGamesTheorem.Appendix.LevelInequality.frequencyRank line 439

    Source documentation

    The actual rank of a Fourier index S : F → E.

    def frequencyRank (S : F →ₗ[F2] E) : ℕ := Module.finrank F2 (LinearMap.range S)
  39. def OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel line 441
  40. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.linearCoeff_rankLevel line 445
  41. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel_energy line 456

    Source documentation

    The selected rank mass equals the normalized squared norm of the actual rank projection.

    theorem rankLevel_energy (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankLevel d f X ^ 2) =
      ∑ S with frequencyRank S = d, linearCoeff f S ^ 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel, OAI.UniqueGamesTheorem.Appendix.LevelInequality.frequencyRank

  42. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel_inner_self line 465

    Source documentation

    Orthogonal-projection identity used in the final Hölder step.

    theorem rankLevel_inner_self (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankLevel d f X ^ 2) = 𝔼 X, rankLevel d f X * f X := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel

  43. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel_energy_le line 475

    Source documentation

    Rank projection contracts the normalized L2 norm.

    theorem rankLevel_energy_le (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankLevel d f X ^ 2) ≤ 𝔼 X, f X ^ 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel

  44. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel_degree_le line 482
  45. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.rankLevel_bound_of_fourth_moment line 487
  46. def OAI.UniqueGamesTheorem.Appendix.LevelInequality.IsRestrictionGlobal line 498
  47. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_restriction line 505
  48. theorem OAI.UniqueGamesTheorem.Appendix.LevelInequality.boolean_global_iff_density line 515

    Source documentation

    On Boolean functions the restriction-global norm bound is exactly the restriction-density hypothesis in Theorem 2.3.

    theorem boolean_global_iff_density (f : (E →ₗ[F2] F) → ℝ) (hf : IsBoolean f)
    (d : ℕ) (η : ℝ) :
    IsRestrictionGlobal f d η ↔
      ∀ (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F),
        UniqueGamesTheorem.Fourier.MatrixRestrictions.order A B ≤ d →
          (𝔼 N, UniqueGamesTheorem.Fourier.MatrixRestrictions.restrict f A B T N) ≤ η := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.LevelInequality.IsBoolean, OAI.UniqueGamesTheorem.Appendix.LevelInequality.IsRestrictionGlobal, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.order, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.restrict

  49. def OAI.UniqueGamesTheorem.Appendix.LevelInequality.Theorem23 line 524
  50. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.absorption line 555
  51. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.geometric_sum_le line 579
  52. def OAI.UniqueGamesTheorem.Appendix.A5Scalar.positiveSum line 588
  53. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.pair_sum_factor line 592
  54. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.positiveSum_zero_eq line 600

    Source documentation

    The exact decomposition with the origin deleted.

    theorem positiveSum_zero_eq (q : ℝ) (n m : ℕ) :
    positiveSum q n m 0 =
      q * ((∑ i ∈ Finset.range n, q ^ i) * (∑ j ∈ Finset.range (m + 1), q ^ j)) +
        q * (∑ j ∈ Finset.range m, q ^ j) := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.A5Scalar.positiveSum

  55. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.positiveSum_zero_le line 625
  56. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.positiveSum_pos_le line 638
  57. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.a16_finite_geometric line 657

    Source documentation

    The original positive-order geometric bound in (A.16), with independent finite truncations. No upper bound on k is required.

    theorem a16_finite_geometric (d n m k : ℕ) (hd : 1 ≤ d) :
    (∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (m + 1),
      if 1 ≤ i + j + k then ((2 : ℝ)⁻¹) ^ (63 * d * (i + j + k)) else 0) ≤
        ((2 : ℝ)⁻¹) ^ (31 * d * (k + 1)) := by
…
  58. theorem OAI.UniqueGamesTheorem.Appendix.A5Scalar.a16_original_range line 698
  59. theorem OAI.UniqueGamesTheorem.Appendix.A5WeightedReindex.exponent_weight_le line 719
  60. theorem OAI.UniqueGamesTheorem.Appendix.A5WeightedReindex.counted_weight_le line 734
  61. def OAI.UniqueGamesTheorem.Appendix.A5WeightedReindex.fiber line 751
  62. theorem OAI.UniqueGamesTheorem.Appendix.A5WeightedReindex.sum_grouped line 755

    Source documentation

    Exact finite grouping by the actual result and both dimension indices.

    theorem sum_grouped (d : ℕ) (result : α → β) (i j : α → ℕ)
    (hbound : ∀ a, i a ≤ d ∧ j a ≤ d) (C : β → ℕ → ℕ → ℝ) :
    (∑ a, C (result a) (i a) (j a)) =
      ∑ b, ∑ r ∈ Finset.range (d + 1), ∑ s ∈ Finset.range (d + 1),
        ((fiber result i j b r s).card : ℝ) * C b r s := by
…

    Mentions: OAI.UniqueGamesTheorem.Appendix.A5WeightedReindex.fiber

  63. theorem OAI.UniqueGamesTheorem.Appendix.A5WeightedReindex.weighted_reindex line 775