English
Under mild conditions, the uncurry of a family of measurable maps is measurable.
Русский
При умеренных условиях развёртка семейства отображений в единое отображение измерима.
LaTeX
$$$\text{Measurable}(\text{uncurry } u)$$$
Lean4
theorem measurable_uncurry_of_continuous_of_measurable {α β ι : Type*} [TopologicalSpace ι] [MetrizableSpace ι]
[MeasurableSpace ι] [SecondCountableTopology ι] [OpensMeasurableSpace ι] {mβ : MeasurableSpace β}
[TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β] {m : MeasurableSpace α} {u : ι → α → β}
(hu_cont : ∀ x, Continuous fun i => u i x) (h : ∀ i, Measurable (u i)) : Measurable (Function.uncurry u) :=
by
obtain ⟨t_sf, ht_sf⟩ : ∃ t : ℕ → SimpleFunc ι ι, ∀ j x, Tendsto (fun n => u (t n j) x) atTop (𝓝 <| u j x) :=
by
have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
refine ⟨h_str_meas.approx, fun j x => ?_⟩
exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)
let U (n : ℕ) (p : ι × α) := u (t_sf n p.fst) p.snd
have h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd) :=
by
rw [tendsto_pi_nhds]
exact fun p => ht_sf p.fst p.snd
refine measurable_of_tendsto_metrizable (fun n => ?_) h_tendsto
have h_meas : Measurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd :=
by
have :
(fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
(fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
rfl
rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]
exact measurable_from_prod_countable_left fun j => h j
have :
(fun p : ι × α => u (t_sf n p.fst) p.snd) =
(fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
(⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
rfl
simp_rw [U, this]
refine h_meas.comp (Measurable.prodMk ?_ measurable_snd)
exact ((t_sf n).measurable.comp measurable_fst).subtype_mk
