PPTLabeledResidualCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual residual partition using its finite arithmetic labels. The reciprocal-factor entropy is a proved bound, not an additional input.

theorem OAI.TotientAsymptotic.ppt_labeled_residual_count line 16

Source documentation

Once the pointwise grids have been assigned, the full finite label space absorbs their entropy while retaining every inverse-power saving.

theorem ppt_labeled_residual_count (d : ℕ) (hd : 0 < d)
    {A γ : ℝ} (hA : 0 < A) (hγ : 0 < γ) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (H : ℕ) (δ : ℝ) (R : Finset ℕ) (label : ℕ → PPTResidualLabel)
      (W V : PPTResidualLabel → ℝ) (Y U : PPTResidualLabel → ℕ → ℝ)
      (tail : (l : PPTResidualLabel) → Fin (pptLabelH l) → ℕ)
      (pair : (l : PPTResidualLabel) → ℕ → ShiftedPair (pptLabelB l)),
      (H : ℝ) ≤ A*Real.log (B z) → 0 < δ → 1/B z ≤ δ →
      (∀ n ∈ R, label n ∈ pptResidualLabels (discardPrimeBound (B z)) H δ) →
      (∀ l ∈ R.image label, 1 ≤ pptLabelB l ∧ pptLabelB l ≤ H ∧ pptLabelH l ≤ H) →
      (∀ l ∈ R.image label, 1 < W l ∧ 0 ≤ B (W l) ∧ W l ≤ V l) →
      (∀ l ∈ R.image label,
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.PPTResidualLabel, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.pptLabelH, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.pptLabelB, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptResidualLabels, OAI.TotientAsymptotic.discardPrimeBound