OAI/Computability/MaxCut/Games/RowErasureConcentration.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The row-erasure union bound is eventually strictly below one. The number of descriptions grows exponentially in m, while the tail exponent grows as 2 ^ ((ell-r)*(m-r)). The only asymptotic input is the standard proved limit that a fixed polynomial divided by 2^n tends to zero.

  1. theorem OAI.MaxCutGames.Inverse.RowErasure.table_expect_prod line 12
  2. theorem OAI.MaxCutGames.Inverse.RowErasure.exp_half_le_seven_quarters_inline_RowErasureConcentration line 21
  3. theorem OAI.MaxCutGames.Inverse.RowErasure.exp_half_indicator_inline_RowErasureConcentration line 27
  4. theorem OAI.MaxCutGames.Inverse.RowErasure.table_coordinate_exp_le line 32
  5. def OAI.MaxCutGames.Inverse.RowErasure.randomizedMatches line 62
  6. theorem OAI.MaxCutGames.Inverse.RowErasure.randomizedMatches_eq_masked_sum_inline_RowErasureTail line 66
  7. theorem OAI.MaxCutGames.Inverse.RowErasure.randomizedMatches_exp_product_inline_RowErasureTail line 85
  8. theorem OAI.MaxCutGames.Inverse.RowErasure.table_randomizedMatches_mgf_eq_inline_RowErasureTail line 93
  9. theorem OAI.MaxCutGames.Inverse.RowErasure.table_randomizedMatches_product_le_inline_RowErasureTail line 110
  10. theorem OAI.MaxCutGames.Inverse.RowErasure.table_randomizedMatches_mgf_le line 140
  11. theorem OAI.MaxCutGames.Inverse.RowErasure.uniformMass_mono line 149
  12. theorem OAI.MaxCutGames.Inverse.RowErasure.table_randomizedMatches_tail_le line 160

    Source documentation

    A full uniform table supplies independent coordinate samples. Only the entries in B ∩ s contribute; all other entries deterministically contribute 0.

    theorem table_randomizedMatches_tail_le
    {X Y : Type*} [Fintype X] [Fintype Y] [Nonempty Y]
    (s : Finset X) (B : X → Prop) (target : X → Y)
    (α : ℝ) (hα : 0 < α) (hαone : α ≤ 1)
    (hsmall : 1 / (Fintype.card Y : ℝ) ≤ α / 8) :
    uniformMass (fun replacement : X → Y =>
      α * s.card / 4 ≤ randomizedMatches s B target replacement) ≤
      Real.exp (-(α ^ 2 * s.card) / 32) := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.uniformMass, OAI.MaxCutGames.Inverse.RowErasure.randomizedMatches

  13. theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.randomizedAgreement_probability_le line 214

    Source documentation

    The per-description bound used by the simultaneous erasure union bound.

    theorem SliceFamily.randomizedAgreement_probability_le
    {X Y A S D : Type*} [Fintype X] [Fintype Y] [Nonempty Y]
    (F : SliceFamily X Y A S D) (B : X → Prop) (α : ℝ)
    (hα : 0 < α) (hαone : α ≤ 1)
    (hsmall : 1 / (Fintype.card Y : ℝ) ≤ α / 8) (d : D) :
    uniformMass (fun replacement : X → Y =>
      (F.points d).Nonempty ∧ α / 4 ≤ F.randomizedAgreement B replacement d) ≤
      Real.exp (-(α ^ 2 * (F.points d).card) / 32) := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasure.SliceFamily, OAI.MaxCutGames.Inverse.RowErasure.uniformMass

  14. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.exists_replacement_of_budget line 243

    Source documentation

    One replacement table simultaneously defeats every padded slice/target. The budget depends only on dimensions and α, not on the labeling or erased set.

    theorem exists_replacement_of_budget {ell m r : ℕ}
    (B : Mat ell m → Prop) (α : ℝ) (hα : 0 < α) (hαone : α ≤ 1)
    (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8)
    (hbudget : (2 : ℝ) ^ ((2 * r + 1) * (ell + m)) *
      Real.exp (-(α ^ 2 * (2 : ℝ) ^ ((ell - r) * (m - r))) / 32) < 1) :
    ∃ replacement : Mat ell m → Vector ell,
      ∀ d : Description ell m r, ((family ell m r).points d).Nonempty →
        (family ell m r).randomizedAgreement B replacement d < α / 4 := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasureMatrix.family

  15. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.advice_mass_ge_of_inverse_and_budget line 271

    Source documentation

    Finite product concentration and concrete slice counts discharge the random-erasure obligation under the inverse hypothesis.

    theorem advice_mass_ge_of_inverse_and_budget {ell m r : ℕ}
    (f : Mat ell m → Vector ell) (η α : ℝ) (hη : 0 < η)
    (hα : 0 < α) (hαone : α ≤ 1)
    (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8)
    (haccept : 4 * η ≤ Shortcode.equalityAcceptance f)
    (inverse : ∀ g : Mat ell m → Vector ell,
      η ≤ Shortcode.equalityAcceptance g → HasAffineSlice g α r)
    (hbudget : (2 : ℝ) ^ ((2 * r + 1) * (ell + m)) *
      Real.exp (-(α ^ 2 * (2 : ℝ) ^ ((ell - r) * (m - r))) / 32) < 1) :
    η / (2 ^ (ell * r) : ℝ) ≤ adviceMass ((family ell m r).goodAt f α) := by
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.equalityAcceptance, OAI.MaxCutGames.Inverse.RowErasureMatrix.family

  16. theorem OAI.MaxCutGames.Inverse.RowErasure.eventually_log_unionBound_neg line 302

    Source documentation

    Logarithm of the finite union-bound estimate, for every sufficiently large column dimension. Neither the threshold nor the proof depends on a parity condition on the column dimension.

    theorem eventually_log_unionBound_neg (α : ℝ) (hα : 0 < α)
    (ell r : ℕ) (hr : r < ell) :
    ∀ᶠ m : ℕ in atTop,
      (((2 * r + 1) * (ell + m) : ℕ) : ℝ) * Real.log 2 -
        α ^ 2 * (2 : ℝ) ^ ((ell - r) * (m - r)) / 32 < 0 := by
