OAI/NumberTheory/Ostmann/Arithmetic/MovingFinalRate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Specializing the final decay to the actual frequency rate

  1. theorem OAI.Ostmann.eventually_moving_frequency_rate_margin line 11
  2. theorem OAI.Ostmann.bulk_exponential_lower_contradicts_decay line 24
  3. theorem OAI.Ostmann.eventually_moving_numeric_contradiction line 39

    Source documentation

    The precise numerical upper bound already proved for the selected-prior statistic contradicts the lower bound preserved by the transfer iteration.

    theorem eventually_moving_numeric_contradiction (Bs BD Bz B C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ k : ℕ in atTop, ∀ᶠ L : ℝ in atTop,
      let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.spectatorBulkCount