From 95413e23e3d29b45c701fcd31f2dbadaf1b79cba Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 6 May 2022 09:15:39 +0000 Subject: [PATCH] feat(measure_theory/group/*): various lemmas about invariant measures (#13539) * Make the `measurable_equiv` argument to `measure_preserving.symm` explicit. This argument is cannot always be deduced from the other explicit arguments (which can be seen form the changes in `src/measure_theory/constructions/pi.lean`). * From the sphere eversion project * Required for convolutions --- src/analysis/complex/cauchy_integral.lean | 2 +- src/dynamics/ergodic/measure_preserving.lean | 2 +- src/measure_theory/constructions/pi.lean | 6 +- src/measure_theory/constructions/prod.lean | 42 +++++- .../function/strongly_measurable.lean | 9 +- src/measure_theory/group/arithmetic.lean | 22 ++- .../group/fundamental_domain.lean | 4 +- src/measure_theory/group/integration.lean | 48 +++++- .../group/measurable_equiv.lean | 14 ++ src/measure_theory/group/measure.lean | 65 ++++++-- src/measure_theory/group/prod.lean | 141 ++++++++++++------ .../integral/divergence_theorem.lean | 6 +- .../integral/torus_integral.lean | 4 +- .../measure/complex_lebesgue.lean | 2 +- src/measure_theory/measure/lebesgue.lean | 2 +- src/measure_theory/measure/measure_space.lean | 7 + 16 files changed, 293 insertions(+), 83 deletions(-) diff --git a/src/analysis/complex/cauchy_integral.lean b/src/analysis/complex/cauchy_integral.lean index 63f73b5416ef0..5263bbb4a1ec8 100644 --- a/src/analysis/complex/cauchy_integral.lean +++ b/src/analysis/complex/cauchy_integral.lean @@ -189,7 +189,7 @@ begin refine (integral2_divergence_prod_of_has_fderiv_within_at_off_countable (λ p, -(I • F p)) F (λ p, - (I • F' p)) F' z.re w.im w.re z.im t (hs.preimage e.injective) (htc.const_smul _).neg htc (λ p hp, ((htd p hp).const_smul I).neg) htd _).symm, - rw [← volume_preserving_equiv_real_prod.symm.integrable_on_comp_preimage + rw [← (volume_preserving_equiv_real_prod.symm _).integrable_on_comp_preimage (measurable_equiv.measurable_embedding _)] at Hi, simpa only [hF'] using Hi.neg end diff --git a/src/dynamics/ergodic/measure_preserving.lean b/src/dynamics/ergodic/measure_preserving.lean index 12013b65c9d3a..305c3f171284b 100644 --- a/src/dynamics/ergodic/measure_preserving.lean +++ b/src/dynamics/ergodic/measure_preserving.lean @@ -56,7 +56,7 @@ protected lemma ae_measurable {f : α → β} (hf : measure_preserving f μa μb ae_measurable f μa := hf.1.ae_measurable -lemma symm {e : α ≃ᵐ β} {μa : measure α} {μb : measure β} (h : measure_preserving e μa μb) : +lemma symm (e : α ≃ᵐ β) {μa : measure α} {μb : measure β} (h : measure_preserving e μa μb) : measure_preserving e.symm μb μa := ⟨e.symm.measurable, by rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]⟩ diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean index f3e10833b467e..cf65cef2c62d1 100644 --- a/src/measure_theory/constructions/pi.lean +++ b/src/measure_theory/constructions/pi.lean @@ -591,7 +591,7 @@ lemma measure_preserving_pi_equiv_pi_subtype_prod {ι : Type u} {α : ι → Typ ((measure.pi $ λ i : subtype p, μ i).prod (measure.pi $ λ i, μ i)) := begin set e := (measurable_equiv.pi_equiv_pi_subtype_prod α p).symm, - suffices : measure_preserving e _ _, from this.symm, + refine measure_preserving.symm e _, refine ⟨e.measurable, (pi_eq $ λ s hs, _).symm⟩, have : e ⁻¹' (pi univ s) = (pi univ (λ i : {i // p i}, s i)) ×ˢ (pi univ (λ i : {i // ¬p i}, s i)), @@ -613,7 +613,7 @@ lemma measure_preserving_pi_fin_succ_above_equiv {n : ℕ} {α : fin (n + 1) → ((μ i).prod $ measure.pi $ λ j, μ (i.succ_above j)) := begin set e := (measurable_equiv.pi_fin_succ_above_equiv α i).symm, - suffices : measure_preserving e _ _, from this.symm, + refine measure_preserving.symm e _, refine ⟨e.measurable, (pi_eq $ λ s hs, _).symm⟩, rw [e.map_apply, i.prod_univ_succ_above _, ← pi_pi, ← prod_prod], congr' 1 with ⟨x, f⟩, @@ -635,7 +635,7 @@ begin rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply], congr' 1, exact e.to_equiv.image_eq_preimage s }, simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure], - exact ((measurable_equiv.fun_unique α β).symm.measurable.measure_preserving _).symm + exact (e.symm.measurable.measure_preserving _).symm e.symm end lemma volume_preserving_fun_unique (α : Type u) (β : Type v) [unique α] [measure_space β] : diff --git a/src/measure_theory/constructions/prod.lean b/src/measure_theory/constructions/prod.lean index 36bf4d0157c5e..b9092bd1daf90 100644 --- a/src/measure_theory/constructions/prod.lean +++ b/src/measure_theory/constructions/prod.lean @@ -557,10 +557,10 @@ end end measure -namespace measure_preserving - open measure +namespace measure_preserving + variables {δ : Type*} [measurable_space δ] {μa : measure α} {μb : measure β} {μc : measure γ} {μd : measure δ} @@ -603,6 +603,34 @@ hf.skew_product this $ filter.eventually_of_forall $ λ _, hg.map_eq end measure_preserving +namespace quasi_measure_preserving + +lemma prod_of_right {f : α × β → γ} {μ : measure α} {ν : measure β} {τ : measure γ} + (hf : measurable f) [sigma_finite ν] + (h2f : ∀ᵐ x ∂μ, quasi_measure_preserving (λ y, f (x, y)) ν τ) : + quasi_measure_preserving f (μ.prod ν) τ := +begin + refine ⟨hf, _⟩, + refine absolutely_continuous.mk (λ s hs h2s, _), + simp_rw [map_apply hf hs, prod_apply (hf hs), preimage_preimage, + lintegral_congr_ae (h2f.mono (λ x hx, hx.preimage_null h2s)), lintegral_zero], +end + +lemma prod_of_left {α β γ} [measurable_space α] [measurable_space β] + [measurable_space γ] {f : α × β → γ} {μ : measure α} {ν : measure β} {τ : measure γ} + (hf : measurable f) [sigma_finite μ] [sigma_finite ν] + (h2f : ∀ᵐ y ∂ν, quasi_measure_preserving (λ x, f (x, y)) μ τ) : + quasi_measure_preserving f (μ.prod ν) τ := +begin + rw [← prod_swap], + convert (quasi_measure_preserving.prod_of_right (hf.comp measurable_swap) h2f).comp + ((measurable_swap.measure_preserving (ν.prod μ)).symm measurable_equiv.prod_comm) + .quasi_measure_preserving, + ext ⟨x, y⟩, refl, +end + +end quasi_measure_preserving + end measure_theory open measure_theory.measure @@ -627,6 +655,16 @@ lemma ae_measurable.snd [sigma_finite ν] {f : β → γ} (hf : ae_measurable f ν) : ae_measurable (λ (z : α × β), f z.2) (μ.prod ν) := hf.comp_measurable' measurable_snd prod_snd_absolutely_continuous +lemma measure_theory.ae_strongly_measurable.fst {γ} [topological_space γ] [sigma_finite ν] + {f : α → γ} (hf : ae_strongly_measurable f μ) : + ae_strongly_measurable (λ (z : α × β), f z.1) (μ.prod ν) := +hf.comp_measurable' measurable_fst prod_fst_absolutely_continuous + +lemma measure_theory.ae_strongly_measurable.snd {γ} [topological_space γ] [sigma_finite ν] + {f : β → γ} (hf : ae_strongly_measurable f ν) : + ae_strongly_measurable (λ (z : α × β), f z.2) (μ.prod ν) := +hf.comp_measurable' measurable_snd prod_snd_absolutely_continuous + /-- The Bochner integral is a.e.-measurable. This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable. -/ lemma measure_theory.ae_strongly_measurable.integral_prod_right' [sigma_finite ν] diff --git a/src/measure_theory/function/strongly_measurable.lean b/src/measure_theory/function/strongly_measurable.lean index ac8b93e9276e1..aa58802f339e8 100644 --- a/src/measure_theory/function/strongly_measurable.lean +++ b/src/measure_theory/function/strongly_measurable.lean @@ -1299,6 +1299,11 @@ lemma comp_measurable {γ : Type*} {mγ : measurable_space γ} {mα : measurable ae_strongly_measurable (g ∘ f) μ := hg.comp_ae_measurable hf.ae_measurable +lemma comp_measurable' {γ : Type*} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} + {μ : measure γ} {ν : measure α} (hg : ae_strongly_measurable g ν) (hf : measurable f) + (h : μ.map f ≪ ν) : ae_strongly_measurable (g ∘ f) μ := +(hg.mono' h).comp_measurable hf + lemma is_separable_ae_range (hf : ae_strongly_measurable f μ) : ∃ (t : set β), is_separable t ∧ ∀ᵐ x ∂μ, f x ∈ t := begin @@ -1513,10 +1518,12 @@ lemma apply_continuous_linear_map {φ : α → F →L[𝕜] E} ae_strongly_measurable (λ a, φ a v) μ := (continuous_linear_map.apply 𝕜 E v).continuous.comp_ae_strongly_measurable hφ -lemma ae_strongly_measurable_comp₂ (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F} +lemma _root_.continuous_linear_map.ae_strongly_measurable_comp₂ (L : E →L[𝕜] F →L[𝕜] G) + {f : α → E} {g : α → F} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) : ae_strongly_measurable (λ x, L (f x) (g x)) μ := L.continuous₂.comp_ae_strongly_measurable $ hf.prod_mk hg + end continuous_linear_map_nondiscrete_normed_field lemma _root_.ae_strongly_measurable_with_density_iff {E : Type*} [normed_group E] [normed_space ℝ E] diff --git a/src/measure_theory/group/arithmetic.lean b/src/measure_theory/group/arithmetic.lean index b713fee299f5d..8425505e590cf 100644 --- a/src/measure_theory/group/arithmetic.lean +++ b/src/measure_theory/group/arithmetic.lean @@ -57,6 +57,8 @@ class has_measurable_add (M : Type*) [measurable_space M] [has_add M] : Prop := (measurable_const_add : ∀ c : M, measurable ((+) c)) (measurable_add_const : ∀ c : M, measurable (+ c)) +export has_measurable_add (measurable_const_add measurable_add_const) + /-- We say that a type `has_measurable_add` if `uncurry (+)` is a measurable functions. For a typeclass assuming measurability of `((+) c)` and `(+ c)` see `has_measurable_add`. -/ class has_measurable_add₂ (M : Type*) [measurable_space M] [has_add M] : Prop := @@ -72,6 +74,8 @@ class has_measurable_mul (M : Type*) [measurable_space M] [has_mul M] : Prop := (measurable_const_mul : ∀ c : M, measurable ((*) c)) (measurable_mul_const : ∀ c : M, measurable (* c)) +export has_measurable_mul (measurable_const_mul measurable_mul_const) + /-- We say that a type `has_measurable_mul` if `uncurry (*)` is a measurable functions. For a typeclass assuming measurability of `((*) c)` and `(* c)` see `has_measurable_mul`. -/ @[to_additive has_measurable_add₂] @@ -79,7 +83,6 @@ class has_measurable_mul₂ (M : Type*) [measurable_space M] [has_mul M] : Prop (measurable_mul : measurable (λ p : M × M, p.1 * p.2)) export has_measurable_mul₂ (measurable_mul) - has_measurable_mul (measurable_const_mul measurable_mul_const) section mul @@ -152,9 +155,16 @@ instance pi.has_measurable_mul₂ {ι : Type*} {α : ι → Type*} [∀ i, has_m attribute [measurability] measurable.add' measurable.add ae_measurable.add ae_measurable.add' measurable.const_add ae_measurable.const_add measurable.add_const ae_measurable.add_const - end mul +/-- A version of `measurable_div_const` that assumes `has_measurable_mul` instead of + `has_measurable_div`. This can be nice to avoid unnecessary type-class assumptions. -/ +@[to_additive /-" A version of `measurable_sub_const` that assumes `has_measurable_add` instead of + `has_measurable_sub`. This can be nice to avoid unnecessary type-class assumptions. "-/] +lemma measurable_div_const' {G : Type*} [div_inv_monoid G] [measurable_space G] + [has_measurable_mul G] (g : G) : measurable (λ h, h / g) := +by simp_rw [div_eq_mul_inv, measurable_mul_const] + /-- This class assumes that the map `β × γ → β` given by `(x, y) ↦ x ^ y` is measurable. -/ class has_measurable_pow (β γ : Type*) [measurable_space β] [measurable_space γ] [has_pow β γ] := (measurable_pow : measurable (λ p : β × γ, p.1 ^ p.2)) @@ -217,6 +227,8 @@ class has_measurable_sub (G : Type*) [measurable_space G] [has_sub G] : Prop := (measurable_const_sub : ∀ c : G, measurable (λ x, c - x)) (measurable_sub_const : ∀ c : G, measurable (λ x, x - c)) +export has_measurable_sub (measurable_const_sub measurable_sub_const) + /-- We say that a type `has_measurable_sub` if `uncurry (-)` is a measurable functions. For a typeclass assuming measurability of `((-) c)` and `(- c)` see `has_measurable_sub`. -/ class has_measurable_sub₂ (G : Type*) [measurable_space G] [has_sub G] : Prop := @@ -230,6 +242,8 @@ For a typeclass assuming measurability of `uncurry (/)` see `has_measurable_div (measurable_const_div : ∀ c : G₀, measurable ((/) c)) (measurable_div_const : ∀ c : G₀, measurable (/ c)) +export has_measurable_div (measurable_const_div measurable_div_const) + /-- We say that a type `has_measurable_div` if `uncurry (/)` is a measurable functions. For a typeclass assuming measurability of `((/) c)` and `(/ c)` see `has_measurable_div`. -/ @[to_additive has_measurable_sub₂] @@ -447,9 +461,9 @@ class has_measurable_smul₂ (M α : Type*) [has_scalar M α] [measurable_space (measurable_smul : measurable (function.uncurry (•) : M × α → α)) export has_measurable_smul (measurable_const_smul measurable_smul_const) - has_measurable_smul₂ (measurable_smul) +export has_measurable_smul₂ (measurable_smul) export has_measurable_vadd (measurable_const_vadd measurable_vadd_const) - has_measurable_vadd₂ (measurable_vadd) +export has_measurable_vadd₂ (measurable_vadd) @[to_additive] instance has_measurable_smul_of_mul (M : Type*) [has_mul M] [measurable_space M] diff --git a/src/measure_theory/group/fundamental_domain.lean b/src/measure_theory/group/fundamental_domain.lean index c3332631afe08..1f5b9a0fbb8cf 100644 --- a/src/measure_theory/group/fundamental_domain.lean +++ b/src/measure_theory/group/fundamental_domain.lean @@ -119,12 +119,12 @@ h.pairwise_ae_disjoint.mono $ λ g₁ g₂ H, hν H end } @[to_additive] lemma image_of_equiv (h : is_fundamental_domain G s μ) - (f : measurable_equiv α α) (hfμ : measure_preserving f μ μ) + (f : α ≃ᵐ α) (hfμ : measure_preserving f μ μ) (e : equiv.perm G) (hef : ∀ g, semiconj f ((•) (e g)) ((•) g)) : is_fundamental_domain G (f '' s) μ := begin rw f.image_eq_preimage, - refine h.preimage_of_equiv hfμ.symm.quasi_measure_preserving e.symm.bijective (λ g x, _), + refine h.preimage_of_equiv (hfμ.symm f).quasi_measure_preserving e.symm.bijective (λ g x, _), rcases f.surjective x with ⟨x, rfl⟩, rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply] end diff --git a/src/measure_theory/group/integration.lean b/src/measure_theory/group/integration.lean index 8deb54b2fb5e0..1143a97806c65 100644 --- a/src/measure_theory/group/integration.lean +++ b/src/measure_theory/group/integration.lean @@ -5,6 +5,7 @@ Authors: Floris van Doorn -/ import measure_theory.integral.bochner import measure_theory.group.measure +import measure_theory.group.action /-! # Integration on Groups @@ -18,7 +19,7 @@ namespace measure_theory open measure topological_space open_locale ennreal -variables {𝕜 G E F : Type*} [measurable_space G] +variables {𝕜 M α G E F : Type*} [measurable_space G] variables [normed_group E] [normed_space ℝ E] [complete_space E] [normed_group F] variables {μ : measure G} {f : G → E} {g : G} @@ -68,10 +69,15 @@ begin simp [map_mul_right_eq_self μ g] end +@[simp, to_additive] +lemma lintegral_div_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) : + ∫⁻ x, f (x / g) ∂μ = ∫⁻ x, f x ∂μ := +by simp_rw [div_eq_mul_inv, lintegral_mul_right_eq_self f g⁻¹] + /-- Translating a function by left-multiplication does not change its integral with respect to a left-invariant measure. -/ -@[to_additive "Translating a function by left-addition does not change its integral with respect to -a left-invariant measure."] +@[simp, to_additive "Translating a function by left-addition does not change its integral with + respect to a left-invariant measure."] lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) : ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ := begin @@ -82,8 +88,8 @@ end /-- Translating a function by right-multiplication does not change its integral with respect to a right-invariant measure. -/ -@[to_additive "Translating a function by right-addition does not change its integral with respect to -a right-invariant measure."] +@[simp, to_additive "Translating a function by right-addition does not change its integral with + respect to a right-invariant measure."] lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) : ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ := begin @@ -92,6 +98,11 @@ begin rw [← h_mul.integral_map, map_mul_right_eq_self] end +@[simp, to_additive] +lemma integral_div_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) : + ∫ x, f (x / g) ∂μ = ∫ x, f x ∂μ := +by simp_rw [div_eq_mul_inv, integral_mul_right_eq_self f g⁻¹] + /-- If some left-translate of a function negates it, then the integral of the function with respect to a left-invariant measure is 0. -/ @[to_additive "If some left-translate of a function negates it, then the integral of the function @@ -139,7 +150,17 @@ begin { exact (measurable_id'.const_mul g⁻¹).inv.ae_measurable } end -@[to_additive] +@[simp, to_additive] +lemma integrable_comp_div_left (f : G → F) + [is_inv_invariant μ] [is_mul_left_invariant μ] (g : G) : + integrable (λ t, f (g / t)) μ ↔ integrable f μ := +begin + refine ⟨λ h, _, λ h, h.comp_div_left g⟩, + convert h.comp_inv.comp_mul_left g⁻¹, + simp_rw [div_inv_eq_mul, mul_inv_cancel_left] +end + +@[simp, to_additive] lemma integral_div_left_eq_self (f : G → E) (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ] (x' : G) : ∫ x, f (x' / x) ∂μ = ∫ x, f x ∂μ := by simp_rw [div_eq_mul_inv, integral_inv_eq_self (λ x, f (x' * x)) μ, @@ -147,6 +168,21 @@ by simp_rw [div_eq_mul_inv, integral_inv_eq_self (λ x, f (x' * x)) μ, end measurable_mul +section smul + +variables [group G] [measurable_space α] [mul_action G α] [has_measurable_smul G α] + +@[simp, to_additive] +lemma integral_smul_eq_self {μ : measure α} [smul_invariant_measure G α μ] (f : α → E) {g : G} : + ∫ x, f (g • x) ∂μ = ∫ x, f x ∂μ := +begin + have h : measurable_embedding (λ x : α, g • x) := + (measurable_equiv.smul g).measurable_embedding, + rw [← h.integral_map, map_smul] +end + +end smul + section topological_group diff --git a/src/measure_theory/group/measurable_equiv.lean b/src/measure_theory/group/measurable_equiv.lean index 56e6a295af42d..4fda5629527a0 100644 --- a/src/measure_theory/group/measurable_equiv.lean +++ b/src/measure_theory/group/measurable_equiv.lean @@ -160,4 +160,18 @@ def inv (G) [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] : lemma symm_inv {G} [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] : (inv G).symm = inv G := rfl +/-- `equiv.div_right` as a `measurable_equiv`. -/ +@[to_additive /-" `equiv.sub_right` as a `measurable_equiv` "-/] +def div_right [has_measurable_mul G] (g : G) : G ≃ᵐ G := +{ to_equiv := equiv.div_right g, + measurable_to_fun := measurable_div_const' g, + measurable_inv_fun := measurable_mul_const g } + +/-- `equiv.div_left` as a `measurable_equiv` -/ +@[to_additive /-" `equiv.sub_left` as a `measurable_equiv` "-/] +def div_left [has_measurable_mul G] [has_measurable_inv G] (g : G) : G ≃ᵐ G := +{ to_equiv := equiv.div_left g, + measurable_to_fun := measurable_id.const_div g, + measurable_inv_fun := measurable_inv.mul_const g } + end measurable_equiv diff --git a/src/measure_theory/group/measure.lean b/src/measure_theory/group/measure.lean index e4655360e0380..16c0670da6b6d 100644 --- a/src/measure_theory/group/measure.lean +++ b/src/measure_theory/group/measure.lean @@ -3,6 +3,7 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ +import dynamics.ergodic.measure_preserving import measure_theory.measure.regular import measure_theory.group.measurable_equiv import measure_theory.measure.open_pos @@ -34,12 +35,12 @@ namespace measure /-- A measure `μ` on a measurable additive group is left invariant if the measure of left translations of a set are equal to the measure of the set itself. -/ class is_add_left_invariant [has_add G] (μ : measure G) : Prop := -( map_add_left_eq_self : ∀ g : G, map ((+) g) μ = μ) +(map_add_left_eq_self : ∀ g : G, map ((+) g) μ = μ) /-- A measure `μ` on a measurable group is left invariant if the measure of left translations of a set are equal to the measure of the set itself. -/ @[to_additive] class is_mul_left_invariant [has_mul G] (μ : measure G) : Prop := -( map_mul_left_eq_self : ∀ g : G, map ((*) g) μ = μ) +(map_mul_left_eq_self : ∀ g : G, map ((*) g) μ = μ) /-- A measure `μ` on a measurable additive group is right invariant if the measure of right translations of a set are equal to the measure of the set itself. -/ @@ -66,9 +67,31 @@ is_mul_left_invariant.map_mul_left_eq_self g lemma map_mul_right_eq_self (μ : measure G) [is_mul_right_invariant μ] (g : G) : map (* g) μ = μ := is_mul_right_invariant.map_mul_right_eq_self g +@[to_additive] +instance [is_mul_left_invariant μ] (c : ℝ≥0∞) : is_mul_left_invariant (c • μ) := +⟨λ g, by rw [map_smul, map_mul_left_eq_self]⟩ + +@[to_additive] +instance [is_mul_right_invariant μ] (c : ℝ≥0∞) : is_mul_right_invariant (c • μ) := +⟨λ g, by rw [map_smul, map_mul_right_eq_self]⟩ + +section has_measurable_mul + +variables [has_measurable_mul G] + +@[to_additive] +lemma measure_preserving_mul_left (μ : measure G) [is_mul_left_invariant μ] (g : G) : + measure_preserving ((*) g) μ μ := +⟨measurable_const_mul g, map_mul_left_eq_self μ g⟩ + +@[to_additive] +lemma measure_preserving_mul_right (μ : measure G) [is_mul_right_invariant μ] (g : G) : + measure_preserving (* g) μ μ := +⟨measurable_mul_const g, map_mul_right_eq_self μ g⟩ + /-- An alternative way to prove that `μ` is left invariant under multiplication. -/ -@[to_additive "An alternative way to prove that `μ` is left invariant under addition."] -lemma forall_measure_preimage_mul_iff [has_measurable_mul G] (μ : measure G) : +@[to_additive /-" An alternative way to prove that `μ` is left invariant under addition. "-/] +lemma forall_measure_preimage_mul_iff (μ : measure G) : (∀ (g : G) (A : set G), measurable_set A → μ ((λ h, g * h) ⁻¹' A) = μ A) ↔ is_mul_left_invariant μ := begin @@ -79,9 +102,9 @@ begin exact ⟨λ h, ⟨h⟩, λ h, h.1⟩ end -/-- An alternative way to prove that `μ` is left invariant under multiplication. -/ -@[to_additive "An alternative way to prove that `μ` is left invariant under addition."] -lemma forall_measure_preimage_mul_right_iff [has_measurable_mul G] (μ : measure G) : +/-- An alternative way to prove that `μ` is right invariant under multiplication. -/ +@[to_additive /-" An alternative way to prove that `μ` is right invariant under addition. "-/] +lemma forall_measure_preimage_mul_right_iff (μ : measure G) : (∀ (g : G) (A : set G), measurable_set A → μ ((λ h, h * g) ⁻¹' A) = μ A) ↔ is_mul_right_invariant μ := begin @@ -92,13 +115,7 @@ begin exact ⟨λ h, ⟨h⟩, λ h, h.1⟩ end -@[to_additive] -instance [is_mul_left_invariant μ] (c : ℝ≥0∞) : is_mul_left_invariant (c • μ) := -⟨λ g, by rw [map_smul, map_mul_left_eq_self]⟩ - -@[to_additive] -instance [is_mul_right_invariant μ] (c : ℝ≥0∞) : is_mul_right_invariant (c • μ) := -⟨λ g, by rw [map_smul, map_mul_right_eq_self]⟩ +end has_measurable_mul end mul @@ -131,6 +148,21 @@ calc μ ((λ h, h * g) ⁻¹' A) = map (λ h, h * g) μ A : ((measurable_equiv.mul_right g).map_apply A).symm ... = μ A : by rw map_mul_right_eq_self μ g +@[to_additive] +lemma map_mul_left_ae (μ : measure G) [is_mul_left_invariant μ] (x : G) : + filter.map (λ h, x * h) μ.ae = μ.ae := +((measurable_equiv.mul_left x).map_ae μ).trans $ congr_arg ae $ map_mul_left_eq_self μ x + +@[to_additive] +lemma map_mul_right_ae (μ : measure G) [is_mul_right_invariant μ] (x : G) : + filter.map (λ h, h * x) μ.ae = μ.ae := +((measurable_equiv.mul_right x).map_ae μ).trans $ congr_arg ae $ map_mul_right_eq_self μ x + +@[to_additive] +lemma map_div_right_ae (μ : measure G) [is_mul_right_invariant μ] (x : G) : + filter.map (λ t, t / x) μ.ae = μ.ae := +((measurable_equiv.div_right x).map_ae μ).trans $ congr_arg ae $ map_div_right_eq_self μ x + end group namespace measure @@ -231,6 +263,11 @@ begin exact (map_map measurable_inv (measurable_const_mul g)).symm end +@[to_additive] +lemma map_div_left_ae (μ : measure G) [is_mul_left_invariant μ] [is_inv_invariant μ] (x : G) : + filter.map (λ t, x / t) μ.ae = μ.ae := +((measurable_equiv.div_left x).map_ae μ).trans $ congr_arg ae $ map_div_left_eq_self μ x + end mul_inv end measure diff --git a/src/measure_theory/group/prod.lean b/src/measure_theory/group/prod.lean index c90930892f694..9e84e468f01ff 100644 --- a/src/measure_theory/group/prod.lean +++ b/src/measure_theory/group/prod.lean @@ -33,12 +33,12 @@ The proof in [Halmos] seems to contain an omission in §60 Th. A, see -/ noncomputable theory -open set (hiding prod_eq) function measure_theory +open set (hiding prod_eq) function measure_theory filter (hiding map) open_locale classical ennreal pointwise measure_theory variables (G : Type*) [measurable_space G] variables [group G] [has_measurable_mul₂ G] -variables (μ ν : measure G) [sigma_finite ν] [sigma_finite μ] +variables (μ ν : measure G) [sigma_finite ν] [sigma_finite μ] {E : set G} /-- The map `(x, y) ↦ (x, xy)` as a `measurable_equiv`. This is a shear mapping. -/ @[to_additive "The map `(x, y) ↦ (x, x + y)` as a `measurable_equiv`. @@ -54,23 +54,18 @@ namespace measure_theory open measure -/-- This condition is part of the definition of a measurable group in [Halmos, §59]. - There, the map in this lemma is called `S`. -/ -@[to_additive map_prod_sum_eq] +/-- A shear mapping preserves the measure `μ.prod ν`. +This condition is part of the definition of a measurable group in [Halmos, §59]. +There, the map in this lemma is called `S`. -/ +@[to_additive map_prod_sum_eq /-" An additive shear mapping preserves the measure `μ.prod ν`. "-/] lemma map_prod_mul_eq [is_mul_left_invariant ν] : map (λ z : G × G, (z.1, z.1 * z.2)) (μ.prod ν) = μ.prod ν := -begin - refine (prod_eq _).symm, intros s t hs ht, - simp_rw [map_apply (measurable_fst.prod_mk (measurable_fst.mul measurable_snd)) (hs.prod ht), - prod_apply ((measurable_fst.prod_mk (measurable_fst.mul measurable_snd)) (hs.prod ht)), - preimage_preimage], - conv_lhs { congr, skip, funext, rw [mk_preimage_prod_right_fn_eq_if ((*) x), measure_if] }, - simp_rw [measure_preimage_mul, lintegral_indicator _ hs, set_lintegral_const, mul_comm] -end +((measure_preserving.id μ).skew_product measurable_mul + (filter.eventually_of_forall $ map_mul_left_eq_self ν)).map_eq /-- The function we are mapping along is `SR` in [Halmos, §59], where `S` is the map in `map_prod_mul_eq` and `R` is `prod.swap`. -/ -@[to_additive map_prod_add_eq_swap] +@[to_additive map_prod_add_eq_swap /-" "-/] lemma map_prod_mul_eq_swap [is_mul_left_invariant μ] : map (λ z : G × G, (z.2, z.2 * z.1)) (μ.prod ν) = ν.prod μ := begin @@ -80,7 +75,7 @@ begin end @[to_additive] -lemma measurable_measure_mul_right {E : set G} (hE : measurable_set E) : +lemma measurable_measure_mul_right (hE : measurable_set E) : measurable (λ x, μ ((λ y, y * x) ⁻¹' E)) := begin suffices : measurable (λ y, @@ -99,11 +94,22 @@ lemma map_prod_inv_mul_eq [is_mul_left_invariant ν] : map (λ z : G × G, (z.1, z.1⁻¹ * z.2)) (μ.prod ν) = μ.prod ν := (measurable_equiv.shear_mul_right G).map_apply_eq_iff_map_symm_apply_eq.mp $ map_prod_mul_eq μ ν +@[to_additive] +lemma quasi_measure_preserving_div [is_mul_right_invariant μ] : + quasi_measure_preserving (λ (p : G × G), p.1 / p.2) (μ.prod μ) μ := +begin + refine quasi_measure_preserving.prod_of_left measurable_div _, + simp_rw [div_eq_mul_inv], + apply eventually_of_forall, + refine λ y, ⟨measurable_mul_const y⁻¹, (map_mul_right_eq_self μ y⁻¹).absolutely_continuous⟩ +end + +variables [is_mul_left_invariant μ] + /-- The function we are mapping along is `S⁻¹R` in [Halmos, §59], where `S` is the map in `map_prod_mul_eq` and `R` is `prod.swap`. -/ @[to_additive map_prod_neg_add_eq_swap] -lemma map_prod_inv_mul_eq_swap [is_mul_left_invariant μ] : - map (λ z : G × G, (z.2, z.2⁻¹ * z.1)) (μ.prod ν) = ν.prod μ := +lemma map_prod_inv_mul_eq_swap : map (λ z : G × G, (z.2, z.2⁻¹ * z.1)) (μ.prod ν) = ν.prod μ := begin rw [← prod_swap], simp_rw @@ -114,7 +120,7 @@ end /-- The function we are mapping along is `S⁻¹RSR` in [Halmos, §59], where `S` is the map in `map_prod_mul_eq` and `R` is `prod.swap`. -/ @[to_additive map_prod_add_neg_eq] -lemma map_prod_mul_inv_eq [is_mul_left_invariant μ] [is_mul_left_invariant ν] : +lemma map_prod_mul_inv_eq [is_mul_left_invariant ν] : map (λ z : G × G, (z.2 * z.1, z.1⁻¹)) (μ.prod ν) = μ.prod ν := begin suffices : map ((λ z : G × G, (z.2, z.2⁻¹ * z.1)) ∘ (λ z : G × G, (z.2, z.2 * z.1))) (μ.prod ν) = @@ -125,7 +131,7 @@ begin map_prod_inv_mul_eq_swap ν μ] end -@[to_additive] lemma quasi_measure_preserving_inv [is_mul_left_invariant μ] : +@[to_additive] lemma quasi_measure_preserving_inv : quasi_measure_preserving (has_inv.inv : G → G) μ μ := begin refine ⟨measurable_inv, absolutely_continuous.mk $ λ s hsm hμs, _⟩, @@ -140,8 +146,11 @@ begin end @[to_additive] -lemma measure_inv_null [is_mul_left_invariant μ] {E : set G} : - μ ((λ x, x⁻¹) ⁻¹' E) = 0 ↔ μ E = 0 := +lemma map_inv_absolutely_continuous : map has_inv.inv μ ≪ μ := +(quasi_measure_preserving_inv μ).absolutely_continuous + +@[to_additive] +lemma measure_inv_null : μ E⁻¹ = 0 ↔ μ E = 0 := begin refine ⟨λ hE, _, (quasi_measure_preserving_inv μ).preimage_null⟩, convert (quasi_measure_preserving_inv μ).preimage_null hE, @@ -149,7 +158,14 @@ begin end @[to_additive] -lemma lintegral_lintegral_mul_inv [is_mul_left_invariant μ] [is_mul_left_invariant ν] +lemma absolutely_continuous_map_inv : μ ≪ map has_inv.inv μ := +begin + refine absolutely_continuous.mk (λ s hs, _), + simp_rw [map_apply measurable_inv hs, inv_preimage, measure_inv_null, imp_self] +end + +@[to_additive] +lemma lintegral_lintegral_mul_inv [is_mul_left_invariant ν] (f : G → G → ℝ≥0∞) (hf : ae_measurable (uncurry f) (μ.prod ν)) : ∫⁻ x, ∫⁻ y, f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ x, ∫⁻ y, f x y ∂ν ∂μ := begin @@ -164,21 +180,62 @@ begin end @[to_additive] -lemma measure_mul_right_null [is_mul_left_invariant μ] {E : set G} (y : G) : +lemma measure_mul_right_null (y : G) : μ ((λ x, x * y) ⁻¹' E) = 0 ↔ μ E = 0 := -calc μ ((λ x, x * y) ⁻¹' E) = 0 ↔ μ (has_inv.inv ⁻¹' ((λ x, y⁻¹ * x) ⁻¹' (has_inv.inv ⁻¹' E))) = 0 : - by simp only [preimage_preimage, mul_inv_rev, inv_inv] +calc μ ((λ x, x * y) ⁻¹' E) = 0 ↔ μ ((λ x, y⁻¹ * x) ⁻¹' E⁻¹)⁻¹ = 0 : + by simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv] ... ↔ μ E = 0 : by simp only [measure_inv_null μ, measure_preimage_mul] @[to_additive] -lemma measure_mul_right_ne_zero [is_mul_left_invariant μ] {E : set G} +lemma measure_mul_right_ne_zero (h2E : μ E ≠ 0) (y : G) : μ ((λ x, x * y) ⁻¹' E) ≠ 0 := (not_iff_not_of_iff (measure_mul_right_null μ y)).mpr h2E +@[to_additive] lemma quasi_measure_preserving_mul_right (g : G) : + quasi_measure_preserving (λ h : G, h * g) μ μ := +begin + refine ⟨measurable_mul_const g, absolutely_continuous.mk $ λ s hs, _⟩, + rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null], exact id, +end + +@[to_additive] +lemma map_mul_right_absolutely_continuous (g : G) : map (* g) μ ≪ μ := +(quasi_measure_preserving_mul_right μ g).absolutely_continuous + +@[to_additive] +lemma absolutely_continuous_map_mul_right (g : G) : μ ≪ map (* g) μ := +begin + refine absolutely_continuous.mk (λ s hs, _), + rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null], exact id +end + +@[to_additive] lemma quasi_measure_preserving_div_left (g : G) : + quasi_measure_preserving (λ h : G, g / h) μ μ := +begin + refine ⟨measurable_const.div measurable_id, _⟩, + simp_rw [div_eq_mul_inv], + rw [← map_map (measurable_const_mul g) measurable_inv], + refine ((map_inv_absolutely_continuous μ).map $ measurable_const_mul g).trans _, + rw [map_mul_left_eq_self], +end + +@[to_additive] +lemma map_div_left_absolutely_continuous (g : G) : map (λ h, g / h) μ ≪ μ := +(quasi_measure_preserving_div_left μ g).absolutely_continuous + +@[to_additive] +lemma absolutely_continuous_map_div_left (g : G) : μ ≪ map (λ h, g / h) μ := +begin + simp_rw [div_eq_mul_inv], + rw [← map_map (measurable_const_mul g) measurable_inv], + conv_lhs { rw [← map_mul_left_eq_self μ g] }, + exact (absolutely_continuous_map_inv μ).map (measurable_const_mul g) +end + /-- This is the computation performed in the proof of [Halmos, §60 Th. A]. -/ @[to_additive] -lemma measure_mul_lintegral_eq [is_mul_left_invariant μ] - [is_mul_left_invariant ν] {E : set G} (Em : measurable_set E) (f : G → ℝ≥0∞) (hf : measurable f) : +lemma measure_mul_lintegral_eq + [is_mul_left_invariant ν] (Em : measurable_set E) (f : G → ℝ≥0∞) (hf : measurable f) : μ E * ∫⁻ y, f y ∂ν = ∫⁻ x, ν ((λ z, z * x) ⁻¹' E) * f (x⁻¹) ∂μ := begin rw [← set_lintegral_one, ← lintegral_indicator _ Em, @@ -196,9 +253,10 @@ begin end /-- Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other. -/ -@[to_additive] -lemma absolutely_continuous_of_is_mul_left_invariant - [is_mul_left_invariant μ] [is_mul_left_invariant ν] (hν : ν ≠ 0) : μ ≪ ν := +@[to_additive /-" Any two nonzero left-invariant measures are absolutely continuous w.r.t. each +other. "-/] +lemma absolutely_continuous_of_is_mul_left_invariant [is_mul_left_invariant ν] (hν : ν ≠ 0) : + μ ≪ ν := begin refine absolutely_continuous.mk (λ E Em hνE, _), have h1 := measure_mul_lintegral_eq μ ν Em 1 measurable_one, @@ -208,8 +266,8 @@ begin end @[to_additive] -lemma ae_measure_preimage_mul_right_lt_top [is_mul_left_invariant μ] [is_mul_left_invariant ν] - {E : set G} (Em : measurable_set E) (hμE : μ E ≠ ∞) : +lemma ae_measure_preimage_mul_right_lt_top [is_mul_left_invariant ν] + (Em : measurable_set E) (hμE : μ E ≠ ∞) : ∀ᵐ x ∂μ, ν ((λ y, y * x) ⁻¹' E) < ∞ := begin refine ae_of_forall_measure_lt_top_ae_restrict' ν.inv _ _, @@ -226,8 +284,8 @@ begin end @[to_additive] -lemma ae_measure_preimage_mul_right_lt_top_of_ne_zero [is_mul_left_invariant μ] - [is_mul_left_invariant ν] {E : set G} (Em : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) : +lemma ae_measure_preimage_mul_right_lt_top_of_ne_zero [is_mul_left_invariant ν] + (Em : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) : ∀ᵐ x ∂μ, ν ((λ y, y * x) ⁻¹' E) < ∞ := begin refine (ae_measure_preimage_mul_right_lt_top ν ν Em h3E).filter_mono _, @@ -247,8 +305,8 @@ end not justified. We prove this inequality for almost all `x` in `measure_theory.ae_measure_preimage_mul_right_lt_top_of_ne_zero`. -/ @[to_additive] -lemma measure_lintegral_div_measure [is_mul_left_invariant μ] - [is_mul_left_invariant ν] {E : set G} (Em : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) +lemma measure_lintegral_div_measure [is_mul_left_invariant ν] + (Em : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) (f : G → ℝ≥0∞) (hf : measurable f) : μ E * ∫⁻ y, f y⁻¹ / ν ((λ x, x * y⁻¹) ⁻¹' E) ∂ν = ∫⁻ x, f x ∂μ := begin @@ -262,8 +320,7 @@ begin end @[to_additive] -lemma measure_mul_measure_eq [is_mul_left_invariant μ] - [is_mul_left_invariant ν] {E F : set G} +lemma measure_mul_measure_eq [is_mul_left_invariant ν] {E F : set G} (hE : measurable_set E) (hF : measurable_set F) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) : μ E * ν F = ν E * μ F := begin @@ -276,9 +333,9 @@ begin end /-- Left invariant Borel measures on a measurable group are unique (up to a scalar). -/ -@[to_additive] -lemma measure_eq_div_smul [is_mul_left_invariant μ] - [is_mul_left_invariant ν] {E : set G} +@[to_additive /-" Left invariant Borel measures on an additive measurable group are unique + (up to a scalar). "-/] +lemma measure_eq_div_smul [is_mul_left_invariant ν] (hE : measurable_set E) (h2E : ν E ≠ 0) (h3E : ν E ≠ ∞) : μ = (μ E / ν E) • ν := begin ext1 F hF, diff --git a/src/measure_theory/integral/divergence_theorem.lean b/src/measure_theory/integral/divergence_theorem.lean index e1fca7fc1fd1b..03385590b4f6f 100644 --- a/src/measure_theory/integral/divergence_theorem.lean +++ b/src/measure_theory/integral/divergence_theorem.lean @@ -380,7 +380,7 @@ begin refine integral_divergence_of_has_fderiv_within_at_off_countable_of_equiv e _ _ (λ _, f) (λ _, F') s hs a b hle (λ i, Hc) (λ x hx i, Hd x hx) _ _ _, { exact λ x y, (order_iso.fun_unique (fin 1) ℝ).symm.le_iff_le }, - { exact (volume_preserving_fun_unique (fin 1) ℝ).symm }, + { exact (volume_preserving_fun_unique (fin 1) ℝ).symm _ }, { intro x, rw [fin.sum_univ_one, hF', e_symm, pi.single_eq_same, one_smul] }, { rw [interval_integrable_iff_integrable_Ioc_of_le hle] at Hi, exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm } @@ -442,7 +442,7 @@ calc ∫ x in Icc a b, f' x (1, 0) + g' x (0, 1) refine integral_divergence_of_has_fderiv_within_at_off_countable_of_equiv e _ _ ![f, g] ![f', g'] s hs a b hle _ (λ x hx, _) _ _ Hi, { exact λ x y, (order_iso.fin_two_arrow_iso ℝ).symm.le_iff_le }, - { exact (volume_preserving_fin_two_arrow ℝ).symm }, + { exact (volume_preserving_fin_two_arrow ℝ).symm _ }, { exact fin.forall_fin_two.2 ⟨Hcf, Hcg⟩ }, { rw [Icc_prod_eq, interior_prod_eq, interior_Icc, interior_Icc] at hx, exact fin.forall_fin_two.2 ⟨Hdf x hx, Hdg x hx⟩ }, @@ -453,7 +453,7 @@ calc ∫ x in Icc a b, f' x (1, 0) + g' x (0, 1) begin have : ∀ (a b : ℝ¹) (f : ℝ¹ → E), ∫ x in Icc a b, f x = ∫ x in Icc (a 0) (b 0), f (λ _, x), { intros a b f, - convert ((volume_preserving_fun_unique (fin 1) ℝ).symm.set_integral_preimage_emb + convert (((volume_preserving_fun_unique (fin 1) ℝ).symm _).set_integral_preimage_emb (measurable_equiv.measurable_embedding _) _ _).symm, exact ((order_iso.fun_unique (fin 1) ℝ).symm.preimage_Icc a b).symm }, simp only [fin.sum_univ_two, this], diff --git a/src/measure_theory/integral/torus_integral.lean b/src/measure_theory/integral/torus_integral.lean index a9ec6d145be3f..d4f8f02512a3e 100644 --- a/src/measure_theory/integral/torus_integral.lean +++ b/src/measure_theory/integral/torus_integral.lean @@ -207,7 +207,7 @@ begin from (order_iso.fun_unique (fin 1) ℝ).symm.preimage_Icc _ _, simp only [torus_integral, circle_integral, interval_integral.integral_of_le real.two_pi_pos.le, measure.restrict_congr_set Ioc_ae_eq_Icc, deriv_circle_map, fin.prod_univ_one, - ← (volume_preserving_fun_unique (fin 1) ℝ).symm.set_integral_preimage_emb + ← ((volume_preserving_fun_unique (fin 1) ℝ).symm _).set_integral_preimage_emb (measurable_equiv.measurable_embedding _), this, measurable_equiv.fun_unique_symm_apply], simp only [torus_map, circle_map, zero_add], rcongr @@ -221,7 +221,7 @@ lemma torus_integral_succ_above {f : ℂⁿ⁺¹ → E} {c : ℂⁿ⁺¹} {R : begin set e : ℝ × ℝⁿ ≃ᵐ ℝⁿ⁺¹ := (measurable_equiv.pi_fin_succ_above_equiv (λ _, ℝ) i).symm, have hem : measure_preserving e, - from (volume_preserving_pi_fin_succ_above_equiv (λ j : fin (n + 1), ℝ) i).symm, + from (volume_preserving_pi_fin_succ_above_equiv (λ j : fin (n + 1), ℝ) i).symm _, have heπ : e ⁻¹' (Icc 0 (λ _, 2 * π)) = Icc 0 (2 * π) ×ˢ Icc (0 : ℝⁿ) (λ _, 2 * π), from ((order_iso.pi_fin_succ_above_iso (λ _, ℝ) i).symm.preimage_Icc _ _).trans (Icc_prod_eq _ _), diff --git a/src/measure_theory/measure/complex_lebesgue.lean b/src/measure_theory/measure/complex_lebesgue.lean index 65712d77cba8b..5022bc9ea59bc 100644 --- a/src/measure_theory/measure/complex_lebesgue.lean +++ b/src/measure_theory/measure/complex_lebesgue.lean @@ -34,7 +34,7 @@ equiv_real_prodₗ.to_homeomorph.to_measurable_equiv lemma volume_preserving_equiv_pi : measure_preserving measurable_equiv_pi := -(measurable_equiv_pi.symm.measurable.measure_preserving _).symm +(measurable_equiv_pi.symm.measurable.measure_preserving _).symm _ lemma volume_preserving_equiv_real_prod : measure_preserving measurable_equiv_real_prod := (volume_preserving_fin_two_arrow ℝ).comp volume_preserving_equiv_pi diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean index ff19fb7c172dd..698d983613721 100644 --- a/src/measure_theory/measure/lebesgue.lean +++ b/src/measure_theory/measure/lebesgue.lean @@ -334,7 +334,7 @@ begin exact this.comp measurable_fst }, exact (measure_preserving.id _).skew_product g_meas (eventually_of_forall (λ a, map_add_left_eq_self _ _)) }, - exact (A.symm.comp B).comp A, + exact ((A.symm e).comp B).comp A, end /-- Any invertible matrix rescales Lebesgue measure through the absolute value of its diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index f86260b4fabfc..f8dfc0c70a098 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -1760,6 +1760,10 @@ protected lemma id {m0 : measurable_space α} (μ : measure α) : quasi_measure_ variables {μa μa' : measure α} {μb μb' : measure β} {μc : measure γ} {f : α → β} +protected lemma _root_.measurable.quasi_measure_preserving {m0 : measurable_space α} + (hf : measurable f) (μ : measure α) : quasi_measure_preserving f μ (μ.map f) := +⟨hf, absolutely_continuous.rfl⟩ + lemma mono_left (h : quasi_measure_preserving f μa μb) (ha : μa' ≪ μa) : quasi_measure_preserving f μa' μb := ⟨h.1, (ha.map h.1).trans h.2⟩ @@ -3056,6 +3060,9 @@ by rw [← (map_measurable_equiv_injective e).eq_iff, map_map_symm, eq_comm] lemma restrict_map (e : α ≃ᵐ β) (s : set β) : (μ.map e).restrict s = (μ.restrict $ e ⁻¹' s).map e := e.measurable_embedding.restrict_map _ _ +lemma map_ae (f : α ≃ᵐ β) (μ : measure α) : filter.map f μ.ae = (map f μ).ae := +by { ext s, simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply] } + end measurable_equiv