LocalFullCandidateScale.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Convert a positive fixed-prefix family into the natural counting scale. These finite-family bridges will be applied after the regular residual comparison estimate has been proved.

theorem OAI.TotientAsymptotic.full_fiber_scale_of_local_count line 18

Source documentation

The fixed-prefix normalization differs from the natural scale by a positive constant, and every retained candidate has the exact full-fiber property.

theorem full_fiber_scale_of_local_count {c δ : ℝ} (hc : 0<c) (hδ : 0<δ)
    (d : ℕ) (hd : 0<d) (L : ℕ)
    (hcount : ∀ᶠ H : ℕ in atTop,∀ᶠ x : ℝ in atTop,
      (δ/(16*d))*(x/Real.log x*G x (m x-H)) ≤
        ((localFullCandidates x c d L H).card:ℝ)) :
    ∃ a K : ℝ,0<a ∧ 0<K ∧ ∀ᶠ x : ℝ in atTop,
      0<x ∧ ∃ S : Finset ℕ,a*(x/Real.log x)*G x (m x) ≤ (S.card:ℝ) ∧
        ∀ b∈S,0<b ∧ ((d*b.totient:ℕ):ℝ)≤x ∧
          FullFiber d b ∧ (b:ℝ)/b.totient≤K := by
…

Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.localFullCandidates, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.FullFiber

theorem OAI.TotientAsymptotic.ppt_bounded_fiber_of_scale_family line 48
Source documentation
Ford's upper counting bound converts the constructed family into the published full-fiber density conclusion.
```
theorem ppt_bounded_fiber_of_scale_family (d : ℕ)
    (hfamily : ∃ a K : ℝ,0<a ∧ 0<K ∧ ∀ᶠ x : ℝ in atTop,
      0<x ∧ ∃ S : Finset ℕ,a*(x/Real.log x)*G x (m x) ≤ (S.card:ℝ) ∧
        ∀ b∈S,0<b ∧ ((d*b.totient:ℕ):ℝ)≤x ∧
          FullFiber d b ∧ (b:ℝ)/b.totient≤K) :
    PPTBoundedFiberPropagation d := by
…
```
Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.FullFiber, OAI.TotientAsymptotic.PPTBoundedFiberPropagation

theorem OAI.TotientAsymptotic.ford_scale_lower_of_one_family line 67

Source documentation

With seed one the totient map is injective on the constructed family, so its positive mass proves Ford's lower counting bound.

theorem ford_scale_lower_of_one_family
    (hfamily : ∃ a K : ℝ,0<a ∧ 0<K ∧ ∀ᶠ x : ℝ in atTop,
      0<x ∧ ∃ S : Finset ℕ,a*(x/Real.log x)*G x (m x) ≤ (S.card:ℝ) ∧
        ∀ b∈S,0<b ∧ ((1*b.totient:ℕ):ℝ)≤x ∧
          FullFiber 1 b ∧ (b:ℝ)/b.totient≤K) :
    ∃ a : ℝ,0<a ∧ ∀ᶠ x : ℝ in atTop,a*(x/Real.log x)*G x (m x)≤V x := by
…

Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.FullFiber, OAI.TotientAsymptotic.V