[Merged by Bors] - feat(measure_theory/measure/measure_space): volume_preimage_coe

[alexjbest]

This is another lemma needed by #2819, I'm not sure exactly of its provenance, but it looks like @YaelDillies extracted it as a lemma at least, if not wrote the original version completely.

Co-authored-by: Yaël Dillies yael.dillies@gmail.com

---

[fpvandoorn]

This is not the right generality. We want to prove lemmas first for a variable measure μ.
Note that the volume on a subtype is defined as measure.comap subtype.val volume, so the lemma for variable measures can mention measure.comap subtype.val μ, but then you can probably also generalize subtype.val to get a general lemma about measure.comap.

[YaelDillies]

@fpvandoorn, are you sure? The current proof crucially relies on measurable_set.null_measurable_set_subtype_coe and subtype.range_coe, which don't have general comap analogs. Here's the best I could do

@[simp] lemma comap_preimage [measurable_space β] {μ : measure α} {s : set α} {f : β → α}
  (hf : injective f) (hf' : measurable f)
  (h : ∀ t, measurable_set t → null_measurable_set (f '' t) μ) (hs : measurable_set s) :
  μ.comap f (f ⁻¹' s) = μ (s ∩ range f) :=
by rw [comap_apply₀ _ _ hf h (hf' hs).null_measurable_set, image_preimage_eq_inter_range]

@[simp] lemma volume_preimage_coe {s t : set α} (hs : null_measurable_set s)
  (ht : measurable_set t) : volume ((coe : s → α) ⁻¹' t) = volume (t ∩ s) :=
by rw [volume_set_coe_def, comap_preimage subtype.coe_injective measurable_subtype_coe
  (by rwa subtype.range_coe) (λ h, measurable_set.null_measurable_set_subtype_coe hs) ht,
  subtype.range_coe]

The assumptions look very unnatural and the actual lemma is not even shorter 😢

[urkud]

In comap_preimage, you can get hfμ from h unit. This assumption holds, e.g., for any https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space.html#measurable_embedding

[fpvandoorn]

Thanks for adding the other versions!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests