English
If f: ENNReal × ENNReal → β is measurable when the first coordinate is finite (via ofNNReal) and also measurable along (∞, r) and (r, ∞), then f is measurable on ENNReal × ENNReal.
Русский
Если f: ENNReal × ENNReal → β измерима при конечном первом аргументе (через ofNNReal) и измерима по линиям (∞, r) и (r, ∞), то f измерима на ENNReal × ENNReal.
LaTeX
$$$\text{Measurable}(f) \text{ if } (f \text{ measurable on } (\text{finite}, \text{finite})) \land (f(∞, r) \text{ measurable}) \land (f(r, ∞) \text{ measurable})$$$
Lean4
theorem measurable_of_measurable_nnreal_nnreal {_ : MeasurableSpace β} {f : ℝ≥0∞ × ℝ≥0∞ → β}
(h₁ : Measurable fun p : ℝ≥0 × ℝ≥0 => f (p.1, p.2)) (h₂ : Measurable fun r : ℝ≥0 => f (∞, r))
(h₃ : Measurable fun r : ℝ≥0 => f (r, ∞)) : Measurable f :=
measurable_of_measurable_nnreal_prod
(measurable_swap_iff.1 <| measurable_of_measurable_nnreal_prod (h₁.comp measurable_swap) h₃)
(measurable_of_measurable_nnreal h₂)
