AllPreimageCoverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform arithmetic extraction for every preimage outside explicit exceptional values.

def OAI.TotientAsymptotic.basicExceptionValues line 13
lemma OAI.TotientAsymptotic.all_preimages_basic line 17
lemma OAI.TotientAsymptotic.all_preimages_tuple_value line 56
Source documentation
Every preimage of an ordinary value induces a tuple with that exact value.
```
lemma all_preimages_tuple_value {H : ℕ} (hPH : P H < H) (hP : 1 ≤ P H) :
    ∀ᶠ x : ℝ in atTop, ∀ v ∈ totientValues x, v ∉ basicExceptionValues x H →
    ∀ n : ℕ, 0 < n → n.totient = v →
      witnessTuple (fordPrime n 0) (fordRemainder x H n) ∈ tupleFinset x H x ∧
      tupleValue (witnessTuple (fordPrime n 0) (fordRemainder x H n)) = v := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.totientValues, OAI.TotientAsymptotic.basicExceptionValues, OAI.TotientAsymptotic.witnessTuple, OAI.TotientAsymptotic.fordPrime, OAI.TotientAsymptotic.fordRemainder, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.tupleValue