blocks_partial_sum — Mathlib

English

Let B_i be the i-th partial sum of the blocks: B_i = sum_{t=1}^i b_t. Then the sum of the first i blocks equals B_i.

Русский

Пусть B_i — i-я частичная сумма блоков: B_i = sum_{t=1}^i b_t. Тогда сумма первых i блоков равна B_i.

LaTeX

$$$B_i=\\sum_{t=1}^i b_t\\quad(0\\le i\\le l),$$$

Lean4

theorem blocks_partial_sum {i : ℕ} (h : i < c.boundaries.card) : (c.blocks.take i).sum = c.boundary ⟨i, h⟩ := by
  induction i with
  | zero => simp
  | succ i
    IH =>
    have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]
    have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length])
    rw [sum_take_succ _ _ A, IH B]
    simp [blocks, blocksFun]

Похожие утверждения