feat(measure_theory/lebesgue_measure): volume of a box in ℝⁿ (#5635)

src/data/real/ennreal.lean

@@ -357,9 +357,10 @@ lemma zero_lt_coe_iff : 0 < (↑p : ennreal) ↔ 0 < p := coe_lt_coe
 @[simp, norm_cast] lemma coe_le_one_iff : ↑r ≤ (1:ennreal) ↔ r ≤ 1 := coe_le_coe
 @[simp, norm_cast] lemma coe_lt_one_iff : (↑p : ennreal) < 1 ↔ p < 1 := coe_lt_coe
 @[simp, norm_cast] lemma one_lt_coe_iff : 1 < (↑p : ennreal) ↔ 1 < p := coe_lt_coe
-@[simp, norm_cast] lemma coe_nat (n : nat) : ((n : ℝ≥0) : ennreal) = n := with_top.coe_nat n
-@[simp] lemma nat_ne_top (n : nat) : (n : ennreal) ≠ ∞ := with_top.nat_ne_top n
-@[simp] lemma top_ne_nat (n : nat) : ∞ ≠ n := with_top.top_ne_nat n
+@[simp, norm_cast] lemma coe_nat (n : ℕ) : ((n : ℝ≥0) : ennreal) = n := with_top.coe_nat n
+@[simp] lemma of_real_coe_nat (n : ℕ) : ennreal.of_real n = n := by simp [ennreal.of_real]
+@[simp] lemma nat_ne_top (n : ℕ) : (n : ennreal) ≠ ∞ := with_top.nat_ne_top n
+@[simp] lemma top_ne_nat (n : ℕ) : ∞ ≠ n := with_top.top_ne_nat n
 @[simp] lemma one_lt_top : 1 < ∞ := coe_lt_top
 
 lemma le_coe_iff : a ≤ ↑r ↔ (∃p:ℝ≥0, a = p ∧ p ≤ r) := with_top.le_coe_iff

src/data/real/nnreal.lean

@@ -187,6 +187,12 @@ protected lemma of_real_mono : monotone nnreal.of_real :=
 @[simp] lemma of_real_coe {r : ℝ≥0} : nnreal.of_real r = r :=
 nnreal.eq $ max_eq_left r.2
 
+@[simp] lemma mk_coe_nat (n : ℕ) : @eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ≥0) n :=
+nnreal.eq (nnreal.coe_nat_cast n).symm
+
+@[simp] lemma of_real_coe_nat (n : ℕ) : nnreal.of_real n = n :=
+nnreal.eq $ by simp [coe_of_real]
+
 /-- `nnreal.of_real` and `coe : ℝ≥0 → ℝ` form a Galois insertion. -/
 protected def gi : galois_insertion nnreal.of_real coe :=
 galois_insertion.monotone_intro nnreal.coe_mono nnreal.of_real_mono

src/measure_theory/lebesgue_measure.lean

@@ -1,22 +1,25 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl
+Authors: Johannes Hölzl, Yury Kudryashov
 -/
-import measure_theory.measure_space
-import measure_theory.borel_space
+import measure_theory.pi
 
 /-!
-# Lebesgue measure on the real line
+# Lebesgue measure on the real line and on `ℝⁿ`
 -/
 
 noncomputable theory
 open classical set filter
 open ennreal (of_real)
-open_locale big_operators
+open_locale big_operators ennreal
 
 namespace measure_theory
 
+/-!
+### Preliminary definitions
+-/
+
 /-- Length of an interval. This is the largest monotonic function which correctly
   measures all intervals. -/
 def lebesgue_length (s : set ℝ) : ennreal := ⨅a b (h : s ⊆ Ico a b), of_real (b - a)
@@ -215,6 +218,10 @@ begin
   simp [is_lebesgue_measurable_Iio] { contextual := tt }
 end
 
+/-!
+### Definition of the Lebesgue measure and lengths of intervals
+-/
+
 /-- Lebesgue measure on the Borel sets
 
 The outer Lebesgue measure is the completion of this measure. (TODO: proof this)
@@ -234,6 +241,8 @@ open measure_theory
 
 namespace real
 
+variables {ι : Type*} [fintype ι]
+
 open_locale topological_space
 
 theorem volume_val (s) : volume s = lebesgue_outer s := rfl
@@ -254,11 +263,70 @@ instance has_no_atoms_volume : has_no_atoms (volume : measure ℝ) :=
 @[simp] lemma volume_interval {a b : ℝ} : volume (interval a b) = of_real (abs (b - a)) :=
 by rw [interval, volume_Icc, max_sub_min_eq_abs]
 
