condExpIndL1Fin_disjoint_union — Mathlib

English

Generalized scalar action preserves IndL1: (c • x) maps to c times IndL1 of x.

Русский

Обобщённая операция умножения на скаляр сохраняет IndL1.

LaTeX

$$$condExpIndL1 hm μ s (c \cdot x) = c \cdot condExpIndL1 hm μ s x$$$

Lean4

theorem condExpIndL1Fin_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞)
    (hst : Disjoint s t) (x : G) :
    condExpIndL1Fin hm (hs.union ht)
        ((measure_union_le s t).trans_lt (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne x =
      condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x :=
  by
  ext1
  grw [Lp.coeFn_add, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndL1Fin_ae_eq_condExpIndSMul]
  rw [condExpIndSMul]
  rw [indicatorConstLp_disjoint_union hs ht hμs hμt hst (1 : ℝ)]
  rw [map_add]
  push_cast
  rw [map_add]
  grw [Lp.coeFn_add]
  rfl

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