English
If g is an embedding, then AEStronglyMeasurable (g ∘ f) μ is equivalent to AEStronglyMeasurable f μ.
Русский
Если g — вложение, то AEStronglyMeasurable (g ∘ f) по μ эквивалентно AEStronglyMeasurable f по μ.
LaTeX
$$$IsEmbedding(g) \Rightarrow (AEStronglyMeasurable(g \circ f) \mu \iff AEStronglyMeasurable(f) \mu)$$$
Lean4
theorem _root_.Topology.IsEmbedding.aestronglyMeasurable_comp_iff [PseudoMetrizableSpace β] [PseudoMetrizableSpace γ]
{g : β → γ} {f : α → β} (hg : IsEmbedding g) :
AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ :=
by
letI := pseudoMetrizableSpacePseudoMetric γ
borelize β γ
refine
⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩, fun H =>
hg.continuous.comp_aestronglyMeasurable H⟩
· let G : β → range g := rangeFactorization g
have hG : IsClosedEmbedding G :=
{ hg.codRestrict _ _ with isClosed_range := by rw [rangeFactorization_surjective.range_eq]; exact isClosed_univ }
have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable
exact hG.measurableEmbedding.aemeasurable_comp_iff.1 this
· rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩
exact ⟨g ⁻¹' t, hg.isSeparable_preimage ht, h't⟩
