condExpInd_disjoint_union — Mathlib

English

The norm of condExpInd applied to x is bounded by μ.real(s) times the norm of x.

Русский

Норма condExpInd x не превосходит μ.real(s)·∥x∥.

LaTeX

$$$ \| condExpInd\; G\; hm\; \mu\; s\; x \| \leq μ.real\; s \cdot \|x\|,$$$

Lean4

theorem condExpInd_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞)
    (hst : Disjoint s t) :
    (condExpInd G hm μ (s ∪ t) : G →L[ℝ] α →₁[μ] G) = condExpInd G hm μ s + condExpInd G hm μ t := by ext1 x; push_cast;
  exact condExpInd_disjoint_union_apply hs ht hμs hμt hst x

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