PPTFixedCoordinateValueCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sum the fixed-coordinate strip estimate over the actual floor partition of the terminal coordinate.

theorem OAI.TotientAsymptotic.ppt_fixed_coordinate_value_count line 15

Source documentation

Distinct values with one fixed bad coordinate retain the exponential saving after all terminal-coordinate strips have been summed.

theorem ppt_fixed_coordinate_value_count (H : ℕ) :
    ∃ C c : ℝ, 0 < C ∧ 0 < c ∧
      ∀ᶠ P : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ N : ℕ, N+3+H=m x → ∀ i : Fin (N+2), P ≤ m x-(i.val+1) →
      ∀ Q : Finset ℕ, ∀ n : ℕ→ℕ,
      (∀ v∈Q, 0 < n v ∧ (n v).totient=v ∧
        x^(1/4:ℝ) ≤ fordPrime (n v) 0 ∧ (v:ℝ) ≤ x ∧
        N+3 ≤ (n v).primeFactorsList.length ∧
        fordPrime (n v) (N+3) < fordPrime (n v) (N+2) ∧
        2 < fordPrimeCoordinate (n v) (N+3) ∧
        ∀ j < N+3, fordRowSum (N+3) (fordPrimeCoordinate (n v)) j ≤
          xi x j*(if j=0 then B x else fordPrimeCoordinate (n v) j)) →
…

Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.fordPrime, OAI.TotientAsymptotic.fordPrimeCoordinate, OAI.TotientAsymptotic.fordRowSum, OAI.TotientAsymptotic.xi, OAI.TotientAsymptotic.B

lemma OAI.TotientAsymptotic.ppt_fixed_coordinate_exponential_sum line 90

Source documentation

Sum the reversed-coordinate exponential weights, retaining the exact fixed terminal loss in the constant.

lemma ppt_fixed_coordinate_exponential_sum {N H P m : ℕ} {c : ℝ}
    (hc : 0 < c) (hm : N+3+H=m) (hP : H+1 ≤ P)
    (I : Finset (Fin (N+2))) (hI : ∀ i∈I,P ≤ m-(i.val+1)) :
    (∑ i∈I,Real.exp (-c*(N+2-(i.val+1):ℕ))) ≤
      (Real.exp (c*(H+1:ℕ))/ (1-Real.exp (-c)))*Real.exp (-c*(P:ℝ)) := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m

theorem OAI.TotientAsymptotic.ppt_fixed_bad_coordinate_value_count line 138

Source documentation

A finite family with some bad retained coordinate has exponentially small cardinality, uniformly after the fixed terminal cutoff.

theorem ppt_fixed_bad_coordinate_value_count (H : ℕ) :
    ∃ C c : ℝ, 0 < C ∧ 0 < c ∧
      ∀ᶠ P : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ N : ℕ, N+3+H=m x → ∀ Q : Finset ℕ, ∀ n : ℕ→ℕ,
      (∀ v∈Q, 0 < n v ∧ (n v).totient=v ∧
        x^(1/4:ℝ) ≤ fordPrime (n v) 0 ∧ (v:ℝ) ≤ x ∧
        N+3 ≤ (n v).primeFactorsList.length ∧
        fordPrime (n v) (N+3) < fordPrime (n v) (N+2) ∧
        2 < fordPrimeCoordinate (n v) (N+3) ∧
        ∀ j < N+3,fordRowSum (N+3) (fordPrimeCoordinate (n v)) j ≤
          xi x j*(if j=0 then B x else fordPrimeCoordinate (n v) j)) →
      (∀ v∈Q,∃ j∈Finset.Icc 1 (m x-P),
…