CommonSquarefreeMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The common-largest-prime bound for the globally squarefree application.

theorem OAI.TotientAsymptotic.common_prime_squarefree_mass_bound line 11

theorem OAI.TotientAsymptotic.common_largest_prime_squarefree_mass_bound line 61

Source documentation

The equal-largest-prime branch, for the original finite family of pairs.

theorem common_largest_prime_squarefree_mass_bound : ∃ C D : ℝ,0 < C ∧ 0 < D ∧
    ∀ (k a b : ℕ) (i : Fin k) (y T U V I : ℝ),0 < a → 0 < b →
    Real.exp 2 ≤ y → 1 ≤ B y → 1 < T → 1 ≤ k → 2 ≤ U →
    U ≤ V → (k:ℝ)*(B V-B U+D) ≤ I →
    ∀ Q : Finset (PairedFactors k),
    (∀ f ∈ Q,CommonLargestConditions a b i y T U V I f) →
    (∀ f ∈ Q,Squarefree (pairedProduct f)) →
    (∑ f ∈ Q,(pairedProduct f:ℝ)⁻¹) ≤
      (C*(B y)^2/(Real.log T)^2)*Real.exp (I*(Real.log k+1)) := by
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.PairedFactors, OAI.TotientAsymptotic.CommonLargestConditions, OAI.TotientAsymptotic.pairedProduct