PrefixPreimage.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact prime-prefix factorization and minimization over a common inverse fiber.

def OAI.TotientAsymptotic.tuplePrimeProduct line 12
def OAI.TotientAsymptotic.tupleLeastCandidate line 14
lemma OAI.TotientAsymptotic.wholePreimage_prefix_split line 17
lemma OAI.TotientAsymptotic.tuplePrimeProduct_pos line 29
lemma OAI.TotientAsymptotic.ell_of_common_prefix line 35
Source documentation
If every inverse image has a fixed multiplicative prefix, minimizing the remaining inverse image minimizes the whole fiber.
```
lemma ell_of_common_prefix {v d b : ℕ} (hv : IsTotient v) (hd : IsTotient d)
    (hb : 0 < b) (hreal : (b*ell d).totient=v)
    (hcommon : ∀ n : ℕ, 0 < n → n.totient=v →
      ∃ w : ℕ, 0 < w ∧ w.totient=d ∧ n=b*w) :
    ell v=b*ell d := by
…
```
Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.w
lemma OAI.TotientAsymptotic.coprime_of_prime_gt line 45
lemma OAI.TotientAsymptotic.tuple_candidate_realizes line 53
Source documentation
Replacing the tail of a represented value by its least preimage preserves that value once the tail is smaller than every prefix prime.
```
lemma tuple_candidate_realizes {x t : ℝ} {H : ℕ} {τ : TotientTuple (R x H)}
    (hPH : P H ≤ H) (hτ : IsBasicTuple x H t τ)
    {w : ℕ} (hw : 0 < w) (hwd : w.totient=τ.tail.d)
    (hsmall : ∀ i, w < tuplePrimes τ i)
    (hreal : (tuplePrimeProduct τ*w).totient=tupleValue τ) :
    (tupleLeastCandidate τ).totient=tupleValue τ := by
…
```
Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.IsBasicTuple, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.tuplePrimes, OAI.TotientAsymptotic.tuplePrimeProduct, OAI.TotientAsymptotic.tupleValue, OAI.TotientAsymptotic.tupleLeastCandidate