ArithmeticNormRate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The numerical rate after the actual arithmetic frequency sum

theorem OAI.Ostmann.arithmetic_frequency_budget_rate line 12

Source documentation

The divisor constant is chosen uniformly before the history-dependent modulus. This is the numerical estimate used by the same-assignment norm.

theorem arithmetic_frequency_budget_rate (n : ℕ) (K C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
    ∀ᶠ m : ℝ in atTop, ∃ D : ℝ, 0 ≤ D ∧
      (∀ q : ℕ, q ≠ 0 → (q : ℝ) ≤ Real.exp (2 * C * m) → (q.divisors.card : ℝ) ≤ D) ∧
      ∀ N V : ℕ, ∀ Δ : ℝ, (N : ℝ) ≤ Real.exp (C * m) →
      (V : ℝ) ≤ Real.exp (Δ + Real.sqrt (4 * m)) →
      Real.exp (-(2 ^ n : ℕ) * Δ + K) *
        ((8 * D ^ 4 * (1 + Real.log N) ^ 3) ^ (2 ^ n - 1) *
          (2 * (V : ℝ)) ^ (2 * 2 ^ n)) ≤
        Real.exp ((2 ^ n : ℕ) * Δ + ε * m) := by
…

theorem OAI.Ostmann.arithmetic_norm_page_spectator_cost line 59
Source documentation
There are r*m bulk Page factors and m spectators. Their combined loss is exactly 2 * 6^(r*m), independently of the depth.
```
theorem arithmetic_norm_page_spectator_cost (n m : ℕ) :
    (2 : ℝ) ^ (2 ^ n * m) * 2 * 3 ^ (2 ^ n * m) =
      2 * Real.exp (Real.log 6 * (2 ^ n : ℕ) * m) := by
…
```

theorem OAI.Ostmann.arithmetic_norm_budget_rate line 70

Source documentation

Fixed profile constants are absorbed without changing the coefficient log 6 of the bulk cost.

theorem arithmetic_norm_budget_rate (n : ℕ) (A C ε : ℝ) (hA : 0 ≤ A) (hC : 0 ≤ C) (hε : 0 < ε) :
    ∀ᶠ m : ℝ in atTop, ∃ D : ℝ, 0 ≤ D ∧
      (∀ q : ℕ, q ≠ 0 → (q : ℝ) ≤ Real.exp (2 * C * m) → (q.divisors.card : ℝ) ≤ D) ∧
      ∀ N V : ℕ, ∀ Δ : ℝ, (N : ℝ) ≤ Real.exp (C * m) →
      (V : ℝ) ≤ Real.exp (Δ + Real.sqrt (4 * m)) →
      (A * Real.exp (-(2 ^ n : ℕ) * Δ)) *
        ((2 * Real.exp (Real.log 6 * (2 ^ n : ℕ) * m)) *
          ((8 * D ^ 4 * (1 + Real.log N) ^ 3) ^ (2 ^ n - 1) *
            (2 * (V : ℝ)) ^ (2 * 2 ^ n))) ≤
        Real.exp ((2 ^ n : ℕ) * Δ + Real.log 6 * (2 ^ n : ℕ) * m + ε * m) := by
…