condExpIndL1 — Mathlib

English

If μ[s] ≠ ∞, then condExpIndL1 hm μ s x equals condExpIndL1Fin hm hs hμs x.

Русский

Если μ[s] не бесконечна, condExpIndL1 hm μ s x совпадает с condExpIndL1Fin.

LaTeX

$$$condExpIndL1_of_measurableSet_of_measure_ne_top hm μ s x = condExpIndL1Fin hm hs hμs x$$$

Lean4

/-- Conditional expectation of the indicator of a set, as a function in L1. Its value for sets
which are not both measurable and of finite measure is not used: we set it to 0. -/
def condExpIndL1 {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) (s : Set α) [SigmaFinite (μ.trim hm)]
    (x : G) : α →₁[μ] G :=
  if hs : MeasurableSet s ∧ μ s ≠ ∞ then condExpIndL1Fin hm hs.1 hs.2 x else 0

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