TupleCandidate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.TotientAsymptotic.remainderTail_dvd_suffix line 12
lemma OAI.TotientAsymptotic.basic_tail_lt_all_tuple_primes line 23
theorem OAI.TotientAsymptotic.basic_tuple_candidate_realizes line 55
Source documentation
Every basic tuple has the candidate obtained by replacing its arithmetic tail by the least inverse image of the same tail totient.
```
theorem basic_tuple_candidate_realizes : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ t : ℝ, ∀ τ : TotientTuple (R x H), IsBasicTuple x H t τ →
      (tupleLeastCandidate τ).totient=tupleValue τ := by
…
```
Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsBasicTuple, OAI.TotientAsymptotic.tupleLeastCandidate, OAI.TotientAsymptotic.tupleValue