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 : Eq MeasureTheory.MeasureSpace.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 Real) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume s) (DFunLike.coe StieltjesFunction.id.measure s)

theorem Real.volume_Ico {a b : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Ico a b)) (ENNReal.ofReal (HSub.hSub b a))

theorem Real.volume_Icc {a b : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Icc a b)) (ENNReal.ofReal (HSub.hSub b a))

theorem Real.volume_Ioo {a b : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Ioo a b)) (ENNReal.ofReal (HSub.hSub b a))

theorem Real.volume_Ioc {a b : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Ioc a b)) (ENNReal.ofReal (HSub.hSub b a))

theorem Real.volume_singleton {a : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Singleton.singleton a)) 0

theorem Real.volume_univ : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume Set.univ) Top.top

theorem Real.volume_ball (a r : Real) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Metric.ball a r)) (ENNReal.ofReal (HMul.hMul 2 r))

theorem Real.volume_closedBall (a r : Real) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Metric.closedBall a r)) (ENNReal.ofReal (HMul.hMul 2 r))

theorem Real.volume_emetric_ball (a : Real) (r : ENNReal) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (EMetric.ball a r)) (HMul.hMul 2 r)

theorem Real.volume_emetric_closedBall (a : Real) (r : ENNReal) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (EMetric.closedBall a r)) (HMul.hMul 2 r)

theorem Real.noAtoms_volume : MeasureTheory.NoAtoms MeasureTheory.MeasureSpace.volume

theorem Real.volume_interval {a b : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.uIcc a b)) (ENNReal.ofReal (abs (HSub.hSub b a)))

theorem Real.volume_Ioi {a : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Ioi a)) Top.top

theorem Real.volume_Ici {a : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Ici a)) Top.top

theorem Real.volume_Iio {a : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Iio a)) Top.top

theorem Real.volume_Iic {a : Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Iic a)) Top.top

theorem Real.locallyFinite_volume : MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.MeasureSpace.volume

theorem Real.isFiniteMeasure_restrict_Icc (x y : Real) : MeasureTheory.IsFiniteMeasure (MeasureTheory.MeasureSpace.volume.restrict (Set.Icc x y))

theorem Real.isFiniteMeasure_restrict_Ico (x y : Real) : MeasureTheory.IsFiniteMeasure (MeasureTheory.MeasureSpace.volume.restrict (Set.Ico x y))

theorem Real.isFiniteMeasure_restrict_Ioc (x y : Real) : MeasureTheory.IsFiniteMeasure (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioc x y))

theorem Real.isFiniteMeasure_restrict_Ioo (x y : Real) : MeasureTheory.IsFiniteMeasure (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioo x y))

theorem Real.volume_le_diam (s : Set Real) : LE.le (DFunLike.coe MeasureTheory.MeasureSpace.volume s) (EMetric.diam s)

theorem Filter.Eventually.volume_pos_of_nhds_real {p : Real → Prop} {a : Real} (h : Filter.Eventually (fun (x : Real) => p x) (nhds a)) : LT.lt 0 (DFunLike.coe MeasureTheory.MeasureSpace.volume (setOf fun (x : Real) => p x))

Volume of a box in ℝⁿ

theorem Real.volume_Icc_pi {ι : Type u_1} [Fintype ι] {a b : ι → Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Icc a b)) (Finset.univ.prod fun (i : ι) => ENNReal.ofReal (HSub.hSub (b i) (a i)))

theorem Real.volume_Icc_pi_toReal {ι : Type u_1} [Fintype ι] {a b : ι → Real} (h : LE.le a b) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.Icc a b)).toReal (Finset.univ.prod fun (i : ι) => HSub.hSub (b i) (a i))

theorem Real.volume_pi_Ioo {ι : Type u_1} [Fintype ι] {a b : ι → Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.univ.pi fun (i : ι) => Set.Ioo (a i) (b i))) (Finset.univ.prod fun (i : ι) => ENNReal.ofReal (HSub.hSub (b i) (a i)))

theorem Real.volume_pi_Ioo_toReal {ι : Type u_1} [Fintype ι] {a b : ι → Real} (h : LE.le a b) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.univ.pi fun (i : ι) => Set.Ioo (a i) (b i))).toReal (Finset.univ.prod fun (i : ι) => HSub.hSub (b i) (a i))

theorem Real.volume_pi_Ioc {ι : Type u_1} [Fintype ι] {a b : ι → Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.univ.pi fun (i : ι) => Set.Ioc (a i) (b i))) (Finset.univ.prod fun (i : ι) => ENNReal.ofReal (HSub.hSub (b i) (a i)))

