measure_add — Mathlib

English

The measure is additive with respect to pointwise addition of Stieltjes functions: (f+g).measure = f.measure + g.measure.

Русский

Мера аддитивна по точечному сложению функций Стиллтьеса: (f+g).measure = f.measure + g.measure.

LaTeX

$$$(f+g)\\\\mathrm{measure} = f\\\\mathrm{measure} + g\\\\mathrm{measure}$$$

Lean4

@[simp]
theorem measure_add (f g : StieltjesFunction) : (f + g).measure = f.measure + g.measure :=
  by
  refine Measure.ext_of_Ioc _ _ (fun a b h ↦ ?_)
  simp only [measure_Ioc, add_apply, Measure.coe_add, Pi.add_apply]
  rw [← ENNReal.ofReal_add (sub_nonneg_of_le (f.mono h.le)) (sub_nonneg_of_le (g.mono h.le))]
  ring_nf

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