dominatedFinMeasAdditive_condExpInd

English

Same as the disjoint union additivity, but stated as an applied equality for union.

Русский

То же самое про объединение по дизъюнкции, но в форме применимого равенства для объединения.

LaTeX

$$$ condExpInd\; G\; hm\; \mu\; (s \cup t)\; x = condExpInd\; G\; hm\; \mu\; s\; x + condExpInd\; G\; hm\; \mu\; t\; x,$$

Lean4

theorem dominatedFinMeasAdditive_condExpInd (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] :
    DominatedFinMeasAdditive μ (condExpInd G hm μ : Set α → G →L[ℝ] α →₁[μ] G) 1 :=
  ⟨fun _ _ => condExpInd_disjoint_union, fun _ _ _ => norm_condExpInd_le.trans (one_mul _).symm.le⟩

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