PPTResidualCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

All residual block labels are summed before the strict comparison exponent is spent. This retains the exponential-square budget needed for variable dimensions, grid labels, common factors, and small tails.

theorem OAI.TotientAsymptotic.ppt_finite_residual_block_decay line 20

Source documentation

The literal Ford bound, normal small-tail estimate, and strict exponent together control any finite family of actual residual blocks. The only aggregate quantity is the explicit reciprocal-factor mass.

theorem ppt_finite_residual_block_decay (d : ℕ) (hd : 0 < d)
    {A γ M : ℝ} (hA : 0 ≤ A) (hγ : 0 < γ) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (α : Type) (I : Finset α) (b h c a : α → ℕ) (W V : α → ℝ)
      (Y U : α → ℕ → ℝ) (tail : (i : α) → Fin (h i) → ℕ)
      (T : α → Finset ℕ) (t : (i : α) → ℕ → ShiftedPair (b i)),
      (∀ i ∈ I, 1 ≤ b i) →
      (∀ i ∈ I, (b i : ℝ) ≤ A*Real.log (B z)) →
      (∀ i ∈ I, (h i : ℝ) ≤ A*Real.log (B z)) →
      (∀ i ∈ I, 1 < W i ∧ 0 ≤ B (W i) ∧ W i ≤ V i) →
      (∀ i ∈ I, 1 < Y i (b i) ∧ B (Y i (b i)) ≤ 2*(B z)^(2/3 : ℝ)) →
      (∀ i ∈ I, 0 ≤ B (V i) ∧ B (V i) ≤ 2*(B z)^(2/3 : ℝ)) →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B

lemma OAI.TotientAsymptotic.ppt_residual_block_cover line 125

Source documentation

A finite cover by the actual comparison blocks suffices; the blocks need not be disjoint.

lemma ppt_residual_block_cover {α : Type*} [DecidableEq α]
    (I : Finset α) (T : α → Finset ℕ) (R : Finset ℕ) {X : ℝ}
    (hcover : ∀ n ∈ R, ∃ i ∈ I, n ∈ T i)
    (hcount : (∑ i ∈ I, ((T i).card : ℝ)) ≤ X) : (R.card : ℝ) ≤ X := by
…

Mentions: OAI.TotientAsymptotic.R