condExpL1CLM_of_aestronglyMeasurable'

English

If f is an L1-integrable function represented as an element of lpMeas and is AEStronglyMeasurable with respect to m, then condExpL1CLM applied to f equals f.

Русский

Если f интегрируема в L1 и является AEStronglyMeasurable относительно m, то condExpL1CLM применённый к f равен f.

LaTeX

$$$condExpL1CLM F' hm μ f = f$$$

Lean4

theorem condExpL1CLM_of_aestronglyMeasurable' (f : α →₁[μ] F') (hfm : AEStronglyMeasurable[m] f μ) :
    condExpL1CLM F' hm μ f = f :=
  condExpL1CLM_lpMeas (⟨f, hfm⟩ : lpMeas F' ℝ m 1 μ)

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