SuffixFactorization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact suffix totient factorizations for basic witnesses.

def OAI.TotientAsymptotic.suffixPreimage line 14
lemma OAI.TotientAsymptotic.suffixPreimage_pos line 17
lemma OAI.TotientAsymptotic.basic_prime_coprime_suffix line 25
lemma OAI.TotientAsymptotic.totient_prime_product_exact line 49
theorem OAI.TotientAsymptotic.basic_suffix_totient_split line 80
Source documentation
Cutting a basic witness strictly before its final displayed prime gives an exact multiplicative totient split. Repetitions inside the final cofactor are retained.
```
theorem basic_suffix_totient_split {x : ℝ} {H i j : ℕ}
    {η : RemainderDatum (L x H)} (hη : IsBasicRemainder x H η)
    (hL : L x H < m x) (hij : i ≤ j) (hjL : j < L x H) :
    (suffixPreimage η i).totient = (suffixPreimage η j).totient *
      ∏ r ∈ Finset.Icc (i+1) j, (remainderPrime η r-1) := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.remainderPrime
lemma OAI.TotientAsymptotic.suffixPreimage_at_R line 106