condExpIndL1_add — Mathlib

English

Additivity of condExpIndL1Fin with measurable hs and hμs on sum x+y.

Русский

Аддитивность condExpIndL1Fin для hs и hμs на сумму x+y.

LaTeX

$$condExpIndL1Fin hm hs hμs (x+y) = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y$$

Lean4

theorem condExpIndL1_add (x y : G) : condExpIndL1 hm μ s (x + y) = condExpIndL1 hm μ s x + condExpIndL1 hm μ s y :=
  by
  by_cases hs : MeasurableSet s
  swap; · simp_rw [condExpIndL1_of_not_measurableSet hs]; rw [zero_add]
  by_cases hμs : μ s = ∞
  · simp_rw [condExpIndL1_of_measure_eq_top hμs]; rw [zero_add]
  · simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
    exact condExpIndL1Fin_add hs hμs x y

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