DistinctLargestMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The unequal-largest-prime branch, including the finite choice of cross slots.

theorem OAI.TotientAsymptotic.distinct_largest_fixed_slots_mass_bound line 10

theorem OAI.TotientAsymptotic.distinct_largest_prime_mass_bound line 53

Source documentation

Summing over the two recorded cross slots costs at most k^2.

theorem distinct_largest_prime_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 < T → 1 ≤ k → 2 ≤ U → U ≤ V →
    (k:ℝ)*(B V-B U+D) ≤ I → ∀ Q : Finset (PairedFactors k),
    (∀ f ∈ Q,DistinctLargestConditions a b i y T U V I f) →
    (∀ f ∈ Q,Squarefree (pairedProduct f)) →
    (∑ f ∈ Q,(pairedProduct f:ℝ)⁻¹) ≤
      (k:ℝ)^2*(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.DistinctLargestConditions, OAI.TotientAsymptotic.pairedProduct