Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.initial.smooth_of_multiple

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1177 to 1189

Source documentation

If √n < p < n/L and p ∣ m with 0 < m < n, then m is (n/L)-smooth.

Exact Lean statement

lemma Params.initial.smooth_of_multiple (P : Params) {p m : ℕ} (hp : p > Real.sqrt P.n)
    (hps : p < P.n / P.L) (hm : m < P.n) (hm0 : m ≠ 0) (hpm : p ∣ m) :
    m ∈ smoothNumbers (P.n / P.L)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.initial.smooth_of_multiple (P : Params) {p m : ℕ} (hp : p > Real.sqrt P.n)    (hps : p < P.n / P.L) (hm : m < P.n) (hm0 : m ≠ 0) (hpm : p ∣ m) :    m ∈ smoothNumbers (P.n / P.L) := by  contrapose! hps  refine le_of_not_gt fun h ↦ hps ?_  obtain ⟨q, hq, hqm, hqn⟩ : ∃ q, Prime q ∧ q ∣ m ∧ q ≥ P.n / P.L := by    simp_all [smoothNumbers]  have : p * q > P.n := by    rw [gt_iff_lt, Real.sqrt_lt] at hp <;> norm_cast at * <;> nlinarith  exact absurd (le_of_dvd (pos_of_ne_zero hm0) (Coprime.mul_dvd_of_dvd_of_dvd    (coprime_comm.mp <| hq.coprime_iff_not_dvd.mpr <| not_dvd_of_pos_of_lt      (pos_of_ne_zero <| by grind) <| by nlinarith [div_mul_le_self P.n P.L])        hpm hqm)) (by omega)