Source indexedtheorem · leanprover/lean4:v4.32.0

BrunTitchmarsh.primesBetween_le_siftedSum_add

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:79 to 97

Mathematical statement

Exact Lean statement

theorem primesBetween_le_siftedSum_add :
    primesBetween x (x+y) ≤
      siftedSum (s := toBoundingSieve (self := primeInterSieve x y z hz)) + z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem primesBetween_le_siftedSum_add :    primesBetween x (x+y) ≤      siftedSum (s := toBoundingSieve (self := primeInterSieve x y z hz)) + z := by  classical  trans ↑((Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter      (fun d ↦ ∀ p : ℕ, p.Prime → p ≤ z → ¬p ∣ d) ∪      (Finset.Icc 1 (Nat.floor z))).card  · rw [primesBetween]    exact_mod_cast Finset.card_le_card (primesBetween_subset _ _ _)  trans ↑((Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter      (fun d ↦ ∀ p : ℕ, p.Prime → p ≤ z → ¬p ∣ d)).card +      ↑(Finset.Icc 1 (Nat.floor z)).card  · exact_mod_cast Finset.card_union_le _ _  rw [siftedSum_eq_card]  gcongr  rw [Nat.card_Icc]  simp only [add_tsub_cancel_right]  apply Nat.floor_le  linarith