condExpIndL1Fin — Mathlib

English

Generalized scalar action (possibly complex) preserves CondExpIndL1Fin: (c • x) maps to c times the CondExpIndL1Fin of x.

Русский

Обобщенная скалярная операция сохраняет CondExpIndL1Fin: (c • x) -> c ⋅ CondExpIndL1Fin x.

LaTeX

$$$condExpIndL1Fin hm hs hμs (c \cdot x) = c \cdot condExpIndL1Fin hm hs hμs x$$$

Lean4

/-- Conditional expectation of the indicator of a measurable set with finite measure,
as a function in L1. -/
def condExpIndL1Fin (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
    α →₁[μ] G :=
  (integrable_condExpIndSMul hm hs hμs x).toL1 _

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