OAI/Computability/UniqueGames/Inverse/RowErasureTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Inverse.RowErasure.randomizedMatches line 13
2. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.randomizedMatches_eq_masked_sum line 17
3. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.randomizedMatches_exp_product line 36
4. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.table_randomizedMatches_mgf_eq line 44
5. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.table_randomizedMatches_product_le line 61
6. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.table_randomizedMatches_mgf_le line 91
7. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass_mono line 100
8. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.table_randomizedMatches_tail_le line 111

   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.UniqueGamesTheorem.Inverse.RowErasure.uniformMass, OAI.UniqueGamesTheorem.Inverse.RowErasure.randomizedMatches

9. theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.randomizedAgreement_probability_le line 165

   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.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily, OAI.UniqueGamesTheorem.Inverse.RowErasure.uniformMass