English
If s and t are measurable sets with finite measures and are disjoint, then the conditional expectation on their union equals the sum of the conditional expectations on each: condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x.
Русский
Если s и t измеримы и их меры конечны и множества дизъjointны, то condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x.
LaTeX
$$$ \text{If } s,t \text{ are measurable with finite measure and } s \cap t = \varnothing,\;
condExpIndL1\; hm\; \mu\; (s \cup t)\; x = condExpIndL1\; hm\; \mu s\; x + condExpIndL1\; hm\; \mu t\; x.$$$
Lean4
theorem condExpIndL1_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞)
(hst : Disjoint s t) (x : G) : condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x :=
by
have hμst : μ (s ∪ t) ≠ ∞ :=
((measure_union_le s t).trans_lt (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne
rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x,
condExpIndL1_of_measurableSet_of_measure_ne_top ht hμt x,
condExpIndL1_of_measurableSet_of_measure_ne_top (hs.union ht) hμst x]
exact condExpIndL1Fin_disjoint_union hs ht hμs hμt hst x
