seq_apply — Mathlib

English

The value of the sequence construction at b is given by a double sum over f and a, with a Booleans indicating b equals f(a).

Русский

Значениеseq(q,p) в точке b выражается двойной суммой по f и a с индикаторной характеристикой b=f(a).

LaTeX

$$$ (seq q p) b = \sum' (f : α → β) (a : α), if b = f a then q f * p a else 0 $$$

Lean4

@[simp]
theorem seq_apply : (seq q p) b = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0 :=
  by
  simp only [seq, mul_boole, bind_apply, pure_apply]
  refine tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => ?_)
  simpa only [mul_zero] using mul_ite (b = f a) (q f) (p a) 0

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