CanonicalCoverage.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.TotientAsymptotic.canonical_tuple_coverage line 14
Source documentation
The exact coverage statement once the three explicit exceptional conditions (structure, largest prime, cofactor) have been excluded.
```
lemma canonical_tuple_coverage {x t : ℝ} {H n : ℕ} (hPH : P H < H) (hP : 1 ≤ P H)
    (hm : H ≤ m x) (hn : 0<n)
    (hstruct : extractedStructureCondition x (P H) n)
    (hhead : x^(9/10 : ℝ) ≤ fordPrime n 0)
    (hsize : Real.log (fordCofactor n (L x H+1) : ℝ) ≤ Real.exp (2*bandScale x (L x H)))
    (hval : (n.totient : ℝ) ≤ t)
    (hcop : (fordPrime n 0).Coprime (suffixPreimage (fordRemainder x H n) 0)) :
    n.totient ∈ (tupleFinset x H t).image tupleValue := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.extractedStructureCondition, OAI.TotientAsymptotic.fordPrime, OAI.TotientAsymptotic.fordCofactor, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.fordRemainder, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.tupleValue
theorem OAI.TotientAsymptotic.canonical_tuple_coverage_eventually line 38
Source documentation
The coprimality premise is automatically available uniformly for actual basic remainders once the head lower bound and cofactor cutoff hold.
```
theorem canonical_tuple_coverage_eventually {H : ℕ} (hPH : P H < H) (hP : 1≤P H) :
    ∀ᶠ x : ℝ in atTop, ∀ t : ℝ, ∀ n : ℕ, 0<n →
      extractedStructureCondition x (P H) n → x^(9/10 : ℝ) ≤ fordPrime n 0 →
      Real.log (fordCofactor n (L x H+1) : ℝ) ≤ Real.exp (2*bandScale x (L x H)) →
      (n.totient : ℝ) ≤ t → n.totient ∈ (tupleFinset x H t).image tupleValue := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.extractedStructureCondition, OAI.TotientAsymptotic.fordPrime, OAI.TotientAsymptotic.fordCofactor, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.tupleValue