OAI/Computability/UniqueGames/Reduction/ExplicitLemmas.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Actual finite linear-map enumeration for the free homogeneous coordinates. The lists contain linear maps themselves, constructed by finite coordinate sums. Their exhaustiveness and lack of repetitions identify the list with the uniform map experiment. No machine running-time claim follows just from their lengths.

  1. def OAI.UniqueGamesTheorem.Reduction.Explicit.pairs line 19

    Source documentation

    A Cartesian product that preserves repetitions in each input list.

    def pairs (xs : List α) (ys : List β) : List (α × β) :=
…
  2. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.length_pairs line 22
  3. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.mem_pairs line 31
  4. def OAI.UniqueGamesTheorem.Reduction.Explicit.words line 36

    Source documentation

    Enumerate all words of length k over an explicitly listed alphabet.

    def words (alphabet : List α) : Nat → List (List α)
  | 0 => [[]]
  | k + 1 => (pairs alphabet (words alphabet k)).map fun p => p.1 :: p.2

    Mentions: OAI.UniqueGamesTheorem.Reduction.Explicit.pairs

  5. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.length_words line 40
  6. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.mem_words line 49

    Source documentation

    The enumerator covers exactly the prescribed words.

    theorem mem_words {alphabet : List α} {w : List α} {k : Nat} :
    w ∈ words alphabet k ↔ w.length = k ∧ ∀ a ∈ w, a ∈ alphabet := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.Explicit.words

  7. abbrev OAI.UniqueGamesTheorem.Reduction.Explicit.CoordinateOutcome line 79

    Source documentation

    (question occurrences, binary map matrix, noise index, binary functional). The matrix is flattened and has (2*k+1)*dimR bits.

    abbrev CoordinateOutcome := (List Nat × List Nat) × (Nat × List Nat)
  8. def OAI.UniqueGamesTheorem.Reduction.Explicit.edgeOutcomes line 81
  9. def OAI.UniqueGamesTheorem.Reduction.Explicit.edgeCount line 87

    Source documentation

    The formula in Equation (4.21).

    def edgeCount (m k dimR noiseCount : Nat) : Nat :=
…
  10. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.length_edgeOutcomes line 90
  11. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.edgeCount_pos line 97
  12. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.edgeOutcomes_nonempty line 101
  13. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.edgeCount_mono line 108
  14. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.product_pow line 113
  15. theorem OAI.UniqueGamesTheorem.Reduction.Explicit.edgeCount_polynomial_bound line 120
  16. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_pairs line 154
  17. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.functions line 158

    Source documentation

    Exhaustive finite-function enumeration with a specified value list.

    def functions (values : List α) : (n : Nat) → List (Fin n → α)
  | 0 => [Fin.elim0]
  | n + 1 => (pairs values (functions values n)).map
      (fun p => Fin.cons p.1 p.2)
  18. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_functions line 163
  19. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.mem_functions line 169
  20. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_functions line 179
  21. abbrev OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Coefficients line 195
  22. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.fromCoefficients line 197
  23. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.toCoefficients line 207
  24. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.to_fromCoefficients line 210
  25. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.from_toCoefficients line 219
  26. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.coefficientEquiv line 226

    Source documentation

    Actual matrix-coefficient equivalence, rather than just a count model.

    def coefficientEquiv : Coefficients k R ≃ (E k →ₗ[F2] R) where
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Coefficients

  27. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.allLinearMaps line 232
  28. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_allLinearMaps line 235
  29. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.mem_allLinearMaps line 242
  30. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_allLinearMaps line 249
  31. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.cardinal_linearMaps line 254
  32. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.vectors line 264
  33. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_vectors line 267
  34. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.mem_vectors line 270
  35. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_vectors line 274
  36. abbrev OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Ambient line 277
  37. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.ambientVectors line 280
  38. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_ambientVectors line 282
  39. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.mem_ambientVectors line 285
  40. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_ambientVectors line 288
  41. abbrev OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Query line 291
  42. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.queries line 293
  43. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.mem_queries line 296
  44. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_queries line 300
  45. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_queries line 304
  46. abbrev OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Outcome line 309
  47. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.outcomes line 313
  48. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_outcomes line 318
  49. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.mem_outcomes line 328
  50. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_outcomes line 337
  51. def OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.indexedOutcomes line 347

    Source documentation

    The executable edge experiment for an arbitrary explicitly ordered noise index type. Equal noise vectors still have separate indices and entries.

    def indexedOutcomes (m k s d : Nat) (indices : List N) :
    List (Query m k s d × (N × (E k →ₗ[F2] F2))) :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Query

  52. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_indexedOutcomes line 351
  53. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.mem_indexedOutcomes line 356
  54. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.nodup_indexedOutcomes line 363
  55. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.indexedOutcomes_nonempty line 368
  56. theorem OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.length_indexedOutcomes_polynomial_bound line 377

    Source documentation

    A genuine polynomial size bound for the actual linear-map edge list. This is deliberately separate from a certified machine running-time bound.

    theorem length_indexedOutcomes_polynomial_bound {m n coefficient degree : Nat}
    (h : m ≤ coefficient * (n+1)^degree) (k s d : Nat) (indices : List N) :
    (indexedOutcomes m k s d indices).length ≤
      (coefficient^k * 2^((2*k+1)*(s+d+1)) * indices.length) *
        (n+1)^(degree*k) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.indexedOutcomes

  57. def OAI.UniqueGamesTheorem.Reduction.FiniteNoise.realizedBit line 406
  58. def OAI.UniqueGamesTheorem.Reduction.FiniteNoise.realizedNoise line 408
  59. theorem OAI.UniqueGamesTheorem.Reduction.FiniteNoise.realizedBit_eq_true_iff line 411
  60. theorem OAI.UniqueGamesTheorem.Reduction.FiniteNoise.coordinate_fiber_sum line 416

    Source documentation

    The two fibers of a coordinate have their actual normalized finite counts.

    theorem coordinate_fiber_sum {D : Nat} (positive : 0 < D) (b : Bool) :
    (∑ z : Fin D, if realizedBit z = b then (D : ℝ)⁻¹ else 0) =
      if b then (D : ℝ)⁻¹ else 1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.FiniteNoise.realizedBit

  61. theorem OAI.UniqueGamesTheorem.Reduction.FiniteNoise.noiseWeight_eq_fiber_sum line 441

    Source documentation

    Product distributivity computes the mass of every complete Boolean noise vector.

    theorem noiseWeight_eq_fiber_sum {D : Nat} (positive : 0 < D) (μ : A → Bool) :
    noiseWeight ((D : ℝ)⁻¹) μ =
      ∑ z : A → Fin D,
        ∏ a, if realizedBit (z a) = μ a then (D : ℝ)⁻¹ else 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.FiniteNoise.realizedBit

  62. theorem OAI.UniqueGamesTheorem.Reduction.FiniteNoise.fiber_product_eq_indicator line 453
  63. theorem OAI.UniqueGamesTheorem.Reduction.FiniteNoise.expect_realizedNoise line 467

    Source documentation

    Exact pushforward law for every observable, using the existing noise weight.

    theorem expect_realizedNoise {D : Nat} (positive : 0 < D) (H : (A → Bool) → ℝ) :
    (𝔼 z : A → Fin D, H (realizedNoise z)) =
      ∑ μ : A → Bool, noiseWeight ((D : ℝ)⁻¹) μ * H μ := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.FiniteNoise.realizedNoise