theorem Real.volume_pi_Ioc_toReal {ι : Type u_1} [Fintype ι] {a b : ι → Real} (h : LE.le a b) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.univ.pi fun (i : ι) => Set.Ioc (a i) (b i))).toReal (Finset.univ.prod fun (i : ι) => HSub.hSub (b i) (a i))

theorem Real.volume_pi_Ico {ι : Type u_1} [Fintype ι] {a b : ι → Real} : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.univ.pi fun (i : ι) => Set.Ico (a i) (b i))) (Finset.univ.prod fun (i : ι) => ENNReal.ofReal (HSub.hSub (b i) (a i)))

theorem Real.volume_pi_Ico_toReal {ι : Type u_1} [Fintype ι] {a b : ι → Real} (h : LE.le a b) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.univ.pi fun (i : ι) => Set.Ico (a i) (b i))).toReal (Finset.univ.prod fun (i : ι) => HSub.hSub (b i) (a i))

theorem Real.volume_pi_ball {ι : Type u_1} [Fintype ι] (a : ι → Real) {r : Real} (hr : LT.lt 0 r) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Metric.ball a r)) (ENNReal.ofReal (HPow.hPow (HMul.hMul 2 r) (Fintype.card ι)))

theorem Real.volume_pi_closedBall {ι : Type u_1} [Fintype ι] (a : ι → Real) {r : Real} (hr : LE.le 0 r) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Metric.closedBall a r)) (ENNReal.ofReal (HPow.hPow (HMul.hMul 2 r) (Fintype.card ι)))

theorem Real.volume_pi_le_prod_diam {ι : Type u_1} [Fintype ι] (s : Set (ι → Real)) : LE.le (DFunLike.coe MeasureTheory.MeasureSpace.volume s) (Finset.univ.prod fun (i : ι) => EMetric.diam (Set.image (Function.eval i) s))

theorem Real.volume_pi_le_diam_pow {ι : Type u_1} [Fintype ι] (s : Set (ι → Real)) : LE.le (DFunLike.coe MeasureTheory.MeasureSpace.volume s) (HPow.hPow (EMetric.diam s) (Fintype.card ι))

Images of the Lebesgue measure under multiplication in ℝ

theorem Real.smul_map_volume_mul_left {a : Real} (h : Ne a 0) : Eq (HSMul.hSMul (ENNReal.ofReal (abs a)) (MeasureTheory.Measure.map (fun (x : Real) => HMul.hMul a x) MeasureTheory.MeasureSpace.volume)) MeasureTheory.MeasureSpace.volume

theorem Real.map_volume_mul_left {a : Real} (h : Ne a 0) : Eq (MeasureTheory.Measure.map (fun (x : Real) => HMul.hMul a x) MeasureTheory.MeasureSpace.volume) (HSMul.hSMul (ENNReal.ofReal (abs (Inv.inv a))) MeasureTheory.MeasureSpace.volume)

theorem Real.volume_preimage_mul_left {a : Real} (h : Ne a 0) (s : Set Real) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.preimage (fun (x : Real) => HMul.hMul a x) s)) (HMul.hMul (ENNReal.ofReal (abs (Inv.inv a))) (DFunLike.coe MeasureTheory.MeasureSpace.volume s))

theorem Real.smul_map_volume_mul_right {a : Real} (h : Ne a 0) : Eq (HSMul.hSMul (ENNReal.ofReal (abs a)) (MeasureTheory.Measure.map (fun (x : Real) => HMul.hMul x a) MeasureTheory.MeasureSpace.volume)) MeasureTheory.MeasureSpace.volume

theorem Real.map_volume_mul_right {a : Real} (h : Ne a 0) : Eq (MeasureTheory.Measure.map (fun (x : Real) => HMul.hMul x a) MeasureTheory.MeasureSpace.volume) (HSMul.hSMul (ENNReal.ofReal (abs (Inv.inv a))) MeasureTheory.MeasureSpace.volume)

