Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.large_prime_sum_split

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2676 to 2687

Mathematical statement

Exact Lean statement

lemma large_prime_sum_split (n L : ℕ) (f : ℕ → ℝ) :
    ∑ p ∈ Finset.filter Nat.Prime (Finset.Icc (n / L) n), f p =
      (if (n / L).Prime then f (n / L) else 0) +
      ∑ p ∈ Finset.filter Nat.Prime (Finset.Icc (n / L + 1) n), f p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma large_prime_sum_split (n L : ℕ) (f : ℕ → ℝ) :    ∑ p ∈ Finset.filter Nat.Prime (Finset.Icc (n / L) n), f p =      (if (n / L).Prime then f (n / L) else 0) +      ∑ p ∈ Finset.filter Nat.Prime (Finset.Icc (n / L + 1) n), f p := by  classical  have hnot_mem : n / L ∉ Finset.filter Nat.Prime (Finset.Icc (n / L + 1) n) := by    simp  by_cases hprime : (n / L).Prime  · rw [large_range_split, Finset.filter_insert, if_pos hprime, Finset.sum_insert hnot_mem]    simp [hprime]  · rw [large_range_split, Finset.filter_insert, if_neg hprime]    simp [hprime]