OAI/NumberTheory/TotientAsymptotic/CommonLargestPrime.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Recoverable extraction of the common largest prime from an actual pair of factors.

  1. def OAI.TotientAsymptotic.commonLargestEncoding line 12
  2. def OAI.TotientAsymptotic.commonPrimeDecode line 16
  3. structure OAI.TotientAsymptotic.CommonLargestConditions line 19
  4. lemma OAI.TotientAsymptotic.commonLargest_divisors line 35
  5. lemma OAI.TotientAsymptotic.commonLargest_decode line 45
  6. lemma OAI.TotientAsymptotic.commonLargest_product line 51
  7. lemma OAI.TotientAsymptotic.commonLargest_witness line 59
  8. lemma OAI.TotientAsymptotic.commonLargest_residual line 84
  9. theorem OAI.TotientAsymptotic.common_largest_prime_mass_bound line 103

    Source documentation

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

    theorem common_largest_prime_mass_bound : ∃ C U₀ : ℝ,0 < C ∧ 2 ≤ U₀ ∧
    ∀ (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 → U₀ ≤ U →
    4*(k:ℝ)^2 ≤ U → U ≤ V → (k:ℝ)*(B V-B U+1) ≤ I →
    ∀ Q : Finset (PairedFactors k),
    (∀ f ∈ Q,CommonLargestConditions a b i y T U V I f) →
    (∑ f ∈ Q,(pairedProduct f:ℝ)⁻¹) ≤
      (C*(B y)^2/(Real.log T)^2)*Real.exp (I*(Real.log k+1)+1) := by
…

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