Source indexedtheorem · leanprover/lean4:v4.32.0

hardy_sigma_delayed_eq

PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:68 to 78

Mathematical statement

Exact Lean statement

theorem hardy_sigma_delayed_eq (u : ℕ → ℝ) (n k : ℕ) (hk : k ≠ 0) :
    hardy_sigma_delayed u n k =
    ((n + k + 1 : ℝ) / k) * hardy_sigma u (n + k) - ((n + 1 : ℝ) / k) * hardy_sigma u n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem hardy_sigma_delayed_eq (u : ℕ → ℝ) (n k : ℕ) (hk : k ≠ 0) :    hardy_sigma_delayed u n k =    ((n + k + 1 : ℝ) / k) * hardy_sigma u (n + k) - ((n + 1 : ℝ) / k) * hardy_sigma u n := by  field_simp;  unfold hardy_sigma_delayed hardy_sigma;  rw [ div_mul_cancel₀ _ ( by positivity ), mul_div ];  rw [ eq_sub_iff_add_eq, eq_div_iff ] <;> norm_cast ; norm_num;  rw [ mul_comm, ← Finset.sum_range_add_sum_Ico _ ( by linarith : n + 1 ≤ n + k + 1 ) ];  field_simp;  rw [add_comm, Nat.Ico_succ_right ];  rw [ Nat.Icc_succ_left ]