From f721cdca3b50bbe616dfc291620d51fcc06bfea4 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Tue, 13 Dec 2022 06:33:12 +0000 Subject: [PATCH] feat(measure_theory/measure/haar_lebesgue): Lebesgue measure coming from an alternating map (#17583) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit To an `n`-alternating form `ω` on an `n`-dimensional space, we associate a Lebesgue measure `ω.measure`. We show that it satisfies `ω.measure (parallelepiped v) = |ω v|` when `v` is a family of `n` vectors, where `parallelepiped v` is the parallelepiped spanned by these vectors. In the special case of inner product spaces, this gives a canonical measure when one takes for the alternating form the canonical one associated to some orientation. Therefore, we register a `measure_space` instance on finite-dimensional inner product spaces. As the real line is a special case of inner product space, we need to redefine the Lebesgue measure there to avoid having two competing `measure_space` instances. --- src/analysis/inner_product_space/pi_L2.lean | 14 +- src/analysis/normed/group/basic.lean | 5 + src/linear_algebra/determinant.lean | 4 + src/linear_algebra/finite_dimensional.lean | 9 + src/measure_theory/group/measure.lean | 22 ++- src/measure_theory/measure/haar_lebesgue.lean | 82 ++++++--- src/measure_theory/measure/haar_of_basis.lean | 160 ++++++++++++++++++ src/measure_theory/measure/haar_of_inner.lean | 69 ++++++++ src/measure_theory/measure/lebesgue.lean | 83 ++++----- src/measure_theory/measure/measure_space.lean | 4 + 10 files changed, 384 insertions(+), 68 deletions(-) create mode 100644 src/measure_theory/measure/haar_of_basis.lean create mode 100644 src/measure_theory/measure/haar_of_inner.lean diff --git a/src/analysis/inner_product_space/pi_L2.lean b/src/analysis/inner_product_space/pi_L2.lean index e66ef1bc6a3c0..ab8caa6dc83db 100644 --- a/src/analysis/inner_product_space/pi_L2.lean +++ b/src/analysis/inner_product_space/pi_L2.lean @@ -656,13 +656,25 @@ let ⟨w, hw, hw', hw''⟩ := (orthonormal_empty 𝕜 E).exists_orthonormal_basi ⟨w, hw, hw''⟩ /-- A finite-dimensional `inner_product_space` has an orthonormal basis. -/ -def std_orthonormal_basis : orthonormal_basis (fin (finrank 𝕜 E)) 𝕜 E := +@[irreducible] def std_orthonormal_basis : orthonormal_basis (fin (finrank 𝕜 E)) 𝕜 E := begin let b := classical.some (classical.some_spec $ exists_orthonormal_basis 𝕜 E), rw [finrank_eq_card_basis b.to_basis], exact b.reindex (fintype.equiv_fin_of_card_eq rfl), end +/-- An orthonormal basis of `ℝ` is made either of the vector `1`, or of the vector `-1`. -/ +lemma orthonormal_basis_one_dim (b : orthonormal_basis ι ℝ ℝ) : + ⇑b = (λ _, (1 : ℝ)) ∨ ⇑b = (λ _, (-1 : ℝ)) := +begin + haveI : unique ι, from b.to_basis.unique, + have : b default = 1 ∨ b default = - 1, + { have : ‖b default‖ = 1, from b.orthonormal.1 _, + rwa [real.norm_eq_abs, abs_eq (zero_le_one : (0 : ℝ) ≤ 1)] at this }, + rw eq_const_of_unique b, + refine this.imp _ _; simp, +end + variables {𝕜 E} section subordinate_orthonormal_basis diff --git a/src/analysis/normed/group/basic.lean b/src/analysis/normed/group/basic.lean index 88fc629764a1c..abbeb4e1b952e 100644 --- a/src/analysis/normed/group/basic.lean +++ b/src/analysis/normed/group/basic.lean @@ -1199,9 +1199,14 @@ lemma le_norm_self (r : ℝ) : r ≤ ‖r‖ := le_abs_self r lemma nnnorm_of_nonneg (hr : 0 ≤ r) : ‖r‖₊ = ⟨r, hr⟩ := nnreal.eq $ norm_of_nonneg hr +@[simp] lemma nnnorm_abs (r : ℝ) : ‖(|r|)‖₊ = ‖r‖₊ := by simp [nnnorm] + lemma ennnorm_eq_of_real (hr : 0 ≤ r) : (‖r‖₊ : ℝ≥0∞) = ennreal.of_real r := by { rw [← of_real_norm_eq_coe_nnnorm, norm_of_nonneg hr] } +lemma ennnorm_eq_of_real_abs (r : ℝ) : (‖r‖₊ : ℝ≥0∞) = ennreal.of_real (|r|) := +by rw [← real.nnnorm_abs r, real.ennnorm_eq_of_real (abs_nonneg _)] + lemma to_nnreal_eq_nnnorm_of_nonneg (hr : 0 ≤ r) : r.to_nnreal = ‖r‖₊ := begin rw real.to_nnreal_of_nonneg hr, diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean index 832a3770de7ce..b670bd9a2e843 100644 --- a/src/linear_algebra/determinant.lean +++ b/src/linear_algebra/determinant.lean @@ -208,6 +208,10 @@ by simp [← to_matrix_eq_to_matrix'] linear_map.det (matrix.to_lin b b f) = f.det := by rw [← linear_map.det_to_matrix b, linear_map.to_matrix_to_lin] +@[simp] lemma det_to_lin' (f : matrix ι ι R) : + linear_map.det (f.to_lin') = f.det := +by simp only [← to_lin_eq_to_lin', det_to_lin] + /-- To show `P f.det` it suffices to consider `P (to_matrix _ _ f).det` and `P 1`. -/ @[elab_as_eliminator] lemma det_cases [decidable_eq M] {P : A → Prop} (f : M →ₗ[A] M) diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean index 1b98f9bb85e4c..d0ee8c0ce5983 100644 --- a/src/linear_algebra/finite_dimensional.lean +++ b/src/linear_algebra/finite_dimensional.lean @@ -209,6 +209,15 @@ begin rw [cardinal.mk_fintype, finrank_eq_card_basis h] end +/-- Given a basis of a division ring over itself indexed by a type `ι`, then `ι` is `unique`. -/ +noncomputable def basis.unique {ι : Type*} (b : basis ι K K) : unique ι := +begin + have A : cardinal.mk ι = ↑(finite_dimensional.finrank K K) := + (finite_dimensional.finrank_eq_card_basis' b).symm, + simp only [cardinal.eq_one_iff_unique, finite_dimensional.finrank_self, algebra_map.coe_one] at A, + exact nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 A), +end + variables (K V) /-- A finite dimensional vector space has a basis indexed by `fin (finrank K V)`. -/ diff --git a/src/measure_theory/group/measure.lean b/src/measure_theory/group/measure.lean index f9e58e0ed76a6..b3d09a47c4246 100644 --- a/src/measure_theory/group/measure.lean +++ b/src/measure_theory/group/measure.lean @@ -27,7 +27,7 @@ We also give analogues of all these notions in the additive world. noncomputable theory -open_locale ennreal pointwise big_operators topological_space +open_locale nnreal ennreal pointwise big_operators topological_space open has_inv set function measure_theory.measure filter variables {𝕜 G H : Type*} [measurable_space G] [measurable_space H] @@ -70,14 +70,26 @@ 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 • μ) := +@[to_additive measure_theory.is_add_left_invariant_smul] +instance is_mul_left_invariant_smul [is_mul_left_invariant μ] (c : ℝ≥0∞) : + is_mul_left_invariant (c • μ) := ⟨λ g, by rw [measure.map_smul, map_mul_left_eq_self]⟩ -@[to_additive] -instance [is_mul_right_invariant μ] (c : ℝ≥0∞) : is_mul_right_invariant (c • μ) := +@[to_additive measure_theory.is_add_right_invariant_smul] +instance is_mul_right_invariant_smul [is_mul_right_invariant μ] (c : ℝ≥0∞) : + is_mul_right_invariant (c • μ) := ⟨λ g, by rw [measure.map_smul, map_mul_right_eq_self]⟩ +@[to_additive measure_theory.is_add_left_invariant_smul_nnreal] +instance is_mul_left_invariant_smul_nnreal [is_mul_left_invariant μ] (c : ℝ≥0) : + is_mul_left_invariant (c • μ) := +measure_theory.is_mul_left_invariant_smul (c : ℝ≥0∞) + +@[to_additive measure_theory.is_add_right_invariant_smul_nnreal] +instance is_mul_right_invariant_smul_nnreal [is_mul_right_invariant μ] (c : ℝ≥0) : + is_mul_right_invariant (c • μ) := +measure_theory.is_mul_right_invariant_smul (c : ℝ≥0∞) + section has_measurable_mul variables [has_measurable_mul G] diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean index 6134d647b3f90..b52c0c1122241 100644 --- a/src/measure_theory/measure/haar_lebesgue.lean +++ b/src/measure_theory/measure/haar_lebesgue.lean @@ -30,6 +30,11 @@ We deduce basic properties of any Haar measure on a finite dimensional real vect * `add_haar_closed_ball`: the measure of `closed_ball x r` is `r ^ dim * μ (ball 0 1)`. * `add_haar_sphere`: spheres have zero measure. +This makes it possible to associate a Lebesgue measure to an `n`-alternating map in dimension `n`. +This measure is called `alternating_map.measure`. Its main property is +`ω.measure_parallelepiped v`, stating that the associated measure of the parallelepiped spanned +by vectors `v₁, ..., vₙ` is given by `|ω v|`. + We also show that a Lebesgue density point `x` of a set `s` (with respect to closed balls) has density one for the rescaled copies `{x} + r • t` of a given set `t` with positive measure, in `tendsto_add_haar_inter_smul_one_of_density_one`. In particular, `s` intersects `{x} + r • t` for @@ -67,9 +72,6 @@ open measure topological_space.positive_compacts finite_dimensional lemma add_haar_measure_eq_volume : add_haar_measure Icc01 = volume := by { convert (add_haar_measure_unique volume Icc01).symm, simp [Icc01] } -instance : is_add_haar_measure (volume : measure ℝ) := -by { rw ← add_haar_measure_eq_volume, apply_instance } - /-- The Haar measure equals the Lebesgue measure on `ℝ^ι`. -/ lemma add_haar_measure_eq_volume_pi (ι : Type*) [fintype ι] : add_haar_measure (pi_Icc01 ι) = volume := @@ -201,9 +203,11 @@ begin real.map_linear_map_volume_pi_eq_smul_volume_pi hf, smul_comm], end +variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] + [borel_space E] [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] + {F : Type*} [normed_add_comm_group F] [normed_space ℝ F] [complete_space F] + lemma map_linear_map_add_haar_eq_smul_add_haar - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] {f : E →ₗ[ℝ] E} (hf : f.det ≠ 0) : measure.map f μ = ennreal.of_real (abs (f.det)⁻¹) • μ := begin @@ -237,8 +241,6 @@ end /-- The preimage of a set `s` under a linear map `f` with nonzero determinant has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/ @[simp] lemma add_haar_preimage_linear_map - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] {f : E →ₗ[ℝ] E} (hf : f.det ≠ 0) (s : set E) : μ (f ⁻¹' s) = ennreal.of_real (abs (f.det)⁻¹) * μ s := calc μ (f ⁻¹' s) = measure.map f μ s : @@ -250,8 +252,6 @@ calc μ (f ⁻¹' s) = measure.map f μ s : /-- The preimage of a set `s` under a continuous linear map `f` with nonzero determinant has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/ @[simp] lemma add_haar_preimage_continuous_linear_map - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] {f : E →L[ℝ] E} (hf : linear_map.det (f : E →ₗ[ℝ] E) ≠ 0) (s : set E) : μ (f ⁻¹' s) = ennreal.of_real (abs (linear_map.det (f : E →ₗ[ℝ] E))⁻¹) * μ s := add_haar_preimage_linear_map μ hf s @@ -259,8 +259,6 @@ add_haar_preimage_linear_map μ hf s /-- The preimage of a set `s` under a linear equiv `f` has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/ @[simp] lemma add_haar_preimage_linear_equiv - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] (f : E ≃ₗ[ℝ] E) (s : set E) : μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s := begin @@ -272,8 +270,6 @@ end /-- The preimage of a set `s` under a continuous linear equiv `f` has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/ @[simp] lemma add_haar_preimage_continuous_linear_equiv - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] (f : E ≃L[ℝ] E) (s : set E) : μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s := add_haar_preimage_linear_equiv μ _ s @@ -281,8 +277,6 @@ add_haar_preimage_linear_equiv μ _ s /-- The image of a set `s` under a linear map `f` has measure equal to `μ s` times the absolute value of the determinant of `f`. -/ @[simp] lemma add_haar_image_linear_map - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] (f : E →ₗ[ℝ] E) (s : set E) : μ (f '' s) = ennreal.of_real (abs f.det) * μ s := begin @@ -303,8 +297,6 @@ end /-- The image of a set `s` under a continuous linear map `f` has measure equal to `μ s` times the absolute value of the determinant of `f`. -/ @[simp] lemma add_haar_image_continuous_linear_map - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] (f : E →L[ℝ] E) (s : set E) : μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s := add_haar_image_linear_map μ _ s @@ -312,8 +304,6 @@ add_haar_image_linear_map μ _ s /-- The image of a set `s` under a continuous linear equiv `f` has measure equal to `μ s` times the absolute value of the determinant of `f`. -/ @[simp] lemma add_haar_image_continuous_linear_equiv - {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable_space E] [borel_space E] - [finite_dimensional ℝ E] (μ : measure E) [is_add_haar_measure μ] (f : E ≃L[ℝ] E) (s : set E) : μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s := μ.add_haar_image_linear_map (f : E →ₗ[ℝ] E) s @@ -322,10 +312,6 @@ equal to `μ s` times the absolute value of the determinant of `f`. -/ ### Basic properties of Haar measures on real vector spaces -/ -variables {E : Type*} [normed_add_comm_group E] [measurable_space E] [normed_space ℝ E] - [finite_dimensional ℝ E] [borel_space E] (μ : measure E) [is_add_haar_measure μ] - {F : Type*} [normed_add_comm_group F] [normed_space ℝ F] [complete_space F] - lemma map_add_haar_smul {r : ℝ} (hr : r ≠ 0) : measure.map ((•) r) μ = ennreal.of_real (abs (r ^ (finrank ℝ E))⁻¹) • μ := begin @@ -566,6 +552,56 @@ begin simp only [real.to_nnreal_bit0, real.to_nnreal_one, le_refl], end +section + +/-! +### The Lebesgue measure associated to an alternating map +-/ + +variables {ι G : Type*} [fintype ι] [decidable_eq ι] +[normed_add_comm_group G] [normed_space ℝ G] [measurable_space G] [borel_space G] + +lemma add_haar_parallelepiped (b : basis ι ℝ G) (v : ι → G) : + b.add_haar (parallelepiped v) = ennreal.of_real (|b.det v|) := +begin + haveI : finite_dimensional ℝ G, from finite_dimensional.of_fintype_basis b, + have A : parallelepiped v = (b.constr ℕ v) '' (parallelepiped b), + { rw image_parallelepiped, + congr' 1 with i, + exact (b.constr_basis ℕ v i).symm }, + rw [A, add_haar_image_linear_map, basis.add_haar_self, mul_one, + ← linear_map.det_to_matrix b, ← basis.to_matrix_eq_to_matrix_constr], + refl, +end + +variables [finite_dimensional ℝ G] {n : ℕ} [_i : fact (finrank ℝ G = n)] +include _i + +/-- The Lebesgue measure associated to an alternating map. It gives measure `|ω v|` to the +parallelepiped spanned by the vectors `v₁, ..., vₙ`. Note that it is not always a Haar measure, +as it can be zero, but it is always locally finite and translation invariant. -/ +@[irreducible] noncomputable def _root_.alternating_map.measure + (ω : alternating_map ℝ G ℝ (fin n)) : measure G := +‖ω (fin_basis_of_finrank_eq ℝ G _i.out)‖₊ • (fin_basis_of_finrank_eq ℝ G _i.out).add_haar + +lemma _root_.alternating_map.measure_parallelepiped + (ω : alternating_map ℝ G ℝ (fin n)) (v : fin n → G) : + ω.measure (parallelepiped v) = ennreal.of_real (|ω v|) := +begin + conv_rhs { rw ω.eq_smul_basis_det (fin_basis_of_finrank_eq ℝ G _i.out) }, + simp only [add_haar_parallelepiped, alternating_map.measure, coe_nnreal_smul_apply, + alternating_map.smul_apply, algebra.id.smul_eq_mul, abs_mul, + ennreal.of_real_mul (abs_nonneg _), real.ennnorm_eq_of_real_abs] +end + +instance (ω : alternating_map ℝ G ℝ (fin n)) : is_add_left_invariant ω.measure := +by { rw [alternating_map.measure], apply_instance } + +instance (ω : alternating_map ℝ G ℝ (fin n)) : is_locally_finite_measure ω.measure := +by { rw [alternating_map.measure], apply_instance } + +end + /-! ### Density points diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean new file mode 100644 index 0000000000000..e8da34d00525d --- /dev/null +++ b/src/measure_theory/measure/haar_of_basis.lean @@ -0,0 +1,160 @@ +/- +Copyright (c) 2022 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sébastien Gouëzel +-/ +import measure_theory.measure.haar +import analysis.inner_product_space.pi_L2 + +/-! +# Additive Haar measure constructed from a basis + +Given a basis of a finite-dimensional real vector space, we define the corresponding Lebesgue +measure, which gives measure `1` to the parallelepiped spanned by the basis. + +## Main definitions + +* `parallelepiped v` is the parallelepiped spanned by a finite family of vectors. +* `basis.parallelepiped` is the parallelepiped associated to a basis, seen as a compact set with +nonempty interior. +* `basis.add_haar` is the Lebesgue measure associated to a basis, giving measure `1` to the +corresponding parallelepiped. + +In particular, we declare a `measure_space` instance on any finite-dimensional inner product space, +by using the Lebesgue measure associated to some orthonormal basis (which is in fact independent +of the basis). +-/ + +open set topological_space measure_theory measure_theory.measure finite_dimensional +open_locale big_operators + +noncomputable theory + +variables {ι ι' E F : Type*} [fintype ι] [fintype ι'] + +section add_comm_group + +variables [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] + +/-- The closed parallelepiped spanned by a finite family of vectors. -/ +def parallelepiped (v : ι → E) : set E := +(λ (t : ι → ℝ), ∑ i, t i • v i) '' (Icc 0 1) + +lemma mem_parallelepiped_iff (v : ι → E) (x : E) : + x ∈ parallelepiped v ↔ ∃ (t : ι → ℝ) (ht : t ∈ Icc (0 : ι → ℝ) 1), x = ∑ i, t i • v i := +by simp [parallelepiped, eq_comm] + +lemma image_parallelepiped (f : E →ₗ[ℝ] F) (v : ι → E) : + f '' (parallelepiped v) = parallelepiped (f ∘ v) := +begin + simp only [parallelepiped, ← image_comp], + congr' 1 with t, + simp only [function.comp_app, linear_map.map_sum, linear_map.map_smulₛₗ, ring_hom.id_apply], +end + +/-- Reindexing a family of vectors does not change their parallelepiped. -/ +@[simp] lemma parallelepiped_comp_equiv (v : ι → E) (e : ι' ≃ ι) : + parallelepiped (v ∘ e) = parallelepiped v := +begin + simp only [parallelepiped], + let K : (ι' → ℝ) ≃ (ι → ℝ) := equiv.Pi_congr_left' (λ (a : ι'), ℝ) e, + have : Icc (0 : (ι → ℝ)) 1 = K '' (Icc (0 : (ι' → ℝ)) 1), + { rw ← equiv.preimage_eq_iff_eq_image, + ext x, + simp only [mem_preimage, mem_Icc, pi.le_def, pi.zero_apply, equiv.Pi_congr_left'_apply, + pi.one_apply], + refine ⟨λ h, ⟨λ i, _, λ i, _⟩, λ h, ⟨λ i, h.1 (e.symm i), λ i, h.2 (e.symm i)⟩⟩, + { simpa only [equiv.symm_apply_apply] using h.1 (e i) }, + { simpa only [equiv.symm_apply_apply] using h.2 (e i) } }, + rw [this, ← image_comp], + congr' 1 with x, + simpa only [orthonormal_basis.coe_reindex, function.comp_app, equiv.symm_apply_apply, + equiv.Pi_congr_left'_apply, equiv.apply_symm_apply] + using (e.symm.sum_comp (λ (i : ι'), x i • v (e i))).symm, +end + +/- The parallelepiped associated to an orthonormal basis of `ℝ` is either `[0, 1]` or `[-1, 0]`. -/ +lemma parallelepiped_orthonormal_basis_one_dim (b : orthonormal_basis ι ℝ ℝ) : + parallelepiped b = Icc 0 1 ∨ parallelepiped b = Icc (-1) 0 := +begin + have e : ι ≃ fin 1, + { apply fintype.equiv_fin_of_card_eq, + simp only [← finrank_eq_card_basis b.to_basis, finrank_self] }, + have B : parallelepiped (b.reindex e) = parallelepiped b, + { convert parallelepiped_comp_equiv b e.symm, + ext i, + simp only [orthonormal_basis.coe_reindex] }, + rw ← B, + let F : ℝ → (fin 1 → ℝ) := λ t, (λ i, t), + have A : Icc (0 : fin 1 → ℝ) 1 = F '' (Icc (0 : ℝ) 1), + { apply subset.antisymm, + { assume x hx, + refine ⟨x 0, ⟨hx.1 0, hx.2 0⟩, _⟩, + ext j, + simp only [subsingleton.elim j 0] }, + { rintros x ⟨y, hy, rfl⟩, + exact ⟨λ j, hy.1, λ j, hy.2⟩ } }, + rcases orthonormal_basis_one_dim (b.reindex e) with H|H, + { left, + simp only [H, parallelepiped, algebra.id.smul_eq_mul, mul_one, A, + finset.sum_singleton, ←image_comp, image_id', finset.univ_unique], }, + { right, + simp only [H, parallelepiped, algebra.id.smul_eq_mul, mul_one], + rw A, + simp only [←image_comp, mul_neg, mul_one, finset.sum_singleton, image_neg, preimage_neg_Icc, + neg_zero, finset.univ_unique] }, +end + +end add_comm_group + +section normed_space + +variables [normed_add_comm_group E] [normed_space ℝ E] + +/-- The parallelepiped spanned by a basis, as a compact set with nonempty interior. -/ +def basis.parallelepiped (b : basis ι ℝ E) : positive_compacts E := +{ carrier := parallelepiped b, + is_compact' := is_compact_Icc.image (continuous_finset_sum finset.univ + (λ (i : ι) (H : i ∈ finset.univ), (continuous_apply i).smul continuous_const)), + interior_nonempty' := + begin + suffices H : set.nonempty (interior (b.equiv_funL.symm.to_homeomorph '' (Icc 0 1))), + { dsimp only [parallelepiped], + convert H, + ext t, + exact (b.equiv_fun_symm_apply t).symm }, + have A : set.nonempty (interior (Icc (0 : ι → ℝ) 1)), + { rw [← pi_univ_Icc, interior_pi_set (@finite_univ ι _)], + simp only [univ_pi_nonempty_iff, pi.zero_apply, pi.one_apply, interior_Icc, nonempty_Ioo, + zero_lt_one, implies_true_iff] }, + rwa [← homeomorph.image_interior, nonempty_image_iff], + end } + +variables [measurable_space E] [borel_space E] + +/-- The Lebesgue measure associated to a basis, giving measure `1` to the parallelepiped spanned +by the basis. -/ +@[irreducible] def basis.add_haar (b : basis ι ℝ E) : measure E := +measure.add_haar_measure b.parallelepiped + +instance is_add_haar_measure_basis_add_haar (b : basis ι ℝ E) : + is_add_haar_measure b.add_haar := +by { rw basis.add_haar, exact measure.is_add_haar_measure_add_haar_measure _ } + +lemma basis.add_haar_self (b : basis ι ℝ E) : b.add_haar (parallelepiped b) = 1 := +by { rw [basis.add_haar], exact add_haar_measure_self } + +end normed_space + +/-- A finite dimensional inner product space has a canonical measure, the Lebesgue measure giving +volume `1` to the parallelepiped spanned by any orthonormal basis. We define the measure using +some arbitrary choice of orthonormal basis. The fact that it works with any orthonormal basis +is proved in `orthonormal_basis.volume_parallelepiped`. -/ +@[priority 100] instance measure_space_of_inner_product_space + [inner_product_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] : + measure_space E := +{ volume := (std_orthonormal_basis ℝ E).to_basis.add_haar } + +/- This instance should not be necessary, but Lean has difficulties to find it in product +situations if we do not declare it explicitly. -/ +instance real.measure_space : measure_space ℝ := by apply_instance diff --git a/src/measure_theory/measure/haar_of_inner.lean b/src/measure_theory/measure/haar_of_inner.lean new file mode 100644 index 0000000000000..b10f73db4734b --- /dev/null +++ b/src/measure_theory/measure/haar_of_inner.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2022 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sébastien Gouëzel +-/ +import analysis.inner_product_space.orientation +import measure_theory.measure.haar_lebesgue + +/-! +# Volume forms and measures on inner product spaces + +A volume form induces a Lebesgue measure on general finite-dimensional real vector spaces. In this +file, we discuss the specific situation of inner product spaces, where an orientation gives +rise to a canonical volume form. We show that the measure coming from this volume form gives +measure `1` to the parallelepiped spanned by any orthonormal basis, and that it coincides with +the canonical `volume` from the `measure_space` instance. +-/ + +open finite_dimensional measure_theory measure_theory.measure set + +variables {ι F : Type*} [fintype ι] [inner_product_space ℝ F] [finite_dimensional ℝ F] +[measurable_space F] [borel_space F] + +section + +variables {m n : ℕ} [_i : fact (finrank ℝ F = n)] +include _i + +/-- The volume form coming from an orientation in an inner product space gives measure `1` to the +parallelepiped associated to any orthonormal basis. This is a rephrasing of +`abs_volume_form_apply_of_orthonormal` in terms of measures. -/ +lemma orientation.measure_orthonormal_basis + (o : orientation ℝ F (fin n)) (b : orthonormal_basis ι ℝ F) : + o.volume_form.measure (parallelepiped b) = 1 := +begin + have e : ι ≃ fin n, + { refine fintype.equiv_fin_of_card_eq _, + rw [← _i.out, finrank_eq_card_basis b.to_basis] }, + have A : ⇑b = (b.reindex e) ∘ e, + { ext x, + simp only [orthonormal_basis.coe_reindex, function.comp_app, equiv.symm_apply_apply] }, + rw [A, parallelepiped_comp_equiv, alternating_map.measure_parallelepiped, + o.abs_volume_form_apply_of_orthonormal, ennreal.of_real_one], +end + +/-- In an oriented inner product space, the measure coming from the canonical volume form +associated to an orientation coincides with the volume. -/ +lemma orientation.measure_eq_volume (o : orientation ℝ F (fin n)) : + o.volume_form.measure = volume := +begin + have A : o.volume_form.measure ((std_orthonormal_basis ℝ F).to_basis.parallelepiped) = 1, + from orientation.measure_orthonormal_basis o (std_orthonormal_basis ℝ F), + rw [add_haar_measure_unique o.volume_form.measure + ((std_orthonormal_basis ℝ F).to_basis.parallelepiped), A, one_smul], + simp only [volume, basis.add_haar], +end + +end + +/-- The volume measure in a finite-dimensional inner product space gives measure `1` to the +parallelepiped spanned by any orthonormal basis. -/ +lemma orthonormal_basis.volume_parallelepiped (b : orthonormal_basis ι ℝ F) : + volume (parallelepiped b) = 1 := +begin + haveI : fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩, + let o := (std_orthonormal_basis ℝ F).to_basis.orientation, + rw ← o.measure_eq_volume, + exact o.measure_orthonormal_basis b, +end diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean index 71aca319c9d00..96f968b6af59a 100644 --- a/src/measure_theory/measure/lebesgue.lean +++ b/src/measure_theory/measure/lebesgue.lean @@ -9,13 +9,15 @@ import linear_algebra.matrix.diagonal import linear_algebra.matrix.transvection import measure_theory.constructions.pi import measure_theory.measure.stieltjes +import measure_theory.measure.haar_of_basis /-! # Lebesgue measure on the real line and on `ℝⁿ` -We construct Lebesgue measure on the real line, as a particular case of Stieltjes measure associated -to the function `x ↦ x`. We obtain as a consequence Lebesgue measure on `ℝⁿ`. We prove that they -are translation invariant. +We show that the Lebesgue measure on the real line (constructed as a particular case of additive +Haar measure on inner product spaces) coincides with the Stieltjes measure associated +to the function `x ↦ x`. We deduce properties of this measure on `ℝ`, and then of the product +Lebesgue measure on `ℝⁿ`. In particular, we prove that they are translation invariant. We show that, on `ℝⁿ`, a linear map acts on Lebesgue measure by rescaling it through the absolute value of its determinant, in `real.map_linear_map_volume_pi_eq_smul_volume_pi`. @@ -33,17 +35,31 @@ open_locale big_operators ennreal nnreal topological_space ### Definition of the Lebesgue measure and lengths of intervals -/ -/-- Lebesgue measure on the Borel sigma algebra, giving measure `b - a` to the interval `[a, b]`. -/ -instance real.measure_space : measure_space ℝ := -⟨stieltjes_function.id.measure⟩ - namespace real variables {ι : Type*} [fintype ι] -open_locale topological_space +/-- The volume on the real line (as a particular case of the volume on a finite-dimensional +inner product space) coincides with the Stieltjes measure coming from the identity function. -/ +lemma volume_eq_stieltjes_id : (volume : measure ℝ) = stieltjes_function.id.measure := +begin + haveI : is_add_left_invariant stieltjes_function.id.measure := + ⟨λ a, eq.symm $ real.measure_ext_Ioo_rat $ λ p q, + by simp only [measure.map_apply (measurable_const_add a) measurable_set_Ioo, + sub_sub_sub_cancel_right, stieltjes_function.measure_Ioo, stieltjes_function.id_left_lim, + stieltjes_function.id_apply, id.def, preimage_const_add_Ioo]⟩, + have A : stieltjes_function.id.measure (std_orthonormal_basis ℝ ℝ).to_basis.parallelepiped = 1, + { change stieltjes_function.id.measure (parallelepiped (std_orthonormal_basis ℝ ℝ)) = 1, + rcases parallelepiped_orthonormal_basis_one_dim (std_orthonormal_basis ℝ ℝ) with H|H; + simp only [H, stieltjes_function.measure_Icc, stieltjes_function.id_apply, id.def, tsub_zero, + stieltjes_function.id_left_lim, sub_neg_eq_add, zero_add, ennreal.of_real_one] }, + conv_rhs { rw [add_haar_measure_unique stieltjes_function.id.measure + (std_orthonormal_basis ℝ ℝ).to_basis.parallelepiped, A] }, + simp only [volume, basis.add_haar, one_smul], +end -theorem volume_val (s) : volume s = stieltjes_function.id.measure s := rfl +theorem volume_val (s) : volume s = stieltjes_function.id.measure s := +by simp [volume_eq_stieltjes_id] @[simp] lemma volume_Ico {a b : ℝ} : volume (Ico a b) = of_real (b - a) := by simp [volume_val] @@ -132,6 +148,23 @@ instance is_finite_measure_restrict_Ioc (x y : ℝ) : is_finite_measure (volume. instance is_finite_measure_restrict_Ioo (x y : ℝ) : is_finite_measure (volume.restrict (Ioo x y)) := ⟨by simp⟩ +lemma volume_le_diam (s : set ℝ) : volume s ≤ emetric.diam s := +begin + by_cases hs : metric.bounded s, + { rw [real.ediam_eq hs, ← volume_Icc], + exact volume.mono (real.subset_Icc_Inf_Sup_of_bounded hs) }, + { rw metric.ediam_of_unbounded hs, exact le_top } +end + +lemma _root_.filter.eventually.volume_pos_of_nhds_real + {p : ℝ → Prop} {a : ℝ} (h : ∀ᶠ x in 𝓝 a, p x) : + (0 : ℝ≥0∞) < volume {x | p x} := +begin + rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩, + refine lt_of_lt_of_le _ (measure_mono hs), + simpa [-mem_Ioo] using hx.1.trans hx.2 +end + /-! ### Volume of a box in `ℝⁿ` -/ @@ -184,14 +217,6 @@ begin exact (ennreal.of_real_pow (mul_nonneg zero_le_two hr) _).symm end -lemma volume_le_diam (s : set ℝ) : volume s ≤ emetric.diam s := -begin - by_cases hs : metric.bounded s, - { rw [real.ediam_eq hs, ← volume_Icc], - exact volume.mono (real.subset_Icc_Inf_Sup_of_bounded hs) }, - { rw metric.ediam_of_unbounded hs, exact le_top } -end - lemma volume_pi_le_prod_diam (s : set (ι → ℝ)) : volume s ≤ ∏ i : ι, emetric.diam (function.eval i '' s) := calc volume s ≤ volume (pi univ (λ i, closure (function.eval i '' s))) : @@ -210,14 +235,9 @@ calc volume s ≤ ∏ i : ι, emetric.diam (function.eval i '' s) : volume_pi_le by simp only [ennreal.coe_one, one_mul, finset.prod_const, fintype.card] /-! -### Images of the Lebesgue measure under translation/multiplication in ℝ +### Images of the Lebesgue measure under multiplication in ℝ -/ -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 := begin @@ -258,10 +278,6 @@ calc volume ((* a) ⁻¹' s) = measure.map (* a) volume s : ((homeomorph.mul_right₀ a h).to_measurable_equiv.map_apply s).symm ... = ennreal.of_real (abs a⁻¹) * volume s : by { rw map_volume_mul_right h, refl } -instance : is_neg_invariant (volume : measure ℝ) := -⟨eq.symm $ real.measure_ext_Ioo_rat $ λ p q, by simp [show volume.neg (Ioo (p : ℝ) q) = _, - from measure.map_apply measurable_neg measurable_set_Ioo]⟩ - /-! ### Images of the Lebesgue measure under translation/linear maps in ℝⁿ -/ @@ -376,20 +392,8 @@ end end real -open_locale topological_space - -lemma filter.eventually.volume_pos_of_nhds_real {p : ℝ → Prop} {a : ℝ} (h : ∀ᶠ x in 𝓝 a, p x) : - (0 : ℝ≥0∞) < volume {x | p x} := -begin - rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩, - refine lt_of_lt_of_le _ (measure_mono hs), - simpa [-mem_Ioo] using hx.1.trans hx.2 -end - section region_between -open_locale classical - variable {α : Type*} /-- The region between two real-valued functions on an arbitrary set. -/ @@ -457,6 +461,7 @@ theorem volume_region_between_eq_lintegral' (hf : measurable f) (hg : measurable g) (hs : measurable_set s) : μ.prod volume (region_between f g s) = ∫⁻ y in s, ennreal.of_real ((g - f) y) ∂μ := begin + classical, rw measure.prod_apply, { have h : (λ x, volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator (λ x, ennreal.of_real (g x - f x)), diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index ef343796071df..82ab393b11391 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -1022,6 +1022,10 @@ begin simp [map_of_not_ae_measurable hf, map_of_not_ae_measurable hfc] } end +@[simp] protected lemma map_smul_nnreal (c : ℝ≥0) (μ : measure α) (f : α → β) : + (c • μ).map f = c • μ.map f := +μ.map_smul (c : ℝ≥0∞) f + /-- We can evaluate the pushforward on measurable sets. For non-measurable sets, see `measure_theory.measure.le_map_apply` and `measurable_equiv.map_apply`. -/ @[simp] theorem map_apply_of_ae_measurable