integrable_toReal_condExpKernel — Mathlib

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

theorem integrable_toReal_condExpKernel {s : Set Ω} (hs : MeasurableSet s) :
    Integrable (fun ω => (condExpKernel μ m ω).real s) μ :=
  by
  nontriviality Ω
  rw [condExpKernel_eq]
  exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs

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