English
The measure of the half-open interval Ico(a,b) equals ofReal(leftLim f(b) - leftLim f(a)).
Русский
Мера Ico(a,b) равна ofReal(leftLim f(b) - leftLim f(a)).
LaTeX
$$μ_f(Ico(a,b)) = \operatorname{ofReal}(leftLim f(b) - leftLim f(a))$$
Lean4
@[simp]
theorem measure_Ioo {a b : ℝ} : f.measure (Ioo a b) = ofReal (leftLim f b - f a) :=
by
rcases le_or_gt b a with (hab | hab)
· simp only [hab, measure_empty, Ioo_eq_empty, not_lt]
symm
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim_le hab]
· have A : Disjoint (Ioo a b) { b } := by simp
have D : f b - f a = f b - leftLim f b + (leftLim f b - f a) := by abel
have := f.measure_Ioc a b
simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton, measure_union A (measurableSet_singleton b),
Icc_self] at this
rw [D, ENNReal.ofReal_add, add_comm] at this
· simpa only [ENNReal.add_right_inj ENNReal.ofReal_ne_top]
· simp only [f.mono.leftLim_le le_rfl, sub_nonneg]
· simp only [f.mono.le_leftLim hab, sub_nonneg]