condExpIndL1Fin_add — Mathlib

English

If s is not measurable, condExpIndL1 hm μ s x equals 0.

Русский

Если множество не измеримо, condExpIndL1 hm μ s x равно 0.

LaTeX

$$$condExpIndL1_of_not_measurableSet hm μ s x = 0$$$

Lean4

theorem condExpIndL1Fin_add (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x y : G) :
    condExpIndL1Fin hm hs hμs (x + y) = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y :=
  by
  ext1
  unfold condExpIndL1Fin Integrable.toL1
  grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add, Lp.coeFn_add]

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