…
  17. theorem OAI.MaxCutGames.Inverse.RowErasure.eventually_unionBound_lt_one line 357

    Source documentation

    The exact description-count times tail estimate needed for simultaneous row erasure is strictly below one in all sufficiently large dimensions.

    theorem eventually_unionBound_lt_one (α : ℝ) (hα : 0 < α)
    (ell r : ℕ) (hr : r < ell) :
    ∀ᶠ m : ℕ in atTop,
      (2 : ℝ) ^ ((2 * r + 1) * (ell + m)) *
        Real.exp (-(α ^ 2) * (2 : ℝ) ^ ((ell - r) * (m - r)) / 32) < 1 := by
…
  18. theorem OAI.MaxCutGames.Inverse.RowErasure.exists_unionBound_threshold line 376

    Source documentation

    A threshold usable by dimension-selection arguments, with enough columns to accommodate all r prescribed column constraints.

    theorem exists_unionBound_threshold (α : ℝ) (hα : 0 < α)
    (ell r : ℕ) (hr : r < ell) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → r ≤ m ∧
      (2 : ℝ) ^ ((2 * r + 1) * (ell + m)) *
        Real.exp (-(α ^ 2) * (2 : ℝ) ^ ((ell - r) * (m - r)) / 32) < 1 := by
…
  19. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.exists_erasure_threshold line 395

    Source documentation

    A single dimension threshold supplies replacements for every erased set. There is no inverse-theorem premise in this concentration/counting statement.

    theorem exists_erasure_threshold (α : ℝ) (hα : 0 < α) (hαone : α ≤ 1)
    (ell r : ℕ) (hr : r < ell) (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m →
      ∀ B : Mat ell m → Prop,
        ∃ replacement : Mat ell m → Vector ell,
          ∀ d : Description ell m r, ((family ell m r).points d).Nonempty →
            (family ell m r).randomizedAgreement B replacement d < α / 4 := by
…

    Mentions: OAI.MaxCutGames.Inverse.RowErasureMatrix.family

  20. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.exists_fixed_context_advice_threshold line 410

    Source documentation

    For sufficiently many columns, every accepted function has a positive measure of good row advice, assuming the genuine bounded-slice inverse.

    theorem exists_fixed_context_advice_threshold (η α : ℝ)
    (hη : 0 < η) (hα : 0 < α) (hαone : α ≤ 1)
    (ell r : ℕ) (hr : r < ell) (halphabet : 1 / (2 ^ ell : ℝ) ≤ α / 8) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m →
      (∀ g : Mat ell m → Vector ell,
        η ≤ Shortcode.equalityAcceptance g → HasAffineSlice g α r) →
      ∀ f : Mat ell m → Vector ell,
        4 * η ≤ Shortcode.equalityAcceptance f →
          η / (2 ^ (ell * r) : ℝ) ≤ adviceMass ((family ell m r).goodAt f α) := by
…

    Mentions: OAI.MaxCutGames.Inverse.Shortcode.equalityAcceptance, OAI.MaxCutGames.Inverse.RowErasureMatrix.family

  21. theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.exists_contextual_advice_threshold line 425