LocalBadCandidates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual failed candidates admit normal, ordered, maximal-prefix residuals.

def OAI.TotientAsymptotic.localBadCandidates line 13
lemma OAI.TotientAsymptotic.normal_prime_divisor_suffix line 16

theorem OAI.TotientAsymptotic.local_bad_candidate_prefix_data line 28

Source documentation

The decomposition is made on the actual failed finite family, retaining normality at the chosen residual scale for every prime of every residual.

theorem local_bad_candidate_prefix_data {c : ℝ} (hc : 0 < c)
    (d : ℕ) (hd : 0 < d) (L : ℕ) :
    ∀ᶠ H : ℕ in atTop,∀ᶠ x : ℝ in atTop,
      ∃ (p : ℕ → ℕ → ℕ) (j : ℕ → ℕ),∀ b ∈ localBadCandidates x c d L H,
        b=pptSuffixProduct (p b) (m x-H+1) 0 ∧
        (∀ i < m x-H+1,(p b i).Prime) ∧
        (∀ i k : ℕ,i < k → k < m x-H+1 → p b k < p b i) ∧
        j b < m x-H+1 ∧ 0 < pptPrefixProduct (p b) (j b) ∧
        b=pptPrefixProduct (p b) (j b)*pptSuffixProduct (p b) (m x-H+1) (j b) ∧
        PPTBadResidual d (pptSuffixProduct (p b) (m x-H+1) (j b)) ∧
        ∀ q : ℕ,q.Prime → q ∣ pptSuffixProduct (p b) (m x-H+1) (j b) →
          IsNormalPrime (localNormalityScale (m x-(j b-1))) q := by
…

Mentions: OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.localBadCandidates, OAI.TotientAsymptotic.pptSuffixProduct, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.pptPrefixProduct, OAI.TotientAsymptotic.PPTBadResidual, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.localNormalityScale