Theorems · Theorem · measure theory

norm_condExp_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2}
  {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → E),
  (fun x => ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x => ‖f x‖ | m]

In a Banach space E with a measure μ, then for any f : α → E, we have ‖𝔼[f | m]‖ ≤ᵐ[μ] 𝔼[‖f‖ | m].

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Cited by

2 results in Mathlib

Foundations

Depth 307 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace