OAI/Computability/UniqueGames/Decoding/SparseLawLemmas.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

The finite calculation of projected total variation. The three singleton lines are averaged before the divergence is taken; projection choices are not part of the compared sample space. Coordinates are independently sampled occurrences, irrespective of whether their equation IDs coincide.

  1. def OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformWeights line 27
  2. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformWeights_pos line 30
  3. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformWeights_isProbability line 33
  4. def OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformChiSquare line 42

    Source documentation

    Pearson divergence against the uniform law, written with its constant denominator cleared. uniformChiSquare_eq_pearson identifies the actual likelihood-ratio definition.

    def uniformChiSquare (p : α → ℝ) : ℝ :=
…
  5. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformChiSquare_eq_pearson line 45
  6. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformChiSquare_eq_secondMoment line 55
  7. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformChiSquare_nonneg line 71
  8. def OAI.UniqueGamesTheorem.Decoder.SparseLaw.mixture line 75
  9. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.mixture_isProbability line 78
  10. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformChiSquare_mixture line 88
  11. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.totalVariation_le_half_sqrt line 98
  12. def OAI.UniqueGamesTheorem.Decoder.SparseLaw.independentWeights line 107
  13. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.independentWeights_isProbability line 110
  14. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformChiSquare_independent line 118
  15. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.pow_mul_one_sub_le_one line 134

    Source documentation

    A finite bound sufficient for the cube asymptotic, without introducing a limit theorem or choosing the alphabet after the repetition count.

    theorem pow_mul_one_sub_le_one (x : ℝ) (hx : 0 ≤ x) (k : ℕ) :
    (1 + x) ^ k * (1 - k * x) ≤ 1 := by
…
  16. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.pow_sub_one_le_fraction line 145
  17. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.pow_sub_one_le_twice line 152
  18. def OAI.UniqueGamesTheorem.Decoder.SparseLaw.lineCount line 166

    Source documentation

    At the origin all three singleton lines contribute.

    def lineCount (z : V × V) : ℝ :=
…
  19. def OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonPairWeights line 171

    Source documentation

    The average of the laws of (a,0), (0,a), and (a,a) for uniform a.

    def singletonPairWeights (z : V × V) : ℝ := lineCount V z / (3 * Fintype.card V)

    Mentions: OAI.UniqueGamesTheorem.Decoder.SparseLaw.lineCount

  20. def OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonSamplerWeights line 175

    Source documentation

    Explicit finite pushforward of the three equally likely singleton choices. The same uniform slope supplies both entries of the diagonal choice.

    def singletonSamplerWeights (z : V × V) : ℝ :=
