PPTTrivialFibers.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The elementary part of Ford's full-fiber construction, The distribution of totients, Section 5, p. 25, immediately after (5.18). Its candidates have every prime divisor larger than the fixed seed plus one. Their target preimages which contain the candidate are exactly its multiples by seed preimages. Thus the sieve only has to exclude preimages which do not contain the candidate.

This reduction does not prove the abundance of candidates, or the bound on the candidates with a nontrivial preimage.

lemma OAI.TotientAsymptotic.prime_le_seed_add_one line 22
Source documentation
Every prime divisor of an inverse image of d is at most d+1.
```
lemma prime_le_seed_add_one {d m p : ℕ} (hd : 0 < d) (hm : m.totient = d)
    (hp : p.Prime) (hpm : p ∣ m) : p ≤ d+1 := by
…
```
Mentions: OAI.TotientAsymptotic.m
lemma OAI.TotientAsymptotic.seed_preimage_coprime line 32
Source documentation
A candidate supported on primes above d+1 is coprime to every seed preimage, independently of the number or exponents of its prime factors.
```
lemma seed_preimage_coprime {d b m : ℕ} (hd : 0 < d) (hm : m.totient = d)
    (hrough : ∀ p : ℕ, p.Prime → p ∣ b → d+1 < p) : b.Coprime m := by
…
```
Mentions: OAI.TotientAsymptotic.m
lemma OAI.TotientAsymptotic.seed_multiple_totient line 38
lemma OAI.TotientAsymptotic.target_multiple_coprime line 46
Source documentation
A repeated candidate prime in the residual factor would make the totient at least that prime times the candidate totient, exceeding the fixed multiplier d.
```
lemma target_multiple_coprime {d b m : ℕ} (hb : 0 < b) (hm : 0 < m)
    (heq : (b*m).totient = d*b.totient)
    (hrough : ∀ p : ℕ, p.Prime → p ∣ b → d+1 < p) : b.Coprime m := by
…
```
Mentions: OAI.TotientAsymptotic.m

lemma OAI.TotientAsymptotic.target_preimage_of_dvd line 66

Source documentation

Every target preimage divisible by the candidate has exactly a seed preimage as its residual factor.

lemma target_preimage_of_dvd {d b n : ℕ} (hb : 0 < b) (hn : 0 < n)
    (heq : n.totient = d*b.totient) (hbn : b ∣ n)
    (hrough : ∀ p : ℕ, p.Prime → p ∣ b → d+1 < p) :
    ∃ m : ℕ, 0 < m ∧ m.totient = d ∧ n = b*m := by
…

Mentions: OAI.TotientAsymptotic.m

theorem OAI.TotientAsymptotic.fullFiber_iff_all_preimages_dvd line 83
Source documentation
For Ford's rough candidates, full-fiber preservation is equivalent to excluding target preimages which are not divisible by the candidate.
```
theorem fullFiber_iff_all_preimages_dvd {d b : ℕ} (hd : 0 < d) (hb : 0 < b)
    (hrough : ∀ p : ℕ, p.Prime → p ∣ b → d+1 < p) :
    FullFiber d b ↔ ∀ n : ℕ, 0 < n → n.totient = d*b.totient → b ∣ n := by
…
```
Mentions: OAI.TotientAsymptotic.FullFiber

lemma OAI.TotientAsymptotic.primeProduct_rough line 98

Source documentation

The roughness hypothesis is inherited by a finite product of primes.

lemma primeProduct_rough {ι : Type*} (I : Finset ι) (p : ι → ℕ) (d : ℕ)
    (hp : ∀ i ∈ I, (p i).Prime) (hlarge : ∀ i ∈ I, d+1 < p i) :
    ∀ q : ℕ, q.Prime → q ∣ ∏ i ∈ I, p i → d+1 < q := by
…

theorem OAI.TotientAsymptotic.primeProduct_fullFiber_iff line 106