ResidualTupleRecovery.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact tuple data hidden in a comparison residual, on either side of the prefix cut.

def OAI.TotientAsymptotic.residualTupleData line 14
lemma OAI.TotientAsymptotic.prod_after_cut line 19
lemma OAI.TotientAsymptotic.residualTupleData_denominator line 35
lemma OAI.TotientAsymptotic.residualTupleData_primes line 49
theorem OAI.TotientAsymptotic.residual_tuple_data_card line 58
Source documentation
Different full witnesses can give the same residual tuple. Counting its distinct values uses only the number of prime occurrences of the residual.
```
theorem residual_tuple_data_card {x : ℝ} {H k D : ℕ}
    (S : Finset (RemainderDatum (L x H))) (hD : 0 < D)
    (hL : L x H < m x) (hR : R x H < L x H)
    (hS : ∀ η ∈ S, IsBasicRemainder x H η)
    (hval : ∀ η ∈ S, (suffixPreimage η k).totient=D) :
    (S.image (fun η => residualTupleData η k)).card ≤
      (R x H-k+1)^D.primeFactorsList.length := by
…
```
Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.residualTupleData
theorem OAI.TotientAsymptotic.prefix_recovered_from_residual line 75
Source documentation
The known comparison primes and the residual tuple determine the original prefix datum, including when the comparison cut is beyond R.
```
theorem prefix_recovered_from_residual {x : ℝ} {H k : ℕ}
    {η ξ : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) (hξ : IsBasicRemainder x H ξ)
    (hL : L x H < m x) (hkL : k < L x H)
    (hknown : ∀ r ∈ Finset.Icc 1 k, remainderPrime η r=remainderPrime ξ r)
    (hdata : residualTupleData η k=residualTupleData ξ k) :
    prefixOfRemainder x H η=prefixOfRemainder x H ξ := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.remainderPrime, OAI.TotientAsymptotic.residualTupleData, OAI.TotientAsymptotic.prefixOfRemainder