ArithmeticErrorRates.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the fixed-depth arithmetic comparison costs

The polynomial and spectator costs in Section 8 are dominated by the double-exponential savings. The strict numerical gaps in the manuscript therefore survive the finite history and equality-pattern sums.

theorem OAI.Ostmann.arithmetic_exponent_absorption line 18
theorem OAI.Ostmann.arithmetic_error_absorption line 35

theorem OAI.Ostmann.bulk_variation_error line 47

Source documentation

The mesh variation error in the bulk idealization, including the spectator and polynomial history costs.

theorem bulk_variation_error (C : ℝ) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 2 + C * L * Real.exp ((1 / 1000 : ℝ) * L)) *
        Real.exp (-Real.exp ((14 / 10000 : ℝ) * L)) ≤
          Real.exp (-Real.exp ((125 / 100000 : ℝ) * L)) := by
…

theorem OAI.Ostmann.symbolic_root_error line 57

Source documentation

The polynomial-root loss remains negligible after the same costs.

theorem symbolic_root_error (C c : ℝ) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 2 + C * L * Real.exp ((1 / 1000 : ℝ) * L)) *
        Real.exp (-c * Real.exp ((4 / 1000 : ℝ) * L)) ≤
          Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) :=
…

theorem OAI.Ostmann.bulk_progression_error line 66

Source documentation

The error from the bulk progression formula after counting joint boxes.

theorem bulk_progression_error (C c : ℝ) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 2 + C * L * Real.exp ((14 / 10000 : ℝ) * L)) *
        Real.exp (-c * Real.exp ((16 / 10000 : ℝ) * L)) ≤
          Real.exp (-Real.exp ((125 / 100000 : ℝ) * L)) :=
…

theorem OAI.Ostmann.internal_prime_error line 76

Source documentation

Both the prime-square exclusions and the nonzero-polynomial prime-divisor loss have the stronger internal-prime saving.

theorem internal_prime_error (C c : ℝ) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 2 + C * L * Real.exp ((1 / 1000 : ℝ) * L)) *
        Real.exp (-c * Real.exp ((1 / 100 : ℝ) * L)) ≤
          Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) :=
…

theorem OAI.Ostmann.giant_variation_error line 85

Source documentation

Freezing the two giant log coordinates has ample reserve.

theorem giant_variation_error (C : ℝ) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 2 + C * L * Real.exp ((12 / 1000 : ℝ) * L)) *
        Real.exp (-Real.exp ((15 / 1000 : ℝ) * L)) ≤
          Real.exp (-Real.exp ((13 / 1000 : ℝ) * L)) := by
…

theorem OAI.Ostmann.giant_progression_error line 95

Source documentation

Summing the giant progression errors over all boxes and residues.

theorem giant_progression_error (C c : ℝ) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 2 + C * L * Real.exp ((15 / 1000 : ℝ) * L)) *
        Real.exp (-c * Real.exp ((18 / 1000 : ℝ) * L)) ≤
          Real.exp (-Real.exp ((13 / 1000 : ℝ) * L)) :=
…

theorem OAI.Ostmann.giant_integer_error line 104

Source documentation

The elementary external-integer error has a stronger saving.

theorem giant_integer_error (C c : ℝ) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop,
      Real.exp (C * L ^ 2 + C * L * Real.exp ((15 / 1000 : ℝ) * L)) *
        Real.exp (-c * Real.exp ((49 / 1000 : ℝ) * L)) ≤
          Real.exp (-Real.exp ((13 / 1000 : ℝ) * L)) :=
…