Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.rough_valuation_le_log

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1798 to 1807

Source documentation

For m ∈ rough_set and p ≤ L, vₚ(m) ≤ logₚ L.

Exact Lean statement

lemma Params.rough_valuation_le_log (P : Params) (m : ℕ) (hm : m ∈ rough_set P) (p : ℕ)
    (hp : p ≤ P.L) (hp_prime : p.Prime) : m.factorization p ≤ Nat.log p P.L

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.rough_valuation_le_log (P : Params) (m : ℕ) (hm : m ∈ rough_set P) (p : ℕ)    (hp : p ≤ P.L) (hp_prime : p.Prime) : m.factorization p ≤ Nat.log p P.L := by  have hk_le_L : rough_k P m ≤ P.L := (rough_qk_prop P m hm).2.2.1  have h_val_k_le_log_p_L : (rough_k P m).factorization p ≤ Nat.log p P.L := by    by_cases h : rough_k P m = 0    · simp_all    · exact le_log_of_pow_le hp_prime.one_lt <|        le_trans (le_of_dvd (pos_of_ne_zero h) (ordProj_dvd ..)) hk_le_L  convert h_val_k_le_log_p_L using 1  exact rough_valuation_eq_k_valuation P m hm p hp