OAI/NumberTheory/TotientAsymptotic/PrimeProductValueMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Distinct residual values of a prime prefix carry no preimage multiplicity.

  1. def OAI.TotientAsymptotic.primeProductValues line 13
  2. lemma OAI.TotientAsymptotic.primeProductValues_positive line 16
  3. lemma OAI.TotientAsymptotic.primeProductValues_mass line 25
  4. theorem OAI.TotientAsymptotic.large_prime_product_value_count line 53

    Source documentation

    Count values with a large leading prime after encoding the remaining prefix and its cofactor by their distinct totient values.

    theorem large_prime_product_value_count : ∀ᶠ x : ℝ in atTop,
    ∀ N : ℕ, ∀ P : Finset (Fin N → ℕ), ∀ D Q : Finset ℕ,
      (∀ p ∈ P, ∀ i, (p i).Prime) → (∀ d ∈ D, 0 < d) →
      (∀ v ∈ Q, ∃ n p : ℕ, 0 < n ∧ n.totient=v ∧ p.Prime ∧ p ∣ n ∧
        x^(1/4:ℝ) ≤ p ∧ (v:ℝ) ≤ x ∧ (n/p).totient ∈ primeProductValues P D) →
      (Q.card:ℝ) ≤ (64*x/Real.log x)*
        (∑ p ∈ P,reciprocalShiftWeight p)*(∑ d ∈ D,(d:ℝ)⁻¹) := by
…

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.primeProductValues, OAI.TotientAsymptotic.reciprocalShiftWeight