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, 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.
More properties of the Lebesgue measure are deduced from this in haar_lebesgue.lean, where they
are proved more generally for any additive Haar measure on a finite-dimensional real vector space.
Definition of the Lebesgue measure and lengths of intervals #
@[protected, instance]
Lebesgue measure on the Borel sigma algebra, giving measure b - a to the interval [a, b].
Equations
@[simp]
theorem
real.volume_Ico
{a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Ico a b) = ennreal.of_real (b - a)
@[simp]
theorem
real.volume_Icc
{a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Icc a b) = ennreal.of_real (b - a)
@[simp]
theorem
real.volume_Ioo
{a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Ioo a b) = ennreal.of_real (b - a)
@[simp]
theorem
real.volume_Ioc
{a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Ioc a b) = ennreal.of_real (b - a)
@[simp]
theorem
real.volume_ball
(a r : ℝ) :
⇑measure_theory.measure_space.volume (metric.ball a r) = ennreal.of_real (2 * r)
@[simp]
@[simp]
theorem
real.volume_emetric_ball
(a : ℝ)
(r : ennreal) :
⇑measure_theory.measure_space.volume (emetric.ball a r) = 2 * r
@[simp]
@[protected, instance]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Volume of a box in ℝⁿ #
theorem
real.volume_Icc_pi
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ} :
⇑measure_theory.measure_space.volume (set.Icc a b) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem
real.volume_Icc_pi_to_real
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ}
(h : a ≤ b) :
(⇑measure_theory.measure_space.volume (set.Icc a b)).to_real = finset.univ.prod (λ (i : ι), b i - a i)
theorem
real.volume_pi_Ioo
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ} :
⇑measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioo (a i) (b i))) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem
real.volume_pi_Ioo_to_real
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ}
(h : a ≤ b) :
(⇑measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioo (a i) (b i)))).to_real = finset.univ.prod (λ (i : ι), b i - a i)
theorem
real.volume_pi_Ioc
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ} :
⇑measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioc (a i) (b i))) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem
real.volume_pi_Ioc_to_real
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ}
(h : a ≤ b) :
(⇑measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioc (a i) (b i)))).to_real = finset.univ.prod (λ (i : ι), b i - a i)
theorem
real.volume_pi_Ico
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ} :
⇑measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ico (a i) (b i))) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem
real.volume_pi_Ico_to_real
{ι : Type u_1}
[fintype ι]
{a b : ι → ℝ}
(h : a ≤ b) :
(⇑measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ico (a i) (b i)))).to_real = finset.univ.prod (λ (i : ι), b i - a i)
@[simp]
theorem
real.volume_pi_ball
{ι : Type u_1}
[fintype ι]
(a : ι → ℝ)
{r : ℝ}
(hr : 0 < r) :
⇑measure_theory.measure_space.volume (metric.ball a r) = ennreal.of_real ((2 * r) ^ fintype.card ι)
@[simp]
theorem
real.volume_pi_closed_ball
{ι : Type u_1}
[fintype ι]
(a : ι → ℝ)
{r : ℝ}
(hr : 0 ≤ r) :
⇑measure_theory.measure_space.volume (metric.closed_ball a r) = ennreal.of_real ((2 * r) ^ fintype.card ι)
theorem
real.volume_pi_le_prod_diam
{ι : Type u_1}
[fintype ι]
(s : set (ι → ℝ)) :
⇑measure_theory.measure_space.volume s ≤ finset.univ.prod (λ (i : ι), emetric.diam (function.eval i '' s))
Images of the Lebesgue measure under translation/multiplication in ℝ #
@[protected, instance]
@[simp]
@[simp]
theorem
real.volume_preimage_mul_right
{a : ℝ}
(h : a ≠ 0)
(s : set ℝ) :
⇑measure_theory.measure_space.volume ((λ (_x : ℝ), _x * a) ⁻¹' s) = ennreal.of_real |a⁻¹| * ⇑measure_theory.measure_space.volume s
Images of the Lebesgue measure under translation/linear maps in ℝⁿ #
theorem
real.smul_map_diagonal_volume_pi
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
{D : ι → ℝ}
(h : (matrix.diagonal D).det ≠ 0) :
A diagonal matrix rescales Lebesgue according to its determinant. This is a special case of
real.map_matrix_volume_pi_eq_smul_volume_pi, that one should use instead (and whose proof
uses this particular case).
theorem
real.volume_preserving_transvection_struct
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
(t : matrix.transvection_struct ι ℝ) :
A transvection preserves Lebesgue measure.
theorem
real.map_matrix_volume_pi_eq_smul_volume_pi
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
{M : matrix ι ι ℝ}
(hM : M.det ≠ 0) :
Any invertible matrix rescales Lebesgue measure through the absolute value of its determinant.
theorem
real.map_linear_map_volume_pi_eq_smul_volume_pi
{ι : Type u_1}
[fintype ι]
{f : (ι → ℝ) →ₗ[ℝ] ι → ℝ}
(hf : ⇑linear_map.det f ≠ 0) :
Any invertible linear map rescales Lebesgue measure through the absolute value of its determinant.
theorem
filter.eventually.volume_pos_of_nhds_real
{p : ℝ → Prop}
{a : ℝ}
(h : ∀ᶠ (x : ℝ) in nhds a, p x) :
0 < ⇑measure_theory.measure_space.volume {x : ℝ | p x}
theorem
region_between_subset
{α : Type u_1}
(f g : α → ℝ)
(s : set α) :
region_between f g s ⊆ s ×ˢ set.univ
theorem
measurable_set_region_between
{α : Type u_1}
[measurable_space α]
{f g : α → ℝ}
{s : set α}
(hf : measurable f)
(hg : measurable g)
(hs : measurable_set s) :
measurable_set (region_between f g s)
The region between two measurable functions on a measurable set is measurable.
theorem
volume_region_between_eq_lintegral'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
(hf : measurable f)
(hg : measurable g)
(hs : measurable_set s) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ∫⁻ (y : α) in s, ennreal.of_real ((g - f) y) ∂μ
theorem
volume_region_between_eq_lintegral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
[measure_theory.sigma_finite μ]
(hf : ae_measurable f (μ.restrict s))
(hg : ae_measurable g (μ.restrict s))
(hs : measurable_set s) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ∫⁻ (y : α) in s, ennreal.of_real ((g - f) y) ∂μ
The volume of the region between two almost everywhere measurable functions on a measurable set can be represented as a Lebesgue integral.
theorem
volume_region_between_eq_integral'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
[measure_theory.sigma_finite μ]
(f_int : measure_theory.integrable_on f s μ)
(g_int : measure_theory.integrable_on g s μ)
(hs : measurable_set s)
(hfg : f ≤ᵐ[μ.restrict s] g) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ennreal.of_real (∫ (y : α) in s, (g - f) y ∂μ)
theorem
volume_region_between_eq_integral
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
[measure_theory.sigma_finite μ]
(f_int : measure_theory.integrable_on f s μ)
(g_int : measure_theory.integrable_on g s μ)
(hs : measurable_set s)
(hfg : ∀ (x : α), x ∈ s → f x ≤ g x) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ennreal.of_real (∫ (y : α) in s, (g - f) y ∂μ)
If two functions are integrable on a measurable set, and one function is less than or equal to the other on that set, then the volume of the region between the two functions can be represented as an integral.