integrable_comp_snd_map_prodMk_iff

English

For X: Ω → β and μ a measure on Ω, integrability of f under μ is equivalent to integrability of ω ↦ f(ω) under μ.map ω ↦ (X ω, ω).

Русский

Для X: Ω → β и μ мера на Ω интегрируемость f по μ эквивалентна интегрируемости ω ↦ f(ω) по μ.map ω ↦ (X ω, ω).

LaTeX

$$$$ \\text{Integrable}(f, μ) \\iff \\text{Integrable}(λω, f(ω)) (μ.map ω \\mapsto (X ω, ω)). $$$$

Lean4

theorem integrable_comp_snd_map_prodMk_iff {Ω} {_ : MeasurableSpace Ω} {X : Ω → β} {μ : Measure Ω} (hX : Measurable X)
    {f : Ω → F} : Integrable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω)) ↔ Integrable f μ :=
  ⟨fun h => h.comp_measurable (hX.prodMk measurable_id), fun h => h.comp_snd_map_prodMk X⟩

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