…
  21. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonSamplerWeights_eq line 180
  22. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.lineCount_sum line 207
  23. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.lineCount_sq line 221
  24. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.lineCount_sq_sum line 227
  25. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonPairWeights_isProbability line 238
  26. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonPairWeights_secondMoment line 247
  27. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonPairWeights_chiSquare line 253
  28. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.paddedSlope_chiSquare line 263

    Source documentation

    Exact finite divergence of the padded slope law.

    theorem paddedSlope_chiSquare (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (k : ℕ) :
    uniformChiSquare (independentWeights (mixture β (singletonPairWeights V)) k) =
      (1 + β ^ 2 * ((Fintype.card V : ℝ) - 1) / 3) ^ k - 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformChiSquare, OAI.UniqueGamesTheorem.Decoder.SparseLaw.independentWeights, OAI.UniqueGamesTheorem.Decoder.SparseLaw.mixture, OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonPairWeights

  29. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.paddedSlope_totalVariation line 271
  30. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.paddedSlope_totalVariation_small line 278
  31. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.cubeSlope_totalVariation line 291
  32. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.exists_cubeSlope_totalVariation_le line 324

    Source documentation

    Arbitrarily many expected singleton coordinates coexist with arbitrarily small variation error: taking k=m³ and beta=m⁻² leaves k*beta=m. The bound involves only the fixed alphabet and requested error.

    theorem exists_cubeSlope_totalVariation_le (η : ℝ) (hη : 0 < η) (N : ℕ) :
    ∃ m : ℕ, N ≤ m ∧ 0 < m ∧
      totalVariation
        (independentWeights (mixture (1 / (m : ℝ) ^ 2) (singletonPairWeights V)) (m ^ 3))
        (uniformWeights (Fin (m ^ 3) → V × V)) ≤ η := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.SparseLaw.independentWeights, OAI.UniqueGamesTheorem.Decoder.SparseLaw.mixture, OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonPairWeights, OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformWeights

  33. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.cube_expected_singletons line 351
  34. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.translated_uniform_intercept line 367

    Source documentation

    Pulling back an independent uniform intercept through any translation, even one depending on all slopes and projection choices, leaves its joint law unchanged. No independence of that translation from the slopes is assumed.

    theorem translated_uniform_intercept (p : α → ℝ) (shift : α → V) (a : α) (z : V) :
    p a * uniformWeights V (z - shift a) = p a * uniformWeights V z := rfl

    Mentions: OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformWeights

  35. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniform_intercept_pushforward line 370
  36. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.joint_intercept_pushforward line 377
  37. theorem OAI.UniqueGamesTheorem.Decoder.SparseLaw.totalVariation_append_uniform_intercept line 390
  38. def OAI.UniqueGamesTheorem.Decoder.ConstantSelection.visibleMass line 413

    Source documentation

    Probability of actual visible data carrying a transferred witness.

    def visibleMass (α g₀ : ℝ) (ell r : ℕ) : ℝ :=
…
  39. def OAI.UniqueGamesTheorem.Decoder.ConstantSelection.conditionalMass line 417

    Source documentation

    Independent private decoding success on a transferred witness.

    def conditionalMass (α : ℝ) (ell r : ℕ) : ℝ :=
…
  40. def OAI.UniqueGamesTheorem.Decoder.ConstantSelection.decodingMass line 420
  41. def OAI.UniqueGamesTheorem.Decoder.ConstantSelection.variationBudget line 425

    Source documentation

    The whole-table TV budget includes the coefficient of both compared events in the witness-margin inequality.

    def variationBudget (α g₀ : ℝ) (ell r : ℕ) : ℝ :=
…
  42. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.visibleMass_pos line 428
  43. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.conditionalMass_pos line 433
  44. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.decodingMass_pos line 438
  45. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.variationBudget_pos line 442
  46. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.variationBudget_suffices line 446
  47. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.cube_exponential_antitone line 459

    Source documentation

    Exponential clean-mask decay persists after increasing the cube root.

    theorem cube_exponential_antitone {m n : ℕ} (hmn : m ≤ n)
    {N : ℝ} (hN : 0 < N) :
    Real.exp (-(n : ℝ) / (3600 * N)) ≤
      Real.exp (-(m : ℝ) / (3600 * N)) := by
…
  48. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.exists_simultaneous_cube line 469

    Source documentation

    One tuple length meets the sparse-law and repetition requirements, while exceeding any independent inverse/erasure dimension threshold.

    theorem exists_simultaneous_cube (V : Type*) [Fintype V] [Zero V] [DecidableEq V]
    {N ε γ : ℝ} (hN : 1 ≤ N) (hε : 0 < ε) (hγ : 0 < γ) (lower : ℕ) :
    ∃ m : ℕ, lower ≤ m ∧ 0 < m ∧
      totalVariation
        (independentWeights (mixture (1 / (m : ℝ) ^ 2) (singletonPairWeights V)) (m ^ 3))
        (uniformWeights (Fin (m ^ 3) → V × V)) ≤ ε ∧
      (1 - ((1 / (m : ℝ) ^ 2) / N) / 3600) ^ (m ^ 3) < γ := by
…
  49. theorem OAI.UniqueGamesTheorem.Decoder.ConstantSelection.exists_matrix_cube line 490

    Source documentation

    All scalar requirements for the final decoding contradiction can be met after the fixed alphabet and inverse parameters have been chosen.

    theorem exists_matrix_cube (V : Type*) [Fintype V] [Zero V] [DecidableEq V]
    {α g₀ : ℝ} (hα : 0 < α) (hg₀ : 0 < g₀)
    (ell r dimW lower : ℕ) :
    ∃ m : ℕ, lower ≤ m ∧ 0 < m ∧
      totalVariation
        (independentWeights (mixture (1 / (m : ℝ) ^ 2) (singletonPairWeights V)) (m ^ 3))
        (uniformWeights (Fin (m ^ 3) → V × V)) ≤ variationBudget α g₀ ell r ∧
      (1 - ((1 / (m : ℝ) ^ 2) / (2 : ℝ) ^ (dimW + r)) / 3600) ^ (m ^ 3) <
        decodingMass α g₀ ell r := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.ConstantSelection.variationBudget, OAI.UniqueGamesTheorem.Decoder.ConstantSelection.decodingMass