OAI/NumberTheory/TotientAsymptotic/TwoCoordinateCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two-coordinate instance of Ford Lemma 4.2, before absorbing errors.

  1. def OAI.TotientAsymptotic.coordinateCutoffPairs line 12
  2. lemma OAI.TotientAsymptotic.coordinateCutoffPairs_card line 17
  3. lemma OAI.TotientAsymptotic.coordinateCutoffPairs_data line 27
  4. theorem OAI.TotientAsymptotic.two_coordinate_violation_count line 41

    Source documentation

    Every counted value has some violating preimage. Its regularity controls all preimages, allowing the actual witness to supply the grid cell.

    theorem two_coordinate_violation_count : ∃ C D : ℝ,0 < C ∧ 0 < D ∧
    ∀ (X K L : ℕ) (ω : ℝ),4 ≤ X → 12 ≤ B X → 0 ≤ ω → 2 ≤ L → L ≤ K →
    (L:ℝ)+2 ≤ B X/2 → (K:ℝ) ≤ B X+2 →
    Real.exp K ≤ Real.log X/(20*B X) → ∀ Q : Finset ℕ,
    (∀ v ∈ Q,v ≤ X ∧ CountingRegular (loglogCutoff L) X v ∧
      ∃ n : ℕ,0 < n ∧ n.totient=v ∧
        (1+ω)*B X < a 1*fordPrimeCoordinate n 1+a 2*fordPrimeCoordinate n 2) →
    (Q.card:ℝ) ≤ C*X*(K+1:ℕ)^2*
      Real.exp (-(1+ω)*B X+(3/2:ℝ)*(B X+5-K)+4*B (loglogCutoff L)+5*D+
        8*Real.sqrt (B (loglogCutoff L)*K)) := by
…

    Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.CountingRegular, OAI.TotientAsymptotic.loglogCutoff, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.fordPrimeCoordinate