Lebesgue measure on the real line and on ℝⁿ

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_linearMap_volume_pi_eq_smul_volume_pi.

More properties of the Lebesgue measure are deduced from this in Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.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

theorem Real.volume_eq_stieltjes_id : MeasureTheory.volume = StieltjesFunction.id.measure

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.

theorem Real.volume_val (s : Set ℝ) : MeasureTheory.volume s = StieltjesFunction.id.measure s

@[simp]

theorem Real.volume_Ico {a : ℝ} {b : ℝ} : MeasureTheory.volume (Set.Ico a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.volume_Icc {a : ℝ} {b : ℝ} : MeasureTheory.volume (Set.Icc a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.volume_Ioo {a : ℝ} {b : ℝ} : MeasureTheory.volume (Set.Ioo a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.volume_Ioc {a : ℝ} {b : ℝ} : MeasureTheory.volume (Set.Ioc a b) = ENNReal.ofReal (b - a)

theorem Real.volume_singleton {a : ℝ} : MeasureTheory.volume {a} = 0

theorem Real.volume_univ : MeasureTheory.volume Set.univ = ⊤

@[simp]

theorem Real.volume_ball (a : ℝ) (r : ℝ) : MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal (2 * r)

@[simp]

theorem Real.volume_closedBall (a : ℝ) (r : ℝ) : MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal (2 * r)

@[simp]

theorem Real.volume_emetric_ball (a : ℝ) (r : ENNReal) : MeasureTheory.volume (EMetric.ball a r) = 2 * r

@[simp]

theorem Real.volume_emetric_closedBall (a : ℝ) (r : ENNReal) : MeasureTheory.volume (EMetric.closedBall a r) = 2 * r

instance Real.noAtoms_volume : MeasureTheory.NoAtoms MeasureTheory.volume

Equations

• Real.noAtoms_volume = ⋯

@[simp]

theorem Real.volume_interval {a : ℝ} {b : ℝ} : MeasureTheory.volume (Set.uIcc a b) = ENNReal.ofReal |b - a|

@[simp]

theorem Real.volume_Ioi {a : ℝ} : MeasureTheory.volume (Set.Ioi a) = ⊤

@[simp]

theorem Real.volume_Ici {a : ℝ} : MeasureTheory.volume (Set.Ici a) = ⊤

@[simp]

theorem Real.volume_Iio {a : ℝ} : MeasureTheory.volume (Set.Iio a) = ⊤

@[simp]

theorem Real.volume_Iic {a : ℝ} : MeasureTheory.volume (Set.Iic a) = ⊤

instance Real.locallyFinite_volume : MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume

Equations

• Real.locallyFinite_volume = ⋯

instance Real.isFiniteMeasure_restrict_Icc (x : ℝ) (y : ℝ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Icc x y))

Equations

• ⋯ = ⋯

instance Real.isFiniteMeasure_restrict_Ico (x : ℝ) (y : ℝ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ico x y))

Equations

• ⋯ = ⋯

instance Real.isFiniteMeasure_restrict_Ioc (x : ℝ) (y : ℝ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ioc x y))

Equations

• ⋯ = ⋯

instance Real.isFiniteMeasure_restrict_Ioo (x : ℝ) (y : ℝ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ioo x y))

Equations

• ⋯ = ⋯

theorem Real.volume_le_diam (s : Set ℝ) : MeasureTheory.volume s ≤ EMetric.diam s

theorem Filter.Eventually.volume_pos_of_nhds_real {p : ℝ → Prop} {a : ℝ} (h : ∀ᶠ (x : ℝ) in nhds a, p x) : 0 < MeasureTheory.volume {x : ℝ | p x}

Volume of a box in ℝⁿ

theorem Real.volume_Icc_pi {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} : MeasureTheory.volume (Set.Icc a b) = ∏ i : ι, ENNReal.ofReal (b i - a i)

@[simp]

theorem Real.volume_Icc_pi_toReal {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} (h : a ≤ b) : (MeasureTheory.volume (Set.Icc a b)).toReal = ∏ i : ι, (b i - a i)

