ArithmeticPrimeNormRate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The frequency budget after return to the original prime law

theorem OAI.Ostmann.arithmetic_prime_page_spectator_cost line 13

theorem OAI.Ostmann.arithmetic_prime_norm_budget_rate line 30

Source documentation

The prime-cell mixture adds one factor two per bulk coordinate. This changes the constant in the exponential from log six to log twelve.

theorem arithmetic_prime_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 12 * (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 12 * (2 ^ n : ℕ) * m + ε * m) := by
…

theorem OAI.Ostmann.arithmetic_prime_fourier_budget_rate line 55
Source documentation
Specialization to the actual even bulk size, with the literal window and Page/spectator constants of the prime norm estimate.
```
theorem arithmetic_prime_fourier_budget_rate (ψ : 𝓢(ℝ, ℂ)) (n k : ℕ) (hk : 0 < k)
    (B C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount