aestronglyMeasurable_comp_snd_map_prodMk_iff

English

AEStronglyMeasurable (λx, f x. snd) under map ω ↦ (X ω, ω) is equivalent to AEStronglyMeasurable f μ for measurable X.

Русский

AEStronglyMeasurable(λx, f x. snd) под отображением ω ↦ (X ω, ω) эквивалентно AEStronglyMeasurable f μ для измеримой X.

LaTeX

$$$$ \\text{AEStronglyMeasurable}(λx, f x.2) (μ.map ω ↦ (X ω, ω)) \\iff \\text{AEStronglyMeasurable}(f, μ). $$$$

Lean4

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

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