OAI/NumberTheory/Ostmann/Construction/FinalArithmeticContradiction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The final contradiction with the actual arithmetic error scale

  1. theorem OAI.Ostmann.arithmetic_error_sum_eventually line 12
  2. theorem OAI.Ostmann.eventual_final_arithmetic_contradiction line 58

    Source documentation

    The final comparison needs precisely the ordinary exponential bulk saving supplied by the quartet argument, plus the negligible arithmetic error. No double-exponential assumption is made on that bulk saving.

    theorem eventual_final_arithmetic_contradiction (n k : ℕ) (hk : 0 < k)
    (B₁ D C δ : ℝ) (hδ : 0 < δ)
    (hentropy : C + D + 2 * B₁ + δ ≤ (n : ℝ) * Real.log 2 - 1) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.spectatorBulkCount