+@[simp] lemma volume_Ioi {a : ℝ} : volume (Ioi a) = ∞ :=
+top_unique $ le_of_tendsto' ennreal.tendsto_nat_nhds_top $ λ n,
+calc (n : ennreal) = volume (Ioo a (a + n)) : by simp
+... ≤ volume (Ioi a) : measure_mono Ioo_subset_Ioi_self
+
+@[simp] lemma volume_Ici {a : ℝ} : volume (Ici a) = ∞ :=
+by simp [← measure_congr Ioi_ae_eq_Ici]
+
+@[simp] lemma volume_Iio {a : ℝ} : volume (Iio a) = ∞ :=
+top_unique $ le_of_tendsto' ennreal.tendsto_nat_nhds_top $ λ n,
+calc (n : ennreal) = volume (Ioo (a - n) a) : by simp
+... ≤ volume (Iio a) : measure_mono Ioo_subset_Iio_self
+
+@[simp] lemma volume_Iic {a : ℝ} : volume (Iic a) = ∞ :=
+by simp [← measure_congr Iio_ae_eq_Iic]
+
 instance locally_finite_volume : locally_finite_measure (volume : measure ℝ) :=
 ⟨λ x, ⟨Ioo (x - 1) (x + 1),
   mem_nhds_sets is_open_Ioo ⟨sub_lt_self _ zero_lt_one, lt_add_of_pos_right _ zero_lt_one⟩,
   by simp only [real.volume_Ioo, ennreal.of_real_lt_top]⟩⟩
 
+/-!
+### Volume of a box in `ℝⁿ`
+-/
+
+lemma volume_Icc_pi {a b : ι → ℝ} : volume (Icc a b) = ∏ i, ennreal.of_real (b i - a i) :=
+begin
+  rw [← pi_univ_Icc, volume_pi_pi],
+  { simp only [real.volume_Icc] },
+  { exact λ i, is_measurable_Icc }
+end
+
+@[simp] lemma volume_Icc_pi_to_real {a b : ι → ℝ} (h : a ≤ b) :
+  (volume (Icc a b)).to_real = ∏ i, (b i - a i) :=
+by simp only [volume_Icc_pi, ennreal.to_real_prod, ennreal.to_real_of_real (sub_nonneg.2 (h _))]
+
+lemma volume_pi_Ioo {a b : ι → ℝ} :
+  volume (pi univ (λ i, Ioo (a i) (b i))) = ∏ i, ennreal.of_real (b i - a i) :=
+(measure_congr measure.univ_pi_Ioo_ae_eq_Icc).trans volume_Icc_pi
+
+@[simp] lemma volume_pi_Ioo_to_real {a b : ι → ℝ} (h : a ≤ b) :
+  (volume (pi univ (λ i, Ioo (a i) (b i)))).to_real = ∏ i, (b i - a i) :=
+by simp only [volume_pi_Ioo, ennreal.to_real_prod, ennreal.to_real_of_real (sub_nonneg.2 (h _))]
+
+lemma volume_pi_Ioc {a b : ι → ℝ} :
+  volume (pi univ (λ i, Ioc (a i) (b i))) = ∏ i, ennreal.of_real (b i - a i) :=
+(measure_congr measure.univ_pi_Ioc_ae_eq_Icc).trans volume_Icc_pi
+
+@[simp] lemma volume_pi_Ioc_to_real {a b : ι → ℝ} (h : a ≤ b) :
+  (volume (pi univ (λ i, Ioc (a i) (b i)))).to_real = ∏ i, (b i - a i) :=
+by simp only [volume_pi_Ioc, ennreal.to_real_prod, ennreal.to_real_of_real (sub_nonneg.2 (h _))]
+
+lemma volume_pi_Ico {a b : ι → ℝ} :
+  volume (pi univ (λ i, Ico (a i) (b i))) = ∏ i, ennreal.of_real (b i - a i) :=
+(measure_congr measure.univ_pi_Ico_ae_eq_Icc).trans volume_Icc_pi
+
+@[simp] lemma volume_pi_Ico_to_real {a b : ι → ℝ} (h : a ≤ b) :
+  (volume (pi univ (λ i, Ico (a i) (b i)))).to_real = ∏ i, (b i - a i) :=
+by simp only [volume_pi_Ico, ennreal.to_real_prod, ennreal.to_real_of_real (sub_nonneg.2 (h _))]
+
+/-!
+### Images of the Lebesgue measure under translation/multiplication/...
+-/
+
 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_add_left a) is_measurable_Ioo, sub_sub_sub_cancel_right]

src/measure_theory/pi.lean

@@ -357,11 +357,11 @@ end measure
 instance measure_space.pi [Π i, measure_space (α i)] : measure_space (Π i, α i) :=
 ⟨measure.pi (λ i, volume)⟩
 
-lemma measure_space.pi_def [Π i, measure_space (α i)] :
+lemma volume_pi [Π i, measure_space (α i)] :
   (volume : measure (Π i, α i)) = measure.pi (λ i, volume) :=
 rfl
 
-lemma volume_pi [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
+lemma volume_pi_pi [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
   (s : Π i, set (α i)) (hs : ∀ i, is_measurable (s i)) :
   volume (pi univ s) = ∏ i, volume (s i) :=
 measure.pi_pi (λ i, volume) s hs