BandComparison.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The comparison of the exact Ford band centers with the phase-dependent centers in the manuscript, equation alpha-comparison. The ratio is independent of the retained prime index, so its convergence gives a uniform comparison over all indices below m.

def OAI.TotientAsymptotic.bandCenterRatio line 19
lemma OAI.TotientAsymptotic.rho_pow_eq_exp line 21
lemma OAI.TotientAsymptotic.alpha_theta_eq line 26
lemma OAI.TotientAsymptotic.bandScale_pos line 38
lemma OAI.TotientAsymptotic.fordBandScale_eq_ratio_mul line 43
lemma OAI.TotientAsymptotic.fordBandScale_div_bandScale line 54
lemma OAI.TotientAsymptotic.bandCenterRatio_eq_one_add line 59
lemma OAI.TotientAsymptotic.B_tendsto line 67
lemma OAI.TotientAsymptotic.m_tendsto line 70
lemma OAI.TotientAsymptotic.bandCenterRatio_tendsto line 73
theorem OAI.TotientAsymptotic.fordBandScale_uniform_comparison line 109
Source documentation
The error bound is simultaneous over every retained index.
```
theorem fordBandScale_uniform_comparison {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop, ∀ i : ℕ, i < m x →
      |fordBandScale x i / bandScale x i - 1| < ε := by
…
```
Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.bandScale
theorem OAI.TotientAsymptotic.fordBands_imply_modelBands line 120
Source documentation
Ford's four-percent bands lie in the model's ten-percent bands for all sufficiently large endpoints, uniformly over all retained indices.
```
theorem fordBands_imply_modelBands :
    ∀ᶠ x : ℝ in atTop, ∀ i : ℕ, i < m x → ∀ n : ℕ,
      fordBandCondition x (1/25) i n →
        (9/10 : ℝ) * bandScale x i ≤ primeDoubleLog n i ∧
          primeDoubleLog n i ≤ (11/10 : ℝ) * bandScale x i := by
…
```
Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.fordBandCondition, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.primeDoubleLog