rnDeriv_map_aux — Mathlib

Lean4
theorem _root_.MeasurableEmbedding.rnDeriv_map_aux (hf : MeasurableEmbedding f) (hμν : μ ≪ ν) [SigmaFinite μ]
    [SigmaFinite ν] : (fun x ↦ (μ.map f).rnDeriv (ν.map f) (f x)) =ᵐ[ν] μ.rnDeriv ν :=
  by
  refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)
  · exact (Measure.measurable_rnDeriv _ _).comp hf.measurable
  · exact Measure.measurable_rnDeriv _ _
  rw [← hf.lintegral_map, Measure.setLIntegral_rnDeriv hμν]
  have hs_eq : s = f ⁻¹' (f '' s) := by rw [hf.injective.preimage_image]
  have : SigmaFinite (ν.map f) := hf.sigmaFinite_map
  rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν), hf.map_apply]
Похожие утверждения