Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.initial.sum_valuation_le

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1335 to 1353

Source documentation

The sum of valuations in the initial factorization is bounded by M times the sum of valuations in the interval. This is because the initial factorization is a subset of M copies of the interval.

Exact Lean statement

lemma Params.initial.sum_valuation_le (P : Params) (p : ℕ) :
    (initial P).sum (fun m ↦ m.factorization p) ≤
      P.M * ∑ m ∈ .Ico (P.n - P.n / P.M) P.n, m.factorization p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.initial.sum_valuation_le (P : Params) (p : ℕ) :    (initial P).sum (fun m ↦ m.factorization p) ≤      P.M * ∑ m ∈ .Ico (P.n - P.n / P.M) P.n, m.factorization p := by  have h_subset : P.initial.a ≤ Multiset.bind (replicate P.M (Finset.Ico (P.n - P.n / P.M) P.n))      (fun s ↦ s.val) := by    simp only [initial, le_iff_count]    intro a    by_cases a ∈ (P.n / P.L).smoothNumbers    · simp_all only [join, count_filter_of_pos]      simp only [sum_replicate, count_nsmul, count_bind, map_replicate]      rfl    · simp_all [join]  have h_sum_le : ∀ {s t : Multiset ℕ}, s ≤ t →      (s.map (fun m ↦ m.factorization p)).sum ≤ (t.map (fun m ↦ m.factorization p)).sum := by    intro s t hst    obtain ⟨u, rfl⟩ := Multiset.le_iff_exists_add.mp hst    simp  convert! h_sum_le h_subset using 1  simp [Multiset.bind]