ArithmeticTwoPrimePatternNormRate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.arithmetic_two_prime_pattern_norm_rate line 15
Source documentation
The actual pattern sum and paired frequency sum have an absolute bulk constant. The cutoff includes the constructed bottom reserve 2 sqrt(m). Only the genuine comparison errors use the full number of histories.
```
theorem arithmetic_two_prime_pattern_norm_rate (ψ : SchwartzMap ℝ ℂ) (n k : ℕ)
    (hk : 0 < k) (hn : n ≤ k) (B Cfreq Cprior ε : ℝ)
    (hCfreq : 0 ≤ Cfreq) (hCprior : 1 ≤ Cprior) (hε : 0 < ε)
    (hdepth : 8 * (Cprior + 1) ≤ (k : ℝ) ^ 3) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount
theorem OAI.Ostmann.arithmetic_two_prime_original_pattern_norm_rate line 94
Source documentation
The actual pattern sum and paired frequency sum have an absolute bulk constant. The cutoff includes the constructed bottom reserve 2 sqrt(m). The fifth error is the literal giant comparison; only comparison errors use the full number of histories.
```
theorem arithmetic_two_prime_original_pattern_norm_rate (ψ : SchwartzMap ℝ ℂ) (n k : ℕ)
    (hk : 0 < k) (hn : n ≤ k) (B Cfreq Cprior ε : ℝ)
    (hCfreq : 0 ≤ Cfreq) (hCprior : 1 ≤ Cprior) (hε : 0 < ε)
    (hdepth : 8 * (Cprior + 1) ≤ (k : ℝ) ^ 3) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount