docs#MeasureTheory.Measure.map_map

Stream: Is there code for X?

[Yaël Dillies]

Is there a version of docs#MeasureTheory.Measure.map_map that only requires ae-measurability somewhere?

[Yaël Dillies]

I'm not even sure whether it's true, but I would at least hope so.

[Yury G. Kudryashov]

docs#AEMeasurable.map_map_of_aemeasurable

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

Found by @loogle MeasureTheory.Measure.Map, AEMeasurable

[loogle]

:exclamation: unknown identifier 'MeasureTheory.Measure.Map'
Did you mean "MeasureTheory.Measure.Map", AEMeasurable?

[Yury G. Kudryashov]

Found by @loogle MeasureTheory.Measure.map, AEMeasurable

[loogle]

:search: MeasureTheory.Measure.tendsto_ae_map, MeasureTheory.Measure.map_of_not_aemeasurable, and 71 more

[Yury G. Kudryashov]

Let's try @loogle AEMeasurable, "map_map"

[Yury G. Kudryashov]

@loogle AEMeasurable, "map_map"

[loogle]

:search: AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map

[Kalle Kytölä]

I'm probably late to the party, but just in case, @Yaël Dillies:

import Mathlib

namespace MeasureTheory

lemma Measure.map_map_ae {α β γ : Type*} [m0 : MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : Measure α}
    {g : β → γ} {f : α → β} (hf : AEMeasurable f μ) (hg : AEMeasurable g (μ.map f)) :
    Measure.map g (Measure.map f μ) = Measure.map (g ∘ f) μ := by
  obtain ⟨F, F_mble, F_aeeq_f⟩ := hf
  obtain ⟨G, G_mble, G_aeeq_g⟩ := hg
  have map_f_eq := Measure.map_congr F_aeeq_f
  have map_g_eq := Measure.map_congr G_aeeq_g
  rw [map_f_eq] at map_g_eq ⊢
  rw [map_g_eq, Measure.map_map G_mble F_mble]
  apply Measure.map_congr
  have aux : μ.map f {b | g b ≠ G b} = 0 := G_aeeq_g
  rw [map_f_eq, map_apply₀ F_mble.aemeasurable] at aux
  filter_upwards [F_aeeq_f, show {a | g (F a) = G (F a)} ∈ ae μ from aux] with a hfa hgfa
  simp only [Function.comp_apply, ←hgfa, hfa]
  exact NullMeasurableSet.of_null aux

end MeasureTheory -- namespace

[Yaël Dillies]

Thanks! This seems to have the same assumptions as docs#AEMeasurable.map_map_of_aemeasurable.

[Kalle Kytölä]

I failed to read the Loogle output... :face_palm:

[Yury G. Kudryashov]

#8837