OAI/Computability/UniqueGames/Inverse/RowErasureLemmas.lean

GitHub source file

53 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. def OAI.UniqueGamesTheorem.Inverse.RowErasure.indicator line 22
  2. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.indicator_true line 26
  3. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.indicator_false line 27
  4. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.indicator_nonneg line 29
  5. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.indicator_le_one line 34
  6. def OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass line 39
  7. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass_nonneg line 42
  8. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass_le_one line 46
  9. def OAI.UniqueGamesTheorem.Inverse.RowErasure.replaceOn line 51

    Source documentation

    One independent replacement value per matrix entry, not per row fiber.

    def replaceOn {X Y : Type*} (B : X → Prop) (f replacement : X → Y) : X → Y := by
…
  10. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.replaceOn_of_not_mem line 55
  11. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.replaceOn_of_mem line 60
  12. def OAI.UniqueGamesTheorem.Inverse.RowErasure.equalityAcceptance line 65
  13. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.acceptance_le_modified_add_two_mass line 72

    Source documentation

    Deterministic acceptance loss under editing a set of entries. Both endpoint marginals must equal the matrix-uniform law; no independence of endpoints is required. This applies to every choice of replacement values.

    theorem acceptance_le_modified_add_two_mass
    {X Y E : Type*} [Fintype X] [Fintype E]
    (left right : E → X) (B : X → Prop) (f g : X → Y)
    (unchanged : ∀ x, ¬ B x → f x = g x)
    (left_uniform : uniformMass (fun e => B (left e)) = uniformMass B)
    (right_uniform : uniformMass (fun e => B (right e)) = uniformMass B) :
    equalityAcceptance left right f ≤
      equalityAcceptance left right g + 2 * uniformMass B := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass, OAI.UniqueGamesTheorem.Inverse.RowErasure.equalityAcceptance

  14. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.acceptance_ge_original_sub_two_mass line 107
  15. def OAI.UniqueGamesTheorem.Inverse.RowErasure.goodUnion line 122

    Source documentation

    A matrix belongs to the erased union exactly when at least one row map provides good advice there.

    def goodUnion {A X : Type*} (good : A → X → Prop) (x : X) : Prop :=
…
  16. def OAI.UniqueGamesTheorem.Inverse.RowErasure.adviceMass line 126

    Source documentation

    Sample a uniform matrix, then an independent uniform row map.

    def adviceMass {A X : Type*} [Fintype A] [Fintype X]
    (good : A → X → Prop) : ℝ :=
…
  17. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.adviceMass_nonneg line 130
  18. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.union_mass_le_card_mul_adviceMass line 136

    Source documentation

    Each matrix in the union has at least one successful row-map atom. No disjointness between good fibers is needed.

    theorem union_mass_le_card_mul_adviceMass
    {A X : Type*} [Fintype A] [Fintype X] (good : A → X → Prop) :
    uniformMass (goodUnion good) ≤ (Fintype.card A : ℝ) * adviceMass good := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass, OAI.UniqueGamesTheorem.Inverse.RowErasure.goodUnion, OAI.UniqueGamesTheorem.Inverse.RowErasure.adviceMass

  19. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.adviceMass_ge_union_div_card line 155
  20. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.adviceMass_ge_of_union_mass line 163
  21. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.eventually_log_unionBound_neg line 192

    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
…
  22. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.eventually_unionBound_lt_one line 247

    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
…
  23. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.exists_unionBound_threshold line 266

    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
…
  24. def OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.direction line 295

    Source documentation

    The linear part of the affine parametrization.

    def direction (A : K →ₗ[R] L) (Q : Submodule R E)
    (N : (E ⧸ Q) →ₗ[R] A.ker) : E →ₗ[R] K :=
…
  25. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.direction_apply line 299
  26. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.exists_direction_of_row_and_column line 305

    Source documentation

    Quotient descent of a linear map which vanishes on the column span and takes values in the common row kernel.

    theorem exists_direction_of_row_and_column (A : K →ₗ[R] L)
    (Q : Submodule R E) (B : E →ₗ[R] K)
    (hQ : Q ≤ B.ker) (hA : LinearMap.range B ≤ A.ker) :
    ∃ N : (E ⧸ Q) →ₗ[R] A.ker, direction A Q N = B := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.direction

  27. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.direction_injective line 321
  28. def OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.AffineSlice line 331

    Source documentation

    The concrete affine slice around any one point satisfying its equations.

    def AffineSlice (A : K →ₗ[R] L) (Q : Submodule R E) (M₀ : E →ₗ[R] K) :=
…
  29. def OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.ofQuotient line 334
  30. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.ofQuotient_val line 346
  31. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.ofQuotient_bijective line 350
  32. def OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.equiv line 374

    Source documentation

    Uniform free quotient maps parametrize exactly the original affine slice.

    def equiv (A : K →ₗ[R] L) (Q : Submodule R E) (M₀ : E →ₗ[R] K) :
    ((E ⧸ Q) →ₗ[R] A.ker) ≃ AffineSlice A Q M₀ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.AffineSlice

  33. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.equiv_apply line 378
  34. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.equiv_affine_target line 383

    Source documentation

    The base point contributes an affine offset; it is not discarded.

    theorem equiv_affine_target (A : K →ₗ[R] L) (Q : Submodule R E)
    (M₀ : E →ₗ[R] K) (N : (E ⧸ Q) →ₗ[R] A.ker) (z : E) (u : K) :
    (equiv A Q M₀ N).val z + u =
      (N (Q.mkQ z) : K) + (M₀ z + u) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.equiv

  35. theorem OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.expect_equiv line 391

    Source documentation

    Exact uniform-law transport through the affine parametrization.

    theorem expect_equiv (A : K →ₗ[R] L) (Q : Submodule R E) (M₀ : E →ₗ[R] K)
    [Fintype ((E ⧸ Q) →ₗ[R] A.ker)] [Fintype (AffineSlice A Q M₀)]
    (f : AffineSlice A Q M₀ → ℝ) :
    Finset.univ.expect (fun N => f (equiv A Q M₀ N)) = Finset.univ.expect f := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.AffineSlice, OAI.UniqueGamesTheorem.Inverse.RowErasureSliceQuotient.equiv

  36. structure OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily line 414

    Source documentation

    Each description includes its row map, row value, column equations and affine target. points_row is the necessary relationship to actual row advice.

    structure SliceFamily (X Y A S D : Type*) where
