PPTComparisonSum.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite summation of the fixed-common-factor, fixed-left-tail comparison blocks in Ford's proof of (5.23). The published comparison predicates remain explicit. The extra factor from fixing the left tail is bounded by its already proved normality estimate.

def OAI.TotientAsymptotic.pptComparisonScale line 19
Source documentation
The part of the comparison bound independent of the two fixed integer factors.
```
def pptComparisonScale (C : ℝ) (b : ℕ) (z W : ℝ) (Y U : ℕ → ℝ) : ℝ :=
…
```
lemma OAI.TotientAsymptotic.ppt_comparison_scale_nonneg line 24
lemma OAI.TotientAsymptotic.ppt_comparison_bound_factor line 32
lemma OAI.TotientAsymptotic.ppt_comparison_block_sum line 42

theorem OAI.TotientAsymptotic.ppt_normal_tail_comparison_sum line 80

Source documentation

The total of the actual comparison blocks is bounded by the two reciprocal totient masses and the explicit normal-tail cost. All input conditions are arithmetic or the literal Ford comparison predicates.

theorem ppt_normal_tail_comparison_sum :
    ∃ C z₀ : ℝ, 0 < C ∧ 1 < z₀ ∧
    ∀ (b d h : ℕ) (z W V : ℝ) (Y U : ℕ → ℝ)
      (R A : Finset ℕ) (T : ℕ → ℕ → Finset ℕ)
      (tail : ℕ → Fin h → ℕ)
      (p q : ℕ → ℕ → ℕ → Fin b → ℕ) (e : ℕ → ℕ → ℕ → ℕ),
      0 < d → z₀ ≤ z → 0 ≤ B z → 1 < W → 0 ≤ B W → W ≤ V → 1 ≤ Y b →
      (∀ t ∈ A, t = ∏ i, tail t i) →
      (∀ t ∈ A, Function.Injective (tail t)) →
      (∀ t ∈ A, ∀ i, IsNormalPrime W (tail t i)) →
      (∀ t ∈ A, ∀ i, (largestPrimeFactor (tail t i-1) : ℝ) ≤ V) →
      (∀ c ∈ R, ∀ t ∈ A,
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor

lemma OAI.TotientAsymptotic.ppt_count_le_comparison_blocks line 118
Source documentation
Coverage by the concrete blocks suffices; blocks need not be disjoint, and candidate totients need not be distinct.
```
lemma ppt_count_le_comparison_blocks (S R A : Finset ℕ) (T : ℕ → ℕ → Finset ℕ)
    (hcover : S ⊆ R.biUnion (fun c => A.biUnion (T c))) :
    (S.card : ℝ) ≤ ∑ c ∈ R, ∑ t ∈ A, ((T c t).card : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.A