English
For a homeomorphism e between X and Y, locally integrable f on Y with respect to map μ is equivalent to locally integrable f ∘ e on X with respect to μ.
Русский
Для гомеморфа e между X и Y локально интегрируемость f на Y по карте μ эквивалентна локальной интегрируемости f ∘ e на X по μ.
LaTeX
$$$\\operatorname{LocallyIntegrable} f (\\operatorname{Measure.map} e \\mu) \\iff \\operatorname{LocallyIntegrable}(f \\circ e) \\mu$$$
Lean4
theorem locallyIntegrable_map_homeomorph [BorelSpace X] [BorelSpace Y] (e : X ≃ₜ Y) {f : Y → ε''} {μ : Measure X} :
LocallyIntegrable f (Measure.map e μ) ↔ LocallyIntegrable (f ∘ e) μ :=
by
refine ⟨fun h x => ?_, fun h x => ?_⟩
· rcases h (e x) with ⟨U, hU, h'U⟩
refine ⟨e ⁻¹' U, e.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
exact (integrableOn_map_equiv e.toMeasurableEquiv).1 h'U
· rcases h (e.symm x) with ⟨U, hU, h'U⟩
refine ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
apply (integrableOn_map_equiv e.toMeasurableEquiv).2
simp only [Homeomorph.toMeasurableEquiv_coe]
convert h'U
ext x
simp only [mem_preimage, Homeomorph.symm_apply_apply]