theorem Real.volume_pi_Ioo {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} : MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioo (a i) (b i)) = ∏ i : ι, ENNReal.ofReal (b i - a i)

@[simp]

theorem Real.volume_pi_Ioo_toReal {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} (h : a ≤ b) : (MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioo (a i) (b i))).toReal = ∏ i : ι, (b i - a i)

theorem Real.volume_pi_Ioc {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} : MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioc (a i) (b i)) = ∏ i : ι, ENNReal.ofReal (b i - a i)

@[simp]

theorem Real.volume_pi_Ioc_toReal {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} (h : a ≤ b) : (MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioc (a i) (b i))).toReal = ∏ i : ι, (b i - a i)

theorem Real.volume_pi_Ico {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} : MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ico (a i) (b i)) = ∏ i : ι, ENNReal.ofReal (b i - a i)

@[simp]

theorem Real.volume_pi_Ico_toReal {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {b : ι → ℝ} (h : a ≤ b) : (MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ico (a i) (b i))).toReal = ∏ i : ι, (b i - a i)

@[simp]

theorem Real.volume_pi_ball {ι : Type u_1} [Fintype ι] (a : ι → ℝ) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

@[simp]

theorem Real.volume_pi_closedBall {ι : Type u_1} [Fintype ι] (a : ι → ℝ) {r : ℝ} (hr : 0 ≤ r) : MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

theorem Real.volume_pi_le_prod_diam {ι : Type u_1} [Fintype ι] (s : Set (ι → ℝ)) : MeasureTheory.volume s ≤ ∏ i : ι, EMetric.diam (Function.eval i '' s)

theorem Real.volume_pi_le_diam_pow {ι : Type u_1} [Fintype ι] (s : Set (ι → ℝ)) : MeasureTheory.volume s ≤ EMetric.diam s ^ Fintype.card ι

Images of the Lebesgue measure under multiplication in ℝ

theorem Real.smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) : ENNReal.ofReal |a| • MeasureTheory.Measure.map (fun (x : ℝ) => a * x) MeasureTheory.volume = MeasureTheory.volume

theorem Real.map_volume_mul_left {a : ℝ} (h : a ≠ 0) : MeasureTheory.Measure.map (fun (x : ℝ) => a * x) MeasureTheory.volume = ENNReal.ofReal |a⁻¹| • MeasureTheory.volume

@[simp]

theorem Real.volume_preimage_mul_left {a : ℝ} (h : a ≠ 0) (s : Set ℝ) : MeasureTheory.volume ((fun (x : ℝ) => a * x) ⁻¹' s) = ENNReal.ofReal |a⁻¹| * MeasureTheory.volume s

theorem Real.smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) : ENNReal.ofReal |a| • MeasureTheory.Measure.map (fun (x : ℝ) => x * a) MeasureTheory.volume = MeasureTheory.volume

theorem Real.map_volume_mul_right {a : ℝ} (h : a ≠ 0) : MeasureTheory.Measure.map (fun (x : ℝ) => x * a) MeasureTheory.volume = ENNReal.ofReal |a⁻¹| • MeasureTheory.volume

@[simp]

