Source indexedlemma · leanprover/lean4:v4.32.0

RS.IPart.sum_telescope_block

PrimeNumberTheoremAnd.Unused.MyMV_A3a · PrimeNumberTheoremAnd/Unused/MyMV_A3a.lean:417 to 423

Mathematical statement

Exact Lean statement

lemma sum_telescope_block {a b : ℝ} (g : ℝ → ℝ) (R : IPartition a b) (u v : Fin (R.n + 1)) (huv : u ≤ v) :
    ∑ j ∈ Finset.Ico u.val v.val, term g R j = g (R.x v) - g (R.x u)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_telescope_block {a b : ℝ} (g : ℝ → ℝ) (R : IPartition a b) (u v : Fin (R.n + 1)) (huv : u ≤ v) :    ∑ j ∈ Finset.Ico u.val v.val, term g R j = g (R.x v) - g (R.x u) := by      unfold term;      induction' v using Fin.inductionOn with v ih ; aesop;      cases huv.eq_or_lt <;> simp_all +decide [ Fin.lt_iff_val_lt_val, Nat.lt_succ_iff ];      rw [ Finset.sum_Ico_succ_top ( by linarith ), ih ( Nat.le_trans ( Nat.le_refl _ ) ‹_› ) ];      simp +decide [ Fin.add_def, Nat.mod_eq_of_lt ] ; ring!