Normalization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Normalization of totient counts and uniform coefficient asymptotics.

lemma OAI.TotientAsymptotic.g_pos line 14
lemma OAI.TotientAsymptotic.G_pos line 27
lemma OAI.TotientAsymptotic.scale_eventually_pos line 33
def OAI.TotientAsymptotic.normalizedCount line 40
Also declared: ComparatorChallenges/TotientAsymptotic.lean:113 (same declaration text).
def OAI.TotientAsymptotic.FordScaleBounds line 44
Source documentation
Ford's counting-scale bounds, with constants independent of the endpoint.
```
def FordScaleBounds : Prop :=
…
```
lemma OAI.TotientAsymptotic.normalizedCount_eq line 49
Source documentation
Exact algebra relating the normalization and the manuscript's mass error.
```
lemma normalizedCount_eq (F : ℝ → ℝ) (x : ℝ) :
    normalizedCount F x = F x * Real.log x / (x * G x (m x)) := by
…
```
Mentions: OAI.TotientAsymptotic.normalizedCount, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m
theorem OAI.TotientAsymptotic.ratio_limit_of_normalized_error line 56
Source documentation
A vanishing normalized error becomes a ratio asymptotic when the limiting coefficient is bounded below. No continuity of the coefficient is required.
```
theorem ratio_limit_of_normalized_error (F f : ℝ → ℝ) (c : ℝ) (hc : 0 < c)
    (hcoeff : ∀ s ∈ Set.Ico (0 : ℝ) 1, c ≤ A f s)
    (herr : Tendsto (fun x => normalizedCount F x - A f (theta x))
      atTop (nhds 0)) :
    Tendsto (fun x => F x / (x / Real.log x * G x (m x) * A f (theta x)))
      atTop (nhds 1) := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.normalizedCount, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m

theorem OAI.TotientAsymptotic.coefficient_conclusions_of_internal_comparison line 83

Source documentation

Uniform coefficient bounds and convergence from phase comparison.

theorem coefficient_conclusions_of_internal_comparison
    (hford : FordScaleBounds)
    (hcomp : ∀ ε : ℝ, 0 < ε → ∃ H₀ : ℕ, ∀ H ≥ H₀,
      ∀ᶠ x : ℝ in atTop,
        |normalizedCount V x - AH H (fun _ => 1) (theta x)| ≤ ε) :
    TendstoUniformlyOn (fun H => AH H (fun _ => 1)) (A (fun _ => 1))
      atTop (Set.Ico (0 : ℝ) 1) ∧
    (∃ cMinus cPlus : ℝ, 0 < cMinus ∧
      ∀ s ∈ Set.Ico (0 : ℝ) 1,
        cMinus ≤ A (fun _ => 1) s ∧ A (fun _ => 1) s ≤ cPlus) ∧
    Tendsto (fun x => V x / mainTerm x) atTop (nhds 1) := by
…

Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.normalizedCount, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.AH, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.mainTerm