theorem Real.volume_preimage_mul_right {a : ℝ} (h : a ≠ 0) (s : Set ℝ) : MeasureTheory.volume ((fun (x : ℝ) => x * a) ⁻¹' s) = ENNReal.ofReal |a⁻¹| * MeasureTheory.volume s

Images of the Lebesgue measure under translation/linear maps in ℝⁿ

theorem Real.smul_map_diagonal_volume_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] {D : ι → ℝ} (h : (Matrix.diagonal D).det ≠ 0) : ENNReal.ofReal |(Matrix.diagonal D).det| • MeasureTheory.Measure.map (⇑(Matrix.toLin' (Matrix.diagonal D))) MeasureTheory.volume = MeasureTheory.volume

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_transvectionStruct {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : Matrix.TransvectionStruct ι ℝ) : MeasureTheory.MeasurePreserving (⇑(Matrix.toLin' t.toMatrix)) MeasureTheory.volume MeasureTheory.volume

A transvection preserves Lebesgue measure.

theorem Real.map_matrix_volume_pi_eq_smul_volume_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι ℝ} (hM : M.det ≠ 0) : MeasureTheory.Measure.map (⇑(Matrix.toLin' M)) MeasureTheory.volume = ENNReal.ofReal |M.det⁻¹| • MeasureTheory.volume

Any invertible matrix rescales Lebesgue measure through the absolute value of its determinant.

theorem Real.map_linearMap_volume_pi_eq_smul_volume_pi {ι : Type u_1} [Fintype ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ} (hf : LinearMap.det f ≠ 0) : MeasureTheory.Measure.map (⇑f) MeasureTheory.volume = ENNReal.ofReal |(LinearMap.det f)⁻¹| • MeasureTheory.volume

Any invertible linear map rescales Lebesgue measure through the absolute value of its determinant.

def regionBetween {α : Type u_1} (f : α → ℝ) (g : α → ℝ) (s : Set α) : Set (α × ℝ)

The region between two real-valued functions on an arbitrary set.

Equations

• regionBetween f g s = {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Ioo (f p.1) (g p.1)}

theorem regionBetween_subset {α : Type u_1} (f : α → ℝ) (g : α → ℝ) (s : Set α) : regionBetween f g s ⊆ s ×ˢ Set.univ

theorem measurableSet_regionBetween {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : α → ℝ} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : MeasurableSet (regionBetween f g s)

The region between two measurable functions on a measurable set is measurable.

theorem measurableSet_region_between_oc {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : α → ℝ} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : MeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)}

The region between two measurable functions on a measurable set is measurable; a version for the region together with the graph of the upper function.

theorem measurableSet_region_between_co {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : α → ℝ} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : MeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)}

The region between two measurable functions on a measurable set is measurable; a version for the region together with the graph of the lower function.

theorem measurableSet_region_between_cc {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : α → ℝ} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : MeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)}

The region between two measurable functions on a measurable set is measurable; a version for the region together with the graphs of both functions.

theorem measurableSet_graph {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) : MeasurableSet {p : α × ℝ | p.2 = f p.1}

The graph of a measurable function is a measurable set.

theorem volume_regionBetween_eq_lintegral' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {g : α → ℝ} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : (μ.prod MeasureTheory.volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y) ∂μ

theorem volume_regionBetween_eq_lintegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {g : α → ℝ} {s : Set α} [MeasureTheory.SFinite μ] (hf : AEMeasurable f (μ.restrict s)) (hg : AEMeasurable g (μ.restrict s)) (hs : MeasurableSet s) : (μ.prod MeasureTheory.volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ENNReal.ofReal ((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 nullMeasurableSet_regionBetween {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ℝ} {g : α → ℝ} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Ioo (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

The region between two a.e.-measurable functions on a null-measurable set is null-measurable.

theorem nullMeasurableSet_region_between_oc {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ℝ} {g : α → ℝ} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for the region together with the graph of the upper function.

theorem nullMeasurableSet_region_between_co {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ℝ} {g : α → ℝ} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for the region together with the graph of the lower function.

theorem nullMeasurableSet_region_between_cc {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ℝ} {g : α → ℝ} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for the region together with the graphs of both functions.

theorem ae_restrict_of_ae_restrict_inter_Ioo {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NoAtoms μ] {s : Set ℝ} {p : ℝ → Prop} (h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Set.Ioo a b), p x) : ∀ᵐ (x : ℝ) ∂μ.restrict s, p x

Consider a real set s. If a property is true almost everywhere in s ∩ (a, b) for all a, b ∈ s, then it is true almost everywhere in s. Formulated with μ.restrict. See also ae_of_mem_of_ae_of_mem_inter_Ioo.

theorem ae_of_mem_of_ae_of_mem_inter_Ioo {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NoAtoms μ] {s : Set ℝ} {p : ℝ → Prop} (h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Set.Ioo a b → p x) : ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x

Consider a real set s. If a property is true almost everywhere in s ∩ (a, b) for all a, b ∈ s, then it is true almost everywhere in s. Formulated with bare membership. See also ae_restrict_of_ae_restrict_inter_Ioo.