English
Similarly, the second component is ae-strongly measurable whenever the pair is identically distributed.
Русский
Аналогично, вторая компонента ae-сложно измерима, если пара идентично распределена.
LaTeX
$$$[TopologicalSpace γ] [PseudoMetrizableSpace γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable g ν$$$
Lean4
/-- If `f` and `g` are identically distributed and `f` is a.e. strongly measurable, so is `g`. -/
theorem aestronglyMeasurable_snd [TopologicalSpace γ] [PseudoMetrizableSpace γ] [BorelSpace γ]
(h : IdentDistrib f g μ ν) (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable g ν :=
by
refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨h.aemeasurable_snd, ?_⟩
rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
refine ⟨closure t, t_sep.closure, ?_⟩
apply h.ae_mem_snd isClosed_closure.measurableSet
filter_upwards [ht] with x hx using subset_closure hx
