integral_comp

Stream: mathlib4

[Lua Viana Reis]

Is this lemma missing? I expected this to be the one called docs#MeasurePreserving.integral_comp (the current version assumes MeasurableEmbedding instead).

import Mathlib.MeasureTheory.Integral.Bochner.Basic

open MeasureTheory

variable [NormedDivisionRing 𝕜]
  {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {_ : MeasureSpace α}

theorem MeasurePreserving.integral_comp_of_aestronglyMeasurable {β} {_ : MeasurableSpace β}
    {f : α → β} {ν} (h₁ : MeasurePreserving f μ ν) {g : β → G} (hg : AEStronglyMeasurable g ν) :
    ∫ x, g (f x) ∂μ = ∫ y, g y ∂ν := by
  rw [←integral_map h₁.aemeasurable (h₁.map_eq ▸ hg), h₁.map_eq]

[David Ledvinka]

Seems like its missing. Your version is the same as the HasLaw version docs#ProbabilityTheory.HasLaw.integral_comp (where HasLaw is the same thing as MeasurePreserving but aemeasurable instead of measurable and the parameters flipped)

[Lua Viana Reis]

Interesting. I wonder why there are two versions instead of a single one with aemeasurable?