measurable_of_measurable_nnreal_prod

English

If H1 makes the map (p1,p2) ↦ f(p1,p2) measurable on ℝ≥0 × β and H2 makes x ↦ f(∞,x) measurable, then f is measurable on ENNReal × β.

Русский

Пусть H1 обеспечивает измеримость функции (p1,p2) ↦ f(p1,p2) на ℝ≥0 × β и H2 — измеримость x ↦ f(∞,x); тогда f измерима на ENNReal × β.

LaTeX

$$$(\exists \text{Measurable}(p\mapsto f(p_1,p_2))) \land (\text{Measurable}(x \mapsto f(\infty,x))) \Rightarrow \text{Measurable } f$$$

Lean4

theorem measurable_of_measurable_nnreal_prod {_ : MeasurableSpace β} {_ : MeasurableSpace γ} {f : ℝ≥0∞ × β → γ}
    (H₁ : Measurable fun p : ℝ≥0 × β => f (p.1, p.2)) (H₂ : Measurable fun x => f (∞, x)) : Measurable f :=
  let e : ℝ≥0∞ × β ≃ᵐ (ℝ≥0 × β) ⊕ (Unit × β) :=
    (ennrealEquivSum.prodCongr (MeasurableEquiv.refl β)).trans (MeasurableEquiv.sumProdDistrib _ _ _)
  e.symm.measurable_comp_iff.1 <| measurable_fun_sum H₁ (H₂.comp measurable_id.snd)

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