English
For any f, s, the outer measure of p.bindOnSupport f on s equals the sum ∑' a p(a) times the outer measure of (f a h) on s.
Русский
Для любой функции f и множества s внешняя мера p.bindOnSupport f на s равна сумме ∑' a p(a) ⋅ (f(a,h)).toOuterMeasure(s).
LaTeX
$$$$ (\\mathrm{bindOnSupport} f).\\mathrm{toOuterMeasure} (s) = \\sum' a \\, p(a) \\cdot (f(a,h)).\\mathrm{toOuterMeasure}(s) $$$$
Lean4
@[simp]
theorem toOuterMeasure_bindOnSupport_apply :
(p.bindOnSupport f).toOuterMeasure s = ∑' a, p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s :=
by
simp only [toOuterMeasure_apply]
classical
calc
(∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
tsum_congr fun b => by split_ifs with hbs <;> simp only [tsum_zero]
_ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 := ENNReal.tsum_comm
_ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
(tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
_ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero]
