condExp_ae_eq_integral_condExpKernel

English

If f is integrable, then ω ↦ || ∫ f(y) d condExpKernel μ m ω || is integrable.

Русский

Если f интегрируема, то ω ↦ ||∫ f(y) d condExpKernel μ m ω|| интегрируема.

LaTeX

$$$\\text{Integrable}(f,μ) \\Rightarrow \\text{Integrable}\\left(ω\\mapsto \\left\\|\\int y\\, f(y) \\; d condExpKernel(μ,m)(ω)\\right\\|\\right)$$$

Lean4

/-- The conditional expectation of `f` with respect to a σ-algebra `m` is almost everywhere equal to
the integral `∫ y, f y ∂(condExpKernel μ m ω)`. -/
theorem condExp_ae_eq_integral_condExpKernel [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F]
    (hm : m ≤ mΩ) (hf_int : Integrable f μ) : μ[f|m] =ᵐ[μ] fun ω => ∫ y, f y ∂condExpKernel μ m ω :=
  ((condExp_ae_eq_integral_condExpKernel' hf_int).symm.trans (by rw [inf_of_le_left hm])).symm

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