OAI/NumberTheory/TotientAsymptotic/NormalizedComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ford's cutoff restrictions in the normalized coordinates of the finite grid.

  1. def OAI.TotientAsymptotic.comparisonCutoffs line 13
  2. lemma OAI.TotientAsymptotic.comparisonCutoffs_doubleLog line 16
  3. lemma OAI.TotientAsymptotic.comparison_upper_cutoff_power line 21
  4. theorem OAI.TotientAsymptotic.ford_parameters_of_normalized_grid line 34

    Source documentation

    A finite grid with these normalized inequalities satisfies exactly the published Ford parameter restrictions, including the first-cutoff power.

    theorem ford_parameters_of_normalized_grid : ∀ᶠ y : ℝ in atTop,
    ∀ b D r : ℕ, ∀ S : ℝ, ∀ ν μ : ℕ → ℝ,
    1 ≤ b → ν 0=1 → Real.exp (Real.exp 1) ≤ S → S ≤ comparisonCutoffs y ν b →
    (∀ j ∈ Finset.range b, ν (j+1) < μ j ∧ μ j < ν j) → ν 1 ≤ 4/5 →
    (∀ j ∈ Finset.Icc 2 b,
      2*Real.sqrt (B S/B y) < ν (j-1)-ν j) →
    1 ≤ D → (D : ℝ) ≤ y^(1/100 : ℝ) →
    (largestPrimeFactor D : ℝ) ≤ comparisonCutoffs y ν b →
    1 ≤ r → (r : ℝ) ≤ y^(1/10 : ℝ) →
    FordComparisonParameters b y S D r (comparisonCutoffs y ν) (comparisonCutoffs y μ) := by
…

    Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.comparisonCutoffs, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.FordComparisonParameters