PPTWitnessCount.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite partition of actual regular residuals.

def OAI.TotientAsymptotic.pptLabelTerminalLower line 13
def OAI.TotientAsymptotic.pptLabelTerminalUpper line 16
def OAI.TotientAsymptotic.pptLabelTerminal line 19
def OAI.TotientAsymptotic.pptLabelUpper line 22
def OAI.TotientAsymptotic.pptLabelLower line 26
structure OAI.TotientAsymptotic.PPTResidualGridWitness line 33
Source documentation
Arithmetic evidence retained from the actual terminal-prefix construction for one integer. Each field is supplied by ppt_selected_grid_data; the structure contains no estimate for a finite family.
```
structure PPTResidualGridWitness (d N H : ℕ) (z S A : ℝ) (r : ℕ) where
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.A
theorem OAI.TotientAsymptotic.ppt_witnessed_residual_count line 68
Source documentation
Partition any finite set of actual witnessed residuals, choose the small tail only after fixing its integer label, and apply the saved Ford bound. Witness multiplicities and alternative prime lists do not enter the count.
```
theorem ppt_witnessed_residual_count (d : ℕ) (hd : 0 < d) {A : ℝ}
    (hA : 0 < A) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop, ∀ (N H : ℕ) (S : ℝ) (R : Finset ℕ),
      (H:ℝ) ≤ A*Real.log (B z) → 1 < S → 0 ≤ B S →
      (∀ r∈R,Nonempty (PPTResidualGridWitness d N H z S A r)) →
      (R.card:ℝ) ≤ z/((d:ℝ)*Real.log z)*(B z)^(-K) := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.PPTResidualGridWitness