Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
wants to merge 2 commits into from
Closed

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

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a4332c1
feat(measure_theory/measure/measure_space): add volume_preimage_coe
alexjbest Oct 17, 2022
ed8e367
measurable_embedding version
YaelDillies Nov 6, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
21 changes: 19 additions & 2 deletions src/measure_theory/measure/measure_space.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1120,6 +1120,12 @@ begin
exact ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm,
end

lemma comap_preimage {β} [measurable_space α] {mβ : measurable_space β} (f : α → β) (μ : measure β)
{s : set β} (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]

section subtype

/-! ### Subtype of a measure space -/
Expand Down Expand Up @@ -3311,6 +3317,11 @@ lemma restrict_map (μ : measure α) (s : set β) :
(μ.map f).restrict s = (μ.restrict $ f ⁻¹' s).map f :=
measure.ext $ λ t ht, by simp [hf.map_apply, ht, hf.measurable ht]

protected lemma comap_preimage (μ : measure β) {s : set β} (hs : measurable_set s) :
μ.comap f (f ⁻¹' s) = μ (s ∩ range f) :=
comap_preimage _ _ hf.injective hf.measurable
(λ t ht, (hf.measurable_set_image' ht).null_measurable_set) hs

end measurable_embedding

section subtype
Expand All @@ -3329,7 +3340,7 @@ lemma ae_restrict_iff_subtype {m0 : measurable_space α} {μ : measure α} {s :
(∀ᵐ x ∂(μ.restrict s), p x) ↔ ∀ᵐ x ∂(comap (coe : s → α) μ), p ↑x :=
by rw [← map_comap_subtype_coe hs, (measurable_embedding.subtype_coe hs).ae_map_iff]

variables [measure_space α]
variables [measure_space α] {s t : set α}

/-!
### Volume on `s : set α`
Expand All @@ -3341,14 +3352,20 @@ instance _root_.set_coe.measure_space (s : set α) : measure_space s :=
lemma volume_set_coe_def (s : set α) : (volume : measure s) = comap (coe : s → α) volume := rfl

lemma measurable_set.map_coe_volume {s : set α} (hs : measurable_set s) :
volume.map (coe : s → α)= restrict volume s :=
volume.map (coe : s → α) = restrict volume s :=
by rw [volume_set_coe_def, (measurable_embedding.subtype_coe hs).map_comap volume,
subtype.range_coe]

lemma volume_image_subtype_coe {s : set α} (hs : measurable_set s) (t : set s) :
volume (coe '' t : set α) = volume t :=
(comap_subtype_coe_apply hs volume t).symm

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

end subtype

namespace measurable_equiv
Expand Down