simpleFunc_add — Mathlib

English

Let E be a topological vector space where addition is a measurable operation. If g is a measurable function α → E and f is a simple function α → E, then the sum f + g is measurable. In particular, pointwise addition preserves measurability when one summand is a simple function.

Русский

Пусть E — топологическое векторное пространство, в котором сложение измеримо. Пусть g: α → E измеримо, а f — простая функция α → E. Тогда сумма f + g измерима. В частности, сложение по одной функции сохраняет измеримость, если другая часть — простая функция.

LaTeX

$$$\text{Measurable}((f : \alpha \to E) + g)$$$

Lean4

/-- In a topological vector space, the addition of a simple function and a measurable function is
measurable. -/
theorem _root_.Measurable.simpleFunc_add {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E]
    [MeasurableAdd E] {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : Measurable ((f : α → E) + g) := by
  classical
    induction f using SimpleFunc.induction with
  | @const c s
    hs =>
    simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero]
    rw [← s.piecewise_same g, ← piecewise_add]
    exact Measurable.piecewise hs (hg.const_add _) (hg.const_add _)
  | @add f f' hff' hf
    hf' =>
    have : (↑(f + f') + g) = (Function.support f).piecewise ((f : α → E) + g) (f' + g) :=
      by
      ext x
      by_cases hx : x ∈ Function.support f
      ·
        simpa only [coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not, Set.piecewise_eq_of_mem _ _ _ hx,
          _root_.add_left_inj, add_eq_left] using Set.disjoint_left.1 hff' hx
      ·
        simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
          Set.piecewise_eq_of_notMem _ _ _ hx, _root_.add_left_inj, add_eq_right] using hx
    rw [this]
    exact Measurable.piecewise f.measurableSet_support hf hf'

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