Richert 1969, hypothesis (A4) and the squareful payment

Frozen source:

• references/richert-1969/richert-1969.pdf, PDF pages 2 and 10, hypothesis (A4) and equation (3.7);
• references/richert-1969/VISION_TRANSCRIPTION.md, sections 1 and 5.

This file identifies the carrier removed by the prime on Richert's weighted sum with a finite union of the p^2 ∣ a fibres. Hypothesis (A4) is then applied fibre by fibre. No sieve fundamental lemma is used here.

def MathlibNt.SieveTheory.Richert1969.wholeSquareDivisibleCarrier (A : Finset ℕ) (p : ℕ) : Finset ℕ

Richert's literal whole-sequence fibre A[p^2] in hypothesis (A4).

Equations

• MathlibNt.SieveTheory.Richert1969.wholeSquareDivisibleCarrier A p = {a ∈ A | p ^ 2 ∣ a}

def MathlibNt.SieveTheory.Richert1969.squareDivisibleCarrier (A : Finset ℕ) (P p : ℕ) : Finset ℕ

The p^2 ∣ a fibre occurring on the left side of Richert's (A4).

Equations

• MathlibNt.SieveTheory.Richert1969.squareDivisibleCarrier A P p = {a ∈ MathlibNt.SieveTheory.Richert1969.lowerCarrier A P | p ^ 2 ∣ a}

theorem MathlibNt.SieveTheory.Richert1969.squareDivisibleCarrier_subset_whole (A : Finset ℕ) (P p : ℕ) : squareDivisibleCarrier A P p ⊆ wholeSquareDivisibleCarrier A p

Sifting only restricts the literal whole-sequence (A4) fibre.

def MathlibNt.SieveTheory.Richert1969.squarefulRemovedCarrier (A Q : Finset ℕ) (P : ℕ) : Finset ℕ

The union of the square-divisible fibres removed by the prime on (3.1).

Equations

• MathlibNt.SieveTheory.Richert1969.squarefulRemovedCarrier A Q P = Q.biUnion fun (p : ℕ) => MathlibNt.SieveTheory.Richert1969.squareDivisibleCarrier A P p

theorem MathlibNt.SieveTheory.Richert1969.squarefulRemovedCarrier_eq_sdiff (A Q : Finset ℕ) (P : ℕ) : squarefulRemovedCarrier A Q P = lowerCarrier A P \ squarefreeWeightedCarrier A Q P

theorem MathlibNt.SieveTheory.Richert1969.squarefulCorrection_eq_removedCarrier_card (A Q : Finset ℕ) (P : ℕ) : squarefulCorrection A Q P = ↑(squarefulRemovedCarrier A Q P).card

The exact squareful correction is the cardinality of the union of the p^2 fibres, not a separate analytic error term.

theorem MathlibNt.SieveTheory.Richert1969.squarefulCorrection_le_sum_squareDivisibleCarrier (A Q : Finset ℕ) (P : ℕ) : squarefulCorrection A Q P ≤ ∑ p ∈ Q, ↑(squareDivisibleCarrier A P p).card

The finite union bound which turns the squareful correction into the sum of the individual (A4) carriers.

def MathlibNt.SieveTheory.Richert1969.SquarefulA4On (A Q : Finset ℕ) (X A4 : ℝ) : Prop

Richert's hypothesis (A4), restricted to the weighted prime carrier used in Theorem 1.

Equations

• MathlibNt.SieveTheory.Richert1969.SquarefulA4On A Q X A4 = ∀ p ∈ Q, ↑(MathlibNt.SieveTheory.Richert1969.wholeSquareDivisibleCarrier A p).card ≤ A4 * (X * Real.log X / ↑p ^ 2 + 1)

theorem MathlibNt.SieveTheory.Richert1969.squarefulCorrection_le_sum_A4 (A Q : Finset ℕ) (P : ℕ) (X A4 : ℝ) (hA4 : SquarefulA4On A Q X A4) : squarefulCorrection A Q P ≤ ∑ p ∈ Q, A4 * (X * Real.log X / ↑p ^ 2 + 1)

Direct use of (A4) in (3.7): the removed carrier is paid by summing the literal A4 * (X log X / p^2 + 1) bounds over the weighted prime interval.

theorem MathlibNt.SieveTheory.Richert1969.theoremOneSquarefulCorrection_le_sum_A4 (A : Finset ℕ) (X : ℝ) (K : ℕ) (v u A4 : ℝ) (hA4 : SquarefulA4On A (theoremOneWeightedPrimes X K u v) X A4) : squarefulCorrection A (theoremOneWeightedPrimes X K u v) (theoremOneSiftingProduct X K v) ≤ ∑ p ∈ theoremOneWeightedPrimes X K u v, A4 * (X * Real.log X / ↑p ^ 2 + 1)

The literal Theorem 1 specialization of the preceding (A4) payment.