theorem Real.volume_preimage_mul_right {a : Real} (h : Ne a 0) (s : Set Real) : Eq (DFunLike.coe MeasureTheory.MeasureSpace.volume (Set.preimage (fun (x : Real) => HMul.hMul x a) s)) (HMul.hMul (ENNReal.ofReal (abs (Inv.inv a))) (DFunLike.coe MeasureTheory.MeasureSpace.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 : ι → Real} (h : Ne (Matrix.diagonal D).det 0) : Eq (HSMul.hSMul (ENNReal.ofReal (abs (Matrix.diagonal D).det)) (MeasureTheory.Measure.map (DFunLike.coe (DFunLike.coe Matrix.toLin' (Matrix.diagonal D))) MeasureTheory.MeasureSpace.volume)) MeasureTheory.MeasureSpace.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 ι Real) : MeasureTheory.MeasurePreserving (DFunLike.coe (DFunLike.coe Matrix.toLin' t.toMatrix)) MeasureTheory.MeasureSpace.volume MeasureTheory.MeasureSpace.volume

A transvection preserves Lebesgue measure.

theorem Real.map_matrix_volume_pi_eq_smul_volume_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι Real} (hM : Ne M.det 0) : Eq (MeasureTheory.Measure.map (DFunLike.coe (DFunLike.coe Matrix.toLin' M)) MeasureTheory.MeasureSpace.volume) (HSMul.hSMul (ENNReal.ofReal (abs (Inv.inv M.det))) MeasureTheory.MeasureSpace.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 : LinearMap (RingHom.id Real) (ι → Real) (ι → Real)} (hf : Ne (DFunLike.coe LinearMap.det f) 0) : Eq (MeasureTheory.Measure.map (DFunLike.coe f) MeasureTheory.MeasureSpace.volume) (HSMul.hSMul (ENNReal.ofReal (abs (Inv.inv (DFunLike.coe LinearMap.det f)))) MeasureTheory.MeasureSpace.volume)

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

def regionBetween {α : Type u_1} (f g : α → Real) (s : Set α) : Set (Prod α Real)

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

Equations

• Eq (regionBetween f g s) (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Ioo (f p.fst) (g p.fst)) p.snd))

theorem regionBetween_subset {α : Type u_1} (f g : α → Real) (s : Set α) : HasSubset.Subset (regionBetween f g s) (SProd.sprod s Set.univ)

theorem measurableSet_regionBetween {α : Type u_1} [MeasurableSpace α] {f g : α → Real} {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 : α → Real} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : MeasurableSet (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Ioc (f p.fst) (g p.fst)) p.snd))

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 : α → Real} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : MeasurableSet (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Ico (f p.fst) (g p.fst)) p.snd))

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 : α → Real} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : MeasurableSet (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Icc (f p.fst) (g p.fst)) p.snd))

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 : α → Real} (hf : Measurable f) : MeasurableSet (setOf fun (p : Prod α Real) => Eq p.snd (f p.fst))

The graph of a measurable function is a measurable set.

theorem volume_regionBetween_eq_lintegral' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → Real} {s : Set α} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) : Eq (DFunLike.coe (μ.prod MeasureTheory.MeasureSpace.volume) (regionBetween f g s)) (MeasureTheory.lintegral (μ.restrict s) fun (y : α) => ENNReal.ofReal (HSub.hSub g f y))

theorem volume_regionBetween_eq_lintegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → Real} {s : Set α} [MeasureTheory.SFinite μ] (hf : AEMeasurable f (μ.restrict s)) (hg : AEMeasurable g (μ.restrict s)) (hs : MeasurableSet s) : Eq (DFunLike.coe (μ.prod MeasureTheory.MeasureSpace.volume) (regionBetween f g s)) (MeasureTheory.lintegral (μ.restrict s) fun (y : α) => ENNReal.ofReal (HSub.hSub 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 : α → Real} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Ioo (f p.fst) (g p.fst)) p.snd)) (μ.prod MeasureTheory.MeasureSpace.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 : α → Real} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Ioc (f p.fst) (g p.fst)) p.snd)) (μ.prod MeasureTheory.MeasureSpace.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 : α → Real} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Ico (f p.fst) (g p.fst)) p.snd)) (μ.prod MeasureTheory.MeasureSpace.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 : α → Real} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ) {s : Set α} (s_mble : MeasureTheory.NullMeasurableSet s μ) : MeasureTheory.NullMeasurableSet (setOf fun (p : Prod α Real) => And (Membership.mem s p.fst) (Membership.mem (Set.Icc (f p.fst) (g p.fst)) p.snd)) (μ.prod MeasureTheory.MeasureSpace.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 Real} [MeasureTheory.NoAtoms μ] {s : Set Real} {p : Real → Prop} (h : ∀ (a b : Real), Membership.mem s a → Membership.mem s b → LT.lt a b → Filter.Eventually (fun (x : Real) => p x) (MeasureTheory.ae (μ.restrict (Inter.inter s (Set.Ioo a b))))) : Filter.Eventually (fun (x : Real) => p x) (MeasureTheory.ae (μ.restrict s))

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 Real} [MeasureTheory.NoAtoms μ] {s : Set Real} {p : Real → Prop} (h : ∀ (a b : Real), Membership.mem s a → Membership.mem s b → LT.lt a b → Filter.Eventually (fun (x : Real) => Membership.mem (Inter.inter s (Set.Ioo a b)) x → p x) (MeasureTheory.ae μ)) : Filter.Eventually (fun (x : Real) => Membership.mem s x → p x) (MeasureTheory.ae μ)

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.