Documentation

Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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 #

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.measure StieltjesFunction.id) 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
@[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) =
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) = Finset.prod Finset.univ fun (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 = Finset.prod Finset.univ fun (i : ι) => b i - a i
theorem Real.volume_pi_Ioo {ι : Type u_1} [Fintype ι] {a : ι} {b : ι} :
MeasureTheory.volume (Set.pi Set.univ fun (i : ι) => Set.Ioo (a i) (b i)) = Finset.prod Finset.univ fun (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.pi Set.univ fun (i : ι) => Set.Ioo (a i) (b i))).toReal = Finset.prod Finset.univ fun (i : ι) => b i - a i
theorem Real.volume_pi_Ioc {ι : Type u_1} [Fintype ι] {a : ι} {b : ι} :
MeasureTheory.volume (Set.pi Set.univ fun (i : ι) => Set.Ioc (a i) (b i)) = Finset.prod Finset.univ fun (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.pi Set.univ fun (i : ι) => Set.Ioc (a i) (b i))).toReal = Finset.prod Finset.univ fun (i : ι) => b i - a i
theorem Real.volume_pi_Ico {ι : Type u_1} [Fintype ι] {a : ι} {b : ι} :
MeasureTheory.volume (Set.pi Set.univ fun (i : ι) => Set.Ico (a i) (b i)) = Finset.prod Finset.univ fun (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.pi Set.univ fun (i : ι) => Set.Ico (a i) (b i))).toReal = Finset.prod Finset.univ fun (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 Finset.prod Finset.univ fun (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.det (Matrix.diagonal D) 0) :
ENNReal.ofReal |Matrix.det (Matrix.diagonal D)| 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' (Matrix.TransvectionStruct.toMatrix t))) 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 : Matrix.det M 0) :
MeasureTheory.Measure.map ((Matrix.toLin' M)) MeasureTheory.volume = ENNReal.ofReal |(Matrix.det M)⁻¹| 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
Instances For
    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) :

    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) :
    (MeasureTheory.Measure.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.SigmaFinite μ] (hf : AEMeasurable f (MeasureTheory.Measure.restrict μ s)) (hg : AEMeasurable g (MeasureTheory.Measure.restrict μ s)) (hs : MeasurableSet s) :
    (MeasureTheory.Measure.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)} (MeasureTheory.Measure.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)} (MeasureTheory.Measure.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)} (MeasureTheory.Measure.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)} (MeasureTheory.Measure.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 sb sa < b∀ᵐ (x : ) ∂MeasureTheory.Measure.restrict μ (s Set.Ioo a b), p x) :
    ∀ᵐ (x : ) ∂MeasureTheory.Measure.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 sb sa < b∀ᵐ (x : ) ∂μ, x s Set.Ioo a bp x) :
    ∀ᵐ (x : ) ∂μ, x sp 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.