LeastPrefix.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.unique_tuple_least_preimage line 15
Source documentation
The exact least-preimage identity on the bijective part of the actual representation map. Every preimage, including the least one, has this prefix.
```
theorem unique_tuple_least_preimage : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ τ ∈ tupleFinset x H x \ discardedTuples x H,
      ell (tupleValue τ)=tupleLeastCandidate τ := by
…
```
Mentions: OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.discardedTuples, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.tupleValue, OAI.TotientAsymptotic.tupleLeastCandidate
def OAI.TotientAsymptotic.candidateInWindow line 33
def OAI.TotientAsymptotic.candidateTuples line 36
lemma OAI.TotientAsymptotic.candidate_count_comparison line 39