English
If g is strongly measurable, there exists a measurable h such that g = h ∘ f.
Русский
Если g сильно измерима, существует измеримая h такая, что g = h ∘ f.
LaTeX
$$$$ \exists h : Y \to Z, \; \text{StronglyMeasurable } h \wedge g = h \circ f. $$$$
Lean4
/-- If a function `g` is strongly measurable with respect to the pullback along some function `f`,
then there exists some strongly measurable function `h : Y → Z` such that `g = h ∘ f`. -/
theorem exists_eq_measurable_comp [Nonempty Z] [TopologicalSpace Z] [IsCompletelyMetrizableSpace Z]
(hg : StronglyMeasurable[mY.comap f] g) : ∃ h : Y → Z, StronglyMeasurable h ∧ g = h ∘ f :=
by
let mX : MeasurableSpace X := mY.comap f
induction g, hg using StronglyMeasurable.induction' with
| const z => exact ⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩
| @pcw g₁ g₂ s hg₁ hg₂ hs h₁ h₂ =>
obtain ⟨t, ht, rfl⟩ := hs
obtain ⟨h₁, mh₁, rfl⟩ := h₁
obtain ⟨h₂, mh₂, rfl⟩ := h₂
classical exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
| @lim g i hg hi h₁ h₂ =>
choose h mh hh using h₁
refine ⟨fun y ↦ _root_.limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
ext x
rw [Function.comp_apply, Tendsto.limUnder_eq]
simp_all
