Arithmetic.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic facts for the weighted companion theorem. The inverse-fiber transport is the elementary consequence used after Ford's propagation construction (The distribution of totients, 2013 revision, Section 5, equations (5.10)--(5.19), and Section 7.3).

lemma OAI.TotientAsymptotic.isTotient_eight line 17
lemma OAI.TotientAsymptotic.ell_eight line 20
theorem OAI.TotientAsymptotic.seed_one line 28
lemma OAI.TotientAsymptotic.fk_le_one line 31
lemma OAI.TotientAsymptotic.fk_pos_iff line 38
lemma OAI.TotientAsymptotic.fk_ell_pos_iff line 52
lemma OAI.TotientAsymptotic.fk_eq_one_sub line 59
lemma OAI.TotientAsymptotic.fk_eq_inv line 65
lemma OAI.TotientAsymptotic.fk_le_inv_succ line 75
lemma OAI.TotientAsymptotic.N_le_V line 95
theorem OAI.TotientAsymptotic.ell_eq_mul_of_full_fiber line 105
Source documentation
The least preimage is preserved by a complete inverse-fiber dilation.
```
theorem ell_eq_mul_of_full_fiber {d v b : ℕ} (hd : IsTotient d) (_hb : 0 < b)
    (hfull : ∀ n : ℕ, (0 < n ∧ n.totient = v) ↔
      ∃ m : ℕ, 0 < m ∧ m.totient = d ∧ n = b*m) :
    ell v = b * ell d := by
…
```
Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.ell

theorem OAI.TotientAsymptotic.ratio_le_of_full_fiber line 119

Source documentation

Ford's full-fiber propagation cannot decrease the least-preimage ratio.

theorem ratio_le_of_full_fiber {d v b : ℕ} (hd : IsTotient d) (hb : 0 < b)
    (hv : v = d*b.totient)
    (hfull : ∀ n : ℕ, (0 < n ∧ n.totient = v) ↔
      ∃ m : ℕ, 0 < m ∧ m.totient = d ∧ n = b*m) :
    (ell d : ℝ) / d ≤ (ell v : ℝ) / v := by
…

Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.ell

theorem OAI.TotientAsymptotic.mul_totient_injective_of_full_fibers line 138

Source documentation

Complete inverse-fiber dilations give distinct totients for distinct multipliers.

theorem mul_totient_injective_of_full_fibers {d b c : ℕ} (hd : IsTotient d)
    (hb : 0 < b) (hc : 0 < c)
    (hbfull : ∀ n : ℕ, (0 < n ∧ n.totient = d*b.totient) ↔
      ∃ m : ℕ, 0 < m ∧ m.totient = d ∧ n = b*m)
    (hcfull : ∀ n : ℕ, (0 < n ∧ n.totient = d*c.totient) ↔
      ∃ m : ℕ, 0 < m ∧ m.totient = d ∧ n = c*m)
    (hvalue : d*b.totient = d*c.totient) : b = c := by
…

Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.m

theorem OAI.TotientAsymptotic.card_convenient_le_V line 151
theorem OAI.TotientAsymptotic.seeds_one_two_of_published_least_preimage line 177
Source documentation
The numerical least-preimage computation stated in the proof of Lemma 5.1 of Pollack--Pomerance--Treviño, Sets of monotonicity for Euler's totient function, Ramanujan Journal 30 (2013), p. 9 of the author manuscript, implies both seed cases of the weighted companion theorem.
```
theorem seeds_one_two_of_published_least_preimage
    (hseed : IsTotient (2^18 * 257))
    (hmin : ell (2^18 * 257) = 135268352) :
    (∃ d : ℕ, IsTotient d ∧ 1*d < ell d) ∧
    (∃ d : ℕ, IsTotient d ∧ 2*d < ell d) := by
…
```
Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell