English
Let ι be a topological space, α a measurable space, and β a topological space. Suppose u: ι → α → β satisfies that for every x ∈ α the map i ↦ u(i, x) is continuous, and that for every i ∈ ι the function u(i, ·) is strongly measurable. Then the uncurried function uncurry(u): α × ι → β, defined by uncurry(u)(x, i) = u(i, x), is strongly measurable.
Русский
Пусть ι — топологическое пространство, α — измеримое пространство, β — топологическое пространство. Пусть u: ι → α → β удовлетворяет условию: для каждого x ∈ α отображение i ↦ u(i, x) непрерывно на ι, и для каждого i ∈ ι функция u(i, ·) является сильно измеримой. Тогда развернутая функция uncurry(u): α × ι → β, заданная uncurry(u)(x, i) = u(i, x), является сильно измеримой.
LaTeX
$$$\\forall x, (\\lambda i. u(i,x)) \\text{ непрерывна} \\,\\wedge\\, \\forall i, u(i) \\text{ сильно измерима} \\Rightarrow \\operatorname{uncurry}u \\in S\\M(α\\times ι,β)$$$
Lean4
theorem stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable {α β ι : Type*} [TopologicalSpace ι]
[MetrizableSpace ι] [MeasurableSpace ι] [SecondCountableTopology ι] [OpensMeasurableSpace ι] [TopologicalSpace β]
[PseudoMetrizableSpace β] [MeasurableSpace α] {u : ι → α → β} (hu_cont : ∀ x, Continuous fun i => u i x)
(h : ∀ i, StronglyMeasurable (u i)) : StronglyMeasurable (Function.uncurry u) :=
by
borelize β
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 stronglyMeasurable_of_tendsto _ (fun n => ?_) h_tendsto
have h_str_meas : StronglyMeasurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd :=
by
refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
· 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]
exact measurable_from_prod_countable_left fun j => (h j).measurable
· have : IsSeparable (⋃ i : (t_sf n).range, range (u i)) := .iUnion fun i => (h i).isSeparable_range
apply this.mono
rintro _ ⟨⟨i, x⟩, rfl⟩
simp only [mem_iUnion, mem_range]
exact ⟨i, x, rfl⟩
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_str_meas.comp_measurable (Measurable.prodMk ?_ measurable_snd)
exact ((t_sf n).measurable.comp measurable_fst).subtype_mk