…
  37. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.agreement line 422
  38. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.GoodAdvice line 425
  39. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.goodAt line 430
  40. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.erasedUnion line 434
  41. def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.randomizedAgreement line 440

    Source documentation

    Only randomized entries count; an unchanged entry contributes zero, even when its old label already matches the target.

    def SliceFamily.randomizedAgreement (F : SliceFamily X Y A S D)
    (B : X → Prop) (replacement : X → Y) (d : D) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily

  42. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.mem_erasedUnion_of_good_row line 444
  43. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.original_agreement_lt_of_not_good line 453
  44. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.modified_agreement_le_original_add_randomized line 461
  45. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.modified_agreement_eq_randomized_of_good line 483
  46. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.modified_agreement_lt line 499

    Source documentation

    If the random replacement bound holds, every permitted nonempty slice has modified agreement strictly below α. The proof splits on goodness of the whole row fiber, not on goodness of the individual column slice.

    theorem SliceFamily.modified_agreement_lt
    (F : SliceFamily X Y A S D) (f replacement : X → Y)
    (α : ℝ) (hα : 0 < α)
    (randomized_small : ∀ d, (F.points d).Nonempty →
      F.randomizedAgreement (F.erasedUnion f α) replacement d < α / 4)
    (d : D) (hne : (F.points d).Nonempty) :
    F.agreement (replaceOn (F.erasedUnion f α) f replacement) d < α := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily, OAI.UniqueGamesTheorem.Inverse.RowErasure.replaceOn

  47. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.union_mass_ge_of_inverse_and_erasure line 520

    Source documentation

    Conditional erasure contradiction. The two deep inputs remain explicit: the inverse theorem for arbitrary (possibly unfolded) functions, and existence of a replacement table uniformly small on every slice/target description.

    theorem SliceFamily.union_mass_ge_of_inverse_and_erasure
    {E : Type*} [Fintype X] [Fintype E]
    (F : SliceFamily X Y A S D) (left right : E → X)
    (f : X → Y) (η α : ℝ) (hη : 0 < η) (hα : 0 < α)
    (acceptance_large : 4 * η ≤ equalityAcceptance left right f)
    (left_uniform : ∀ B : X → Prop,
      uniformMass (fun e => B (left e)) = uniformMass B)
    (right_uniform : ∀ B : X → Prop,
      uniformMass (fun e => B (right e)) = uniformMass B)
    (inverse : ∀ g : X → Y, η ≤ equalityAcceptance left right g →
      ∃ d, (F.points d).Nonempty ∧ α ≤ F.agreement g d)
    (erasure : ∃ replacement : X → Y, ∀ d, (F.points d).Nonempty →
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily, OAI.UniqueGamesTheorem.Inverse.RowErasure.equalityAcceptance, OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass

  48. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass_exists_le_sum line 559
  49. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.exists_avoiding_of_sum_bad_lt_one line 576
  50. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.exists_avoiding_of_card_mul_bound_lt_one line 592
  51. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.exists_erasure_of_probability_bound line 606

    Source documentation

    The union-bound step for actual replacement tables. Nonempty slice descriptions with randomized agreement at least α/4 are the bad events.

    theorem SliceFamily.exists_erasure_of_probability_bound
    {X Y A S D : Type*} [Fintype X] [Fintype Y] [Nonempty Y] [Fintype D]
    (F : SliceFamily X Y A S D) (B : X → Prop) (α ρ : ℝ)
    (hprob : ∀ d, uniformMass (fun replacement : X → Y =>
      (F.points d).Nonempty ∧ α / 4 ≤ F.randomizedAgreement B replacement d) ≤ ρ)
    (hsmall : (Fintype.card D : ℝ) * ρ < 1) :
    ∃ replacement : X → Y, ∀ d, (F.points d).Nonempty →
      F.randomizedAgreement B replacement d < α / 4 := by
…

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

  52. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.advice_average_ge line 623

    Source documentation

    Average the fixed-context advice bound over the spectral good contexts. Both samples remain explicit: the context, then the row map and matrix.

    theorem advice_average_ge
    {Q A X : Type*} [Fintype Q] [Fintype A] [Nonempty A] [Fintype X]
    (goodContext : Q → Prop) (good : Q → A → X → Prop)
    (β η : ℝ) (hη : 0 ≤ η)
    (hcontext : β ≤ uniformMass goodContext)
    (hlocal : ∀ q, goodContext q → η ≤ uniformMass (goodUnion (good q))) :
    β * (η / (Fintype.card A : ℝ)) ≤
      Finset.univ.expect (fun q => adviceMass (good q)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass, OAI.UniqueGamesTheorem.Inverse.RowErasure.goodUnion, OAI.UniqueGamesTheorem.Inverse.RowErasure.adviceMass

  53. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.advice_average_ge_ten_eta_sq_div_card line 644