feat(measure_theory/measure/haar_lebesgue): Lebesgue measure coming f…

…rom an alternating map (#17583)

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

@@ -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

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,

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)

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)`. -/

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]

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,17 +252,13 @@ 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
 
 /-- 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,17 +270,13 @@ 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
 
 /-- 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,17 +297,13 @@ 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
 
 /-- 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