From 822244f7f7ea4596700632bcb08e79b6dcb52369 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 12 Feb 2022 08:07:23 +0000 Subject: [PATCH] refactor(measure_theory/group/basic): rename and split (#11952) * Rename `measure_theory/group/basic` -> `measure_theory/group/measure`. It was not the bottom file in this folder in the import hierarchy (arithmetic is below it). * Split off some results to `measure_theory/group/integration`. This reduces imports in some files, and makes the organization more clear. Furthermore, I will add some integrability results and more integrals in a follow-up PR. * Prove a general instance `pi.is_mul_left_invariant` * Remove lemmas specifically about `volume` on `real` in favor on the general lemmas. ```lean real.map_volume_add_left -> map_add_left_eq_self real.map_volume_pi_add_left -> map_add_left_eq_self real.volume_preimage_add_left -> measure_preimage_add real.volume_pi_preimage_add_left -> measure_preimage_add real.map_volume_add_right -> map_add_right_eq_self real.volume_preimage_add_right -> measure_preimage_add_right ``` --- src/analysis/box_integral/integrability.lean | 1 + src/analysis/fourier.lean | 1 + src/measure_theory/constructions/pi.lean | 21 ++++ src/measure_theory/group/arithmetic.lean | 7 ++ src/measure_theory/group/integration.lean | 108 ++++++++++++++++++ .../group/{basic.lean => measure.lean} | 40 +------ src/measure_theory/group/prod.lean | 1 + src/measure_theory/integral/bochner.lean | 48 -------- .../integral/interval_integral.lean | 2 +- src/measure_theory/integral/periodic.lean | 4 +- src/measure_theory/measure/haar_lebesgue.lean | 6 +- src/measure_theory/measure/lebesgue.lean | 43 ++----- src/number_theory/liouville/measure.lean | 4 +- 13 files changed, 156 insertions(+), 130 deletions(-) create mode 100644 src/measure_theory/group/integration.lean rename src/measure_theory/group/{basic.lean => measure.lean} (91%) diff --git a/src/analysis/box_integral/integrability.lean b/src/analysis/box_integral/integrability.lean index eaf33e8b57851..51efcc90f5fcc 100644 --- a/src/analysis/box_integral/integrability.lean +++ b/src/analysis/box_integral/integrability.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ import analysis.box_integral.basic +import measure_theory.measure.regular /-! # McShane integrability vs Bochner integrability diff --git a/src/analysis/fourier.lean b/src/analysis/fourier.lean index b89aff5426f50..89c31c8098ea9 100644 --- a/src/analysis/fourier.lean +++ b/src/analysis/fourier.lean @@ -8,6 +8,7 @@ import analysis.inner_product_space.l2_space import measure_theory.function.continuous_map_dense import measure_theory.function.l2_space import measure_theory.measure.haar +import measure_theory.group.integration import topology.metric_space.emetric_paracompact import topology.continuous_function.stone_weierstrass diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean index 33632d0bbee43..ecd36a1ec295f 100644 --- a/src/measure_theory/constructions/pi.lean +++ b/src/measure_theory/constructions/pi.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ import measure_theory.constructions.prod +import measure_theory.group.measure /-! # Product measures @@ -534,6 +535,18 @@ begin simp only [equiv.self_comp_symm, map_id] end +@[to_additive] instance pi.is_mul_left_invariant [∀ i, group (α i)] [∀ i, has_measurable_mul (α i)] + [∀ i, is_mul_left_invariant (μ i)] : is_mul_left_invariant (measure.pi μ) := +begin + refine ⟨λ x, (measure.pi_eq (λ s hs, _)).symm⟩, + have A : has_mul.mul x ⁻¹' (set.pi univ (λ (i : ι), s i)) + = set.pi univ (λ (i : ι), ((*) (x i)) ⁻¹' (s i)), by { ext, simp }, + rw [measure.map_apply (measurable_const_mul x) (measurable_set.univ_pi_fintype hs), A, + pi_pi], + simp only [measure_preimage_mul] +end + + end measure instance measure_space.pi [Π i, measure_space (α i)] : measure_space (Π i, α i) := ⟨measure.pi (λ i, volume)⟩ @@ -557,6 +570,14 @@ lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (v volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) := measure.pi_closed_ball _ _ hr +open measure +@[to_additive] +instance pi.is_mul_left_invariant_volume [∀ i, group (α i)] [Π i, measure_space (α i)] + [∀ i, sigma_finite (volume : measure (α i))] + [∀ i, has_measurable_mul (α i)] [∀ i, is_mul_left_invariant (volume : measure (α i))] : + is_mul_left_invariant (volume : measure (Π i, α i)) := +pi.is_mul_left_invariant _ + /-! ### Measure preserving equivalences diff --git a/src/measure_theory/group/arithmetic.lean b/src/measure_theory/group/arithmetic.lean index a07a22ca6d1ef..d2eac5cf3a703 100644 --- a/src/measure_theory/group/arithmetic.lean +++ b/src/measure_theory/group/arithmetic.lean @@ -131,6 +131,13 @@ measurable_mul.comp_ae_measurable (hf.prod_mk hg) omit m +@[to_additive] +instance pi.has_measurable_mul {ι : Type*} {α : ι → Type*} [∀ i, has_mul (α i)] + [∀ i, measurable_space (α i)] [∀ i, has_measurable_mul (α i)] : + has_measurable_mul (Π i, α i) := +⟨λ g, measurable_pi_iff.mpr $ λ i, (measurable_const_mul (g i)).comp $ measurable_pi_apply i, + λ g, measurable_pi_iff.mpr $ λ i, (measurable_mul_const (g i)).comp $ measurable_pi_apply i⟩ + @[priority 100, to_additive] instance has_measurable_mul₂.to_has_measurable_mul [has_measurable_mul₂ M] : has_measurable_mul M := diff --git a/src/measure_theory/group/integration.lean b/src/measure_theory/group/integration.lean new file mode 100644 index 0000000000000..7c66efe73983a --- /dev/null +++ b/src/measure_theory/group/integration.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2022 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn +-/ +import measure_theory.integral.bochner +import measure_theory.group.measure + +/-! +# Integration on Groups + +We develop properties of integrals with a group as domain. +This file contains properties about integrability, Lebesgue integration and Bochner integration. +-/ + +namespace measure_theory + +open measure topological_space +open_locale ennreal + +variables {𝕜 G E : Type*} [measurable_space G] {μ : measure G} +variables [normed_group E] [second_countable_topology E] [normed_space ℝ E] [complete_space E] + [measurable_space E] [borel_space E] + +section measurable_mul + +variables [group G] [has_measurable_mul G] + +/-- Translating a function by left-multiplication does not change its `lintegral` with respect to +a left-invariant measure. -/ +@[to_additive] +lemma lintegral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → ℝ≥0∞) (g : G) : + ∫⁻ x, f (g * x) ∂μ = ∫⁻ x, f x ∂μ := +begin + convert (lintegral_map_equiv f $ measurable_equiv.mul_left g).symm, + simp [map_mul_left_eq_self μ g] +end + +/-- Translating a function by right-multiplication does not change its `lintegral` with respect to +a right-invariant measure. -/ +@[to_additive] +lemma lintegral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) : + ∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ := +begin + convert (lintegral_map_equiv f $ measurable_equiv.mul_right g).symm, + simp [map_mul_right_eq_self μ g] +end + +/-- Translating a function by left-multiplication does not change its integral with respect to a +left-invariant measure. -/ +@[to_additive] +lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) : + ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ := +begin + have h_mul : measurable_embedding (λ x, g * x) := + (measurable_equiv.mul_left g).measurable_embedding, + rw [← h_mul.integral_map, map_mul_left_eq_self] +end + +/-- Translating a function by right-multiplication does not change its integral with respect to a +right-invariant measure. -/ +@[to_additive] +lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) : + ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ := +begin + have h_mul : measurable_embedding (λ x, x * g) := + (measurable_equiv.mul_right g).measurable_embedding, + rw [← h_mul.integral_map, map_mul_right_eq_self] +end + +/-- 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] +lemma integral_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] {f : G → E} {g : G} + (hf' : ∀ x, f (g * x) = - f x) : + ∫ x, f x ∂μ = 0 := +by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self] + +/-- If some right-translate of a function negates it, then the integral of the function with respect +to a right-invariant measure is 0. -/ +@[to_additive] +lemma integral_zero_of_mul_right_eq_neg [is_mul_right_invariant μ] {f : G → E} {g : G} + (hf' : ∀ x, f (x * g) = - f x) : + ∫ x, f x ∂μ = 0 := +by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self] + +end measurable_mul + + +section topological_group + +variables [topological_space G] [group G] [topological_group G] [borel_space G] + [is_mul_left_invariant μ] + +/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function + `f` is 0 iff `f` is 0. -/ +@[to_additive] +lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (hμ : μ ≠ 0) + {f : G → ℝ≥0∞} (hf : continuous f) : + ∫⁻ x, f x ∂μ = 0 ↔ f = 0 := +begin + haveI := is_open_pos_measure_of_mul_left_invariant_of_regular hμ, + rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero] +end + +end topological_group + +end measure_theory diff --git a/src/measure_theory/group/basic.lean b/src/measure_theory/group/measure.lean similarity index 91% rename from src/measure_theory/group/basic.lean rename to src/measure_theory/group/measure.lean index f8f39b67da4c5..b2c8b287d8bb0 100644 --- a/src/measure_theory/group/basic.lean +++ b/src/measure_theory/group/measure.lean @@ -3,7 +3,6 @@ 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 measure_theory.integral.lebesgue import measure_theory.measure.regular import measure_theory.group.measurable_equiv import measure_theory.measure.open_pos @@ -13,7 +12,7 @@ import measure_theory.measure.open_pos We develop some properties of measures on (topological) groups -* We define properties on measures: left and right invariant measures. +* We define properties on measures: measures that are left or right invariant w.r.t. multiplication. * We define the measure `μ.inv : A ↦ μ(A⁻¹)` and show that it is right invariant iff `μ` is left invariant. * We define a class `is_haar_measure μ`, requiring that the measure `μ` is left-invariant, finite @@ -259,17 +258,6 @@ lemma measure_lt_top_of_is_compact_of_is_mul_left_invariant' measure_lt_top_of_is_compact_of_is_mul_left_invariant (interior U) is_open_interior hU ((measure_mono (interior_subset)).trans_lt (lt_top_iff_ne_top.2 h)).ne hK -/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function - `f` is 0 iff `f` is 0. -/ -@[to_additive] -lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (hμ : μ ≠ 0) - {f : G → ℝ≥0∞} (hf : continuous f) : - ∫⁻ x, f x ∂μ = 0 ↔ f = 0 := -begin - haveI := is_open_pos_measure_of_mul_left_invariant_of_regular hμ, - rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero] -end - end group section comm_group @@ -287,32 +275,6 @@ instance is_mul_left_invariant.is_mul_right_invariant {μ : measure G} [is_mul_l end comm_group -section integration - -variables [group G] [has_measurable_mul G] {μ : measure G} - -/-- Translating a function by left-multiplication does not change its `lintegral` with respect to -a left-invariant measure. -/ -@[to_additive] -lemma lintegral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → ℝ≥0∞) (g : G) : - ∫⁻ x, f (g * x) ∂μ = ∫⁻ x, f x ∂μ := -begin - convert (lintegral_map_equiv f $ measurable_equiv.mul_left g).symm, - simp [map_mul_left_eq_self μ g] -end - -/-- Translating a function by right-multiplication does not change its `lintegral` with respect to -a right-invariant measure. -/ -@[to_additive] -lemma lintegral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) : - ∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ := -begin - convert (lintegral_map_equiv f $ measurable_equiv.mul_right g).symm, - simp [map_mul_right_eq_self μ g] -end - -end integration - section haar namespace measure diff --git a/src/measure_theory/group/prod.lean b/src/measure_theory/group/prod.lean index d14568da744e7..b685189cb9a2b 100644 --- a/src/measure_theory/group/prod.lean +++ b/src/measure_theory/group/prod.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ import measure_theory.constructions.prod +import measure_theory.group.measure /-! # Measure theory in the product of groups diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean index ca1e12c6ee119..92347ee300bb7 100644 --- a/src/measure_theory/integral/bochner.lean +++ b/src/measure_theory/integral/bochner.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne -/ import measure_theory.integral.set_to_l1 -import measure_theory.group.basic import analysis.normed_space.bounded_linear_maps import topology.sequences @@ -1296,53 +1295,6 @@ calc ∫ x, f x ∂(measure.dirac a) = ∫ x, f a ∂(measure.dirac a) : end properties -section group - -variables {G : Type*} [measurable_space G] [group G] [has_measurable_mul G] -variables {μ : measure G} - -open measure - -/-- Translating a function by left-multiplication does not change its integral with respect to a -left-invariant measure. -/ -@[to_additive] -lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) : - ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ := -begin - have h_mul : measurable_embedding (λ x, g * x) := - (measurable_equiv.mul_left g).measurable_embedding, - rw [← h_mul.integral_map, map_mul_left_eq_self] -end - -/-- Translating a function by right-multiplication does not change its integral with respect to a -right-invariant measure. -/ -@[to_additive] -lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) : - ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ := -begin - have h_mul : measurable_embedding (λ x, x * g) := - (measurable_equiv.mul_right g).measurable_embedding, - rw [← h_mul.integral_map, map_mul_right_eq_self] -end - -/-- 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] -lemma integral_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] {f : G → E} {g : G} - (hf' : ∀ x, f (g * x) = - f x) : - ∫ x, f x ∂μ = 0 := -by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self] - -/-- If some right-translate of a function negates it, then the integral of the function with respect -to a right-invariant measure is 0. -/ -@[to_additive] -lemma integral_zero_of_mul_right_eq_neg [is_mul_right_invariant μ] {f : G → E} {g : G} - (hf' : ∀ x, f (x * g) = - f x) : - ∫ x, f x ∂μ = 0 := -by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self] - -end group - mk_simp_attribute integral_simps "Simp set for integral rules." attribute [integral_simps] integral_neg integral_smul L1.integral_add L1.integral_sub diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean index 24c0a6899878b..e3124fc2374c6 100644 --- a/src/measure_theory/integral/interval_integral.lean +++ b/src/measure_theory/integral/interval_integral.lean @@ -666,7 +666,7 @@ have A : measurable_embedding (λ x, x + d) := calc ∫ x in a..b, f (x + d) = ∫ x in a+d..b+d, f x ∂(measure.map (λ x, x + d) volume) : by simp [interval_integral, A.set_integral_map] -... = ∫ x in a+d..b+d, f x : by rw [real.map_volume_add_right] +... = ∫ x in a+d..b+d, f x : by rw [map_add_right_eq_self] @[simp] lemma integral_comp_add_left (d) : ∫ x in a..b, f (d + x) = ∫ x in d+a..d+b, f x := diff --git a/src/measure_theory/integral/periodic.lean b/src/measure_theory/integral/periodic.lean index 2c2e082911bcb..872c1e3cb38bb 100644 --- a/src/measure_theory/integral/periodic.lean +++ b/src/measure_theory/integral/periodic.lean @@ -40,11 +40,11 @@ begin haveI : encodable (add_subgroup.zmultiples a) := (countable_range _).to_encodable, simp only [interval_integral.integral_of_le, ha.le, le_add_iff_nonneg_right], haveI : vadd_invariant_measure (add_subgroup.zmultiples a) ℝ volume := - ⟨λ c s hs, real.volume_preimage_add_left _ _⟩, + ⟨λ c s hs, measure_preimage_add _ _ _⟩, exact (is_add_fundamental_domain_Ioc ha b).set_integral_eq (is_add_fundamental_domain_Ioc ha c) hf.map_vadd_zmultiples end - + /-- If `f` is a periodic function with period `a`, then its integral over `[b, b + a]` does not depend on `b`. -/ lemma interval_integral_add_eq {f : ℝ → E} {a : ℝ} (hf : periodic f a) diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean index c243f6984cbcc..b9b0f7473a545 100644 --- a/src/measure_theory/measure/haar_lebesgue.lean +++ b/src/measure_theory/measure/haar_lebesgue.lean @@ -59,10 +59,6 @@ open measure topological_space.positive_compacts finite_dimensional ### The Lebesgue measure is a Haar measure on `ℝ` and on `ℝ^ι`. -/ -instance is_add_left_invariant_real_volume : - is_add_left_invariant (volume : measure ℝ) := -⟨by simp [real.map_volume_add_left]⟩ - /-- The Haar measure equals the Lebesgue measure on `ℝ`. -/ lemma add_haar_measure_eq_volume : add_haar_measure Icc01 = volume := by { convert (add_haar_measure_unique volume Icc01).symm, simp [Icc01] } @@ -72,7 +68,7 @@ by { rw ← add_haar_measure_eq_volume, apply_instance } instance is_add_left_invariant_real_volume_pi (ι : Type*) [fintype ι] : is_add_left_invariant (volume : measure (ι → ℝ)) := -⟨by simp [real.map_volume_pi_add_left]⟩ +⟨by simp [map_add_left_eq_self]⟩ /-- The Haar measure equals the Lebesgue measure on `ℝ^ι`. -/ lemma add_haar_measure_eq_volume_pi (ι : Type*) [fintype ι] : diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean index 3f53a0cb0edf0..cdc97f09e7a03 100644 --- a/src/measure_theory/measure/lebesgue.lean +++ b/src/measure_theory/measure/lebesgue.lean @@ -25,7 +25,7 @@ are proved more generally for any additive Haar measure on a finite-dimensional -/ noncomputable theory -open classical set filter measure_theory +open classical set filter measure_theory measure_theory.measure open ennreal (of_real) open_locale big_operators ennreal nnreal topological_space @@ -213,22 +213,10 @@ calc volume s ≤ ∏ i : ι, emetric.diam (function.eval i '' s) : volume_pi_le ### Images of the Lebesgue measure under translation/multiplication in ℝ -/ -lemma map_volume_add_left (a : ℝ) : measure.map ((+) a) volume = volume := -eq.symm $ real.measure_ext_Ioo_rat $ λ p q, - by simp [measure.map_apply (measurable_const_add a) measurable_set_Ioo, sub_sub_sub_cancel_right] - -@[simp] lemma volume_preimage_add_left (a : ℝ) (s : set ℝ) : volume (((+) a) ⁻¹' s) = volume s := -calc volume (((+) a) ⁻¹' s) = measure.map ((+) a) volume s : - ((homeomorph.add_left a).to_measurable_equiv.map_apply s).symm -... = volume s : by rw map_volume_add_left - -lemma map_volume_add_right (a : ℝ) : measure.map (+ a) volume = volume := -by simpa only [add_comm] using real.map_volume_add_left a - -@[simp] lemma volume_preimage_add_right (a : ℝ) (s : set ℝ) : volume ((+ a) ⁻¹' s) = volume s := -calc volume ((+ a) ⁻¹' s) = measure.map (+ a) volume s : - ((homeomorph.add_right a).to_measurable_equiv.map_apply s).symm -... = volume s : by rw map_volume_add_right +instance is_add_left_invariant_real_volume : + is_add_left_invariant (volume : measure ℝ) := +⟨λ a, eq.symm $ real.measure_ext_Ioo_rat $ λ p q, + by simp [measure.map_apply (measurable_const_add a) measurable_set_Ioo, sub_sub_sub_cancel_right]⟩ lemma smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) : ennreal.of_real (|a|) • measure.map ((*) a) volume = volume := @@ -279,21 +267,10 @@ eq.symm $ real.measure_ext_Ioo_rat $ λ p q, ### Images of the Lebesgue measure under translation/linear maps in ℝⁿ -/ -lemma map_volume_pi_add_left (a : ι → ℝ) : measure.map ((+) a) volume = volume := -begin - refine (measure.pi_eq (λ s hs, _)).symm, - have A : has_add.add a ⁻¹' (set.pi univ (λ (i : ι), s i)) - = set.pi univ (λ (i : ι), ((+) (a i)) ⁻¹' (s i)), by { ext, simp }, - rw [measure.map_apply (measurable_const_add a) (measurable_set.univ_pi_fintype hs), A, - volume_pi_pi], - simp only [volume_preimage_add_left] -end - -@[simp] lemma volume_pi_preimage_add_left (a : ι → ℝ) (s : set (ι → ℝ)) : - volume (((+) a) ⁻¹' s) = volume s := -calc volume (((+) a) ⁻¹' s) = measure.map ((+) a) volume s : - ((homeomorph.add_left a).to_measurable_equiv.map_apply s).symm -... = volume s : by rw map_volume_pi_add_left +-- for some reason `apply_instance` doesn't find this +instance is_add_left_invariant_real_volume_pi (ι : Type*) [fintype ι] : + is_add_left_invariant (volume : measure (ι → ℝ)) := +pi.is_add_left_invariant_volume open matrix @@ -364,7 +341,7 @@ begin refine measurable.add (measurable_pi_lambda _ (λ i, measurable.const_mul _ _)) measurable_snd, exact this.comp measurable_fst }, exact measure_preserving.skew_product (measure_preserving.id _) g_meas - (eventually_of_forall (λ a, map_volume_pi_add_left _)) }, + (eventually_of_forall (λ a, map_add_left_eq_self _ _)) }, have C : measure_preserving e.symm volume volume := ⟨ (measurable_pi_equiv_pi_subtype_prod_symm (λ (i : ι), ℝ) p : _), (measure.map_pi_equiv_pi_subtype_prod_symm (λ (i : ι), volume) p : _) ⟩, diff --git a/src/number_theory/liouville/measure.lean b/src/number_theory/liouville/measure.lean index 2290d01f95739..1211eae475035 100644 --- a/src/number_theory/liouville/measure.lean +++ b/src/number_theory/liouville/measure.lean @@ -30,7 +30,7 @@ open filter set metric measure_theory real lemma set_of_liouville_with_subset_aux : {x : ℝ | ∃ p > 2, liouville_with p x} ⊆ - ⋃ m : ℤ, (λ x : ℝ, x + m) ⁻¹' (⋃ n > (0 : ℕ), + ⋃ m : ℤ, (λ x : ℝ, x + m) ⁻¹' (⋃ n > (0 : ℕ), {x : ℝ | ∃ᶠ b : ℕ in at_top, ∃ a ∈ finset.Icc (0 : ℤ) b, |x - (a : ℤ) / b| < 1 / b ^ (2 + 1 / n : ℝ)}) := begin @@ -74,7 +74,7 @@ measure zero. -/ begin simp only [← set_of_exists], refine measure_mono_null set_of_liouville_with_subset_aux _, - rw measure_Union_null_iff, intro m, rw real.volume_preimage_add_right, clear m, + rw measure_Union_null_iff, intro m, rw measure_preimage_add_right, clear m, refine (measure_bUnion_null_iff $ countable_encodable _).2 (λ n (hn : 1 ≤ n), _), generalize hr : (2 + 1 / n : ℝ) = r, replace hr : 2 < r, by simp [← hr, zero_lt_one.trans_le hn], clear hn n,