BulkDeletionRate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform decay of the original deletion and collision costs

theorem OAI.Ostmann.bulk_auxiliary_prefactor_le line 11

theorem OAI.Ostmann.bulk_collision_deletion_numerical_rate line 49

Source documentation

The cutoff precedes the bulk dimension, deletion sets, and original normalizers. Both bad-event costs have a stronger saving than the cell error.

theorem bulk_collision_deletion_numerical_rate (C : ℝ) (hC : 1 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ a d H T B : ℝ,
      0 ≤ a → 0 ≤ d → 0 ≤ B → a ≤ C * L → d ≤ Real.exp (C * L) → H ≤ C * L →
      B ≤ Real.exp (C * L ^ 2 + C * L * Real.exp ((1 / 1000 : ℝ) * L)) →
      Real.exp ((39 / 10000 : ℝ) * L) ≤ T →
      a * d * Real.exp (H - T) ≤ Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) ∧
      B * (a ^ 2 + 2 * a * d) * Real.exp (H - T) ≤
        Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) := by
…

theorem OAI.Ostmann.bulk_collision_deletion_rate line 87

Source documentation

The actual deleted-set expression, with all old normalizers, and the distinctness error are absorbed together.

theorem bulk_collision_deletion_rate (C : ℝ) (hC : 1 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (J : Type) [Fintype J] (S D : J → Finset ℕ)
      (Z : J → ℝ) (H T K B : ℝ),
      (∀ j, 0 ≤ Z j) → (∀ j, Z j ≤ Real.exp H) →
      (∀ j, ((D j).card : ℝ) ≤ K) → 0 ≤ K → 0 ≤ B →
      (Fintype.card J : ℝ) ≤ C * L → K ≤ Real.exp (C * L) → H ≤ C * L →
      B ≤ Real.exp (C * L ^ 2 + C * L * Real.exp ((1 / 1000 : ℝ) * L)) →
      Real.exp ((39 / 10000 : ℝ) * L) ≤ T →
      (∀ j q, q ∈ S j → Real.exp T ≤ (q : ℝ)) →
      B * (Fintype.card J : ℝ) ^ 2 * Real.exp (H - T) +
        B * ((∏ j, (1 + Z j * ∑ q ∈ S j ∩ D j, (q : ℝ)⁻¹)) - 1) ≤
      Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) := by
…