condExpL1_of_aestronglyMeasurable'

English

For f: α → F', condExpL1 hm μ (-f) = - condExpL1 hm μ f.

Русский

Для функции f: α → F' выполняется condExpL1 hm μ (-f) = - condExpL1 hm μ f.

LaTeX

$$$condExpL1 hm μ (-f) = - condExpL1 hm μ f$$$

Lean4

theorem condExpL1_of_aestronglyMeasurable' (hfm : AEStronglyMeasurable[m] f μ) (hfi : Integrable f μ) :
    condExpL1 hm μ f =ᵐ[μ] f := by
  rw [condExpL1_eq hfi]
  refine EventuallyEq.trans ?_ (Integrable.coeFn_toL1 hfi)
  rw [condExpL1CLM_of_aestronglyMeasurable']
  exact hfm.congr hfi.coeFn_toL1.symm

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