MovingInternalErrorRate.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual internal arithmetic error at the source's prime scales

def OAI.Ostmann.movingInternalArithmeticError line 11

theorem OAI.Ostmann.moving_internal_log_height line 19

Source documentation

The logarithm of the polynomial height, before the prime-divisor count. Only the sampled-coordinate lower cutoff will divide this expression.

theorem moving_internal_log_height (n d : ℕ) (F U C D L : ℝ)
    (hF : 1 ≤ F) (hU : 1 ≤ U) (hC : 0 ≤ C) (hD : 0 ≤ D) (hL : 1 ≤ L)
    (hfreq : Real.log F ≤ C * L) (hdegree : (d : ℝ) ≤ D * L)
    (hvalue : Real.log U ≤ Real.exp ((12 / 1000 : ℝ) * L)) :
    Real.log (2 * ((2 * (F * U ^ d)) ^ (n + 1)) ^ 2) ≤
      (1 + 2 * ((n : ℝ) + 1) * (1 + C + D)) * L *
        Real.exp ((12 / 1000 : ℝ) * L) := by
…

theorem OAI.Ostmann.moving_internal_error_small line 56

Source documentation

The source's three internal errors have a common exponential saving. The prime-divisor term is evaluated with the internal-prime cutoff.

theorem moving_internal_error_small (n c : ℕ) (C D E : ℝ)
    (hC : 0 ≤ C) (hD : 0 ≤ D) (hE : 0 ≤ E) :
    ∀ᶠ L : ℝ in atTop, ∀ (d : ℕ) (F U α β : ℝ),
      1 ≤ F → 1 ≤ U → 0 ≤ α →
      α ≤ Real.exp (E * L - Real.exp ((39 / 10000 : ℝ) * L)) → 0 ≤ β →
      Real.log F ≤ C * L → (d : ℝ) ≤ D * L →
      Real.log U ≤ Real.exp ((12 / 1000 : ℝ) * L) →
      β ≤ Real.exp (E * L - Real.exp ((1 / 100 : ℝ) * L)) →
      movingInternalArithmeticError n c d F U α β (Real.exp ((1 / 100 : ℝ) * L)) ≤
      Real.exp (-((1 / 2 : ℝ) * Real.exp ((39 / 10000 : ℝ) * L))) := by
…

Mentions: OAI.Ostmann.movingInternalArithmeticError

theorem OAI.Ostmann.moving_internal_error_with_cost line 154

Source documentation

Summing equality patterns and paying the true pointwise kernel/spectator cost still leaves the stated internal-prime error.

theorem moving_internal_error_with_cost (n c : ℕ) (C D E Cprior B : ℝ)
    (hC : 0 ≤ C) (hD : 0 ≤ D) (hE : 0 ≤ E) (hCprior : 1 ≤ Cprior) (_hB : 0 ≤ B) :
    ∀ᶠ L : ℝ in atTop, ∀ (d : ℕ) (F U α β : ℝ),
      1 ≤ F → 1 ≤ U → 0 ≤ α →
      α ≤ Real.exp (E * L - Real.exp ((39 / 10000 : ℝ) * L)) → 0 ≤ β →
      Real.log F ≤ C * L → (d : ℝ) ≤ D * L →
      Real.log U ≤ Real.exp ((12 / 1000 : ℝ) * L) →
      β ≤ Real.exp (E * L - Real.exp ((1 / 100 : ℝ) * L)) →
      ((2 : ℝ) ^ ((4 * n * 2 ^ n) ^ 2) *
        (max 2 (Real.exp (Cprior * L))) ^ (4 * n * 2 ^ n)) *
        Real.exp (B * L ^ 2 + B * L * Real.exp ((1 / 1000 : ℝ) * L)) *
        movingInternalArithmeticError n c d F U α β (Real.exp ((1 / 100 : ℝ) * L)) ≤
…

Mentions: OAI.Ostmann.movingInternalArithmeticError