Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.exists_submultiset_prod_between

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:357 to 368

Source documentation

Given a multiset of numbers ≤ L with product > n, there exists a sub-multiset whose product m satisfies n / L < m ≤ n.

Exact Lean statement

lemma exists_submultiset_prod_between {n L : ℕ} (D : Multiset ℕ) (hL : 0 < L) (hn : 1 ≤ n)
    (hD_le : ∀ p ∈ D, p ≤ L) (hD_prod : D.prod > n) :
    ∃ M ≤ D, n < M.prod * L ∧ M.prod ≤ n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma exists_submultiset_prod_between {n L : ℕ} (D : Multiset ℕ) (hL : 0 < L) (hn : 1 ≤ n)    (hD_le : ∀ p ∈ D, p ≤ L) (hD_prod : D.prod > n) :    ∃ M ≤ D, n < M.prod * L ∧ M.prod ≤ n := by  induction D using Multiset.induction with  | empty => aesop  | cons p D ih =>    by_cases hD_prod' : D.prod > n    · obtain ⟨M, hM_le, hM⟩ := ih (fun q hq ↦ hD_le q (mem_cons_of_mem hq)) hD_prod'      exact ⟨M, hM_le.trans (le_cons_self _ _), hM⟩    · refine ⟨D, le_cons_self _ _, ?_, by omega⟩      simp only [Multiset.prod_cons, gt_iff_lt] at hD_prod      nlinarith [hD_le p (mem_cons_self p D)]