BulkWeightedErrorRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform decay of the full weighted bulk replacement error

theorem OAI.Ostmann.PublishedProgressionInput.bulk_weighted_error_rate line 13

Source documentation

The cutoff is chosen before the finite cell sets, modulus and original normalizers. Their literal bounds include every joint box and residue.

theorem PublishedProgressionInput.bulk_weighted_error_rate
    (P : PublishedProgressionInput) (C : ℝ) (hC : 1 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (J Cell : Type) [Fintype J] [Fintype Cell]
      (M Q : ℕ) [NeZero M], 2 ≤ Q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 10000 : ℝ) * L) →
      ∀ (Z : J → ℝ) (a : (J → (ZMod M)ˣ) → ℂ) (A B T : ℝ),
      (∀ j, 0 ≤ Z j) → 0 ≤ A → 0 ≤ B →
      (Fintype.card J : ℝ) ≤ C * L →
      (∀ j, Z j ≤ Real.exp (C * L)) →
      (Fintype.card Cell : ℝ) ≤ Real.exp (Real.exp ((14 / 10000 : ℝ) * L)) →
      (Fintype.card (ZMod M)ˣ : ℝ) ≤ Real.exp (Real.exp ((12 / 10000 : ℝ) * L)) →
      A ≤ Real.exp (C * L * Real.exp ((1 / 1000 : ℝ) * L)) →
…

Mentions: OAI.Ostmann.PublishedProgressionInput