ComparisonClassSum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite summation over the residual integer, canceled primes, and grid.

lemma OAI.TotientAsymptotic.finite_class_card_bound line 13
lemma OAI.TotientAsymptotic.canceled_tuple_mass line 23

theorem OAI.TotientAsymptotic.comparison_class_sum line 33

Source documentation

The actual finite class partition has no independence requirement: its image is only enlarged to the product of the available choices.

theorem comparison_class_sum {α γ : Type*} [DecidableEq γ]
    (Q : Finset α) (D P : Finset ℕ) (G : Finset γ) (c : ℕ)
    (d : α → ℕ) (p : α → Fin c → ℕ) (g : α → γ) (A : ℝ)
    (hD : ∀ q ∈ Q, d q ∈ D)
    (hP : ∀ q ∈ Q, ∀ j, p q j ∈ P)
    (hG : ∀ q ∈ Q, g q ∈ G)
    (hclass : ∀ a ∈ D, ∀ v ∈ Fintype.piFinset (fun _ : Fin c => P), ∀ z ∈ G,
      ((Q.filter (fun q => (d q,p q,g q)=(a,v,z))).card : ℝ) ≤
        A*(a : ℝ)⁻¹*∏ j : Fin c, (((v j-1 : ℕ) : ℝ)⁻¹)) :
    (Q.card : ℝ) ≤ A*(G.card : ℝ)*(∑ a ∈ D, (a : ℝ)⁻¹)*
      (∑ p ∈ P, (((p-1 : ℕ) : ℝ)⁻¹))^c := by
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.a

theorem OAI.TotientAsymptotic.comparison_class_sum_mertens line 67

Source documentation

Enlarge residuals to all smooth integers only after applying the class estimate. Mertens bounds both the smooth sum and each canceled prime sum.

theorem comparison_class_sum_mertens (hmertens : MertensProductInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {α γ : Type*} [DecidableEq γ]
      (Q : Finset α) (D : Finset ℕ) (G : Finset γ) (c Nz Np : ℕ)
      (d : α → ℕ) (p : α → Fin c → ℕ) (g : α → γ) (A : ℝ),
      2 ≤ Nz → 2 ≤ Np → 0 ≤ A →
      (∀ a ∈ D, 0 < a ∧ largestPrimeFactor a ≤ Nz) →
      (∀ q ∈ Q, d q ∈ D) →
      (∀ q ∈ Q, ∀ j, (p q j).Prime ∧ p q j ≤ Np) →
      (∀ q ∈ Q, g q ∈ G) →
      (∀ a ∈ D, ∀ v ∈ Fintype.piFinset (fun _ : Fin c => (Finset.Icc 2 Np).filter Nat.Prime),
        ∀ z ∈ G, ((Q.filter (fun q => (d q,p q,g q)=(a,v,z))).card : ℝ) ≤
          A*(a : ℝ)⁻¹*∏ j : Fin c, (((v j-1 : ℕ) : ℝ)⁻¹)) →
…

Mentions: OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.largestPrimeFactor