AttachTail.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing a basic remainder from its prime prefix and finite tail witness.

def OAI.TotientAsymptotic.attachTail line 12
lemma OAI.TotientAsymptotic.remainderPrime_attachTail line 18
lemma OAI.TotientAsymptotic.attachTail_prefix line 26
lemma OAI.TotientAsymptotic.extract_attachTail line 37
lemma OAI.TotientAsymptotic.attach_extractTail line 61
theorem OAI.TotientAsymptotic.prefixDatum_iff_attach_witness line 91
Source documentation
Prime-prefix membership is exactly a union over the genuine finite tail witnesses. This is an equality of admissible data, before any approximation.
```
theorem prefixDatum_iff_attach_witness {x : ℝ} {H d : ℕ}
    (hPH : P H < H) (hHm : H ≤ m x) (p : Fin (R x H) → ℕ) :
    IsPrefixDatum x H ⟨p,d⟩ ↔ ∃ η ∈ witnesses H (theta x) d,
      IsBasicRemainder x H (attachTail x H p η) := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsPrefixDatum, OAI.TotientAsymptotic.witnesses, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.attachTail