Theorems · Theorem · measure theory

MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound

∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G)
  [CompleteSpace E],
  m ≤ mΩ →
    ∀ [MeasureTheory.IsFiniteMeasure μ] {f : Ω → F} {g : Ω → E},
      MeasureTheory.AEStronglyMeasurable f μ →
        MeasureTheory.Integrable g μ →
          ∀ (c : ℝ), (∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceCompleteSpaceCompleteSpaceMeasureTheory.IsFiniteMeasure