Theorems · Theorem · measure theory

MeasureTheory.condExp_smul

∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [CompleteSpace E] [inst_4 : NormedSpace 𝕜 E] (c : 𝕜)
  (f : α → E) (m : MeasurableSpace α), μ[c • f | m] =ᵐ[μ] c • μ[f | m]

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceCompleteSpaceNormedSpace