Lebesgue measure of intervals and centered interval differences

Replacing two subsets of the real line by open centered intervals of the same respective volumes can only decrease the volume of their one-sided difference. The inequality uses Mathlib's extended-radius balls and Real.volume_eball, and allows zero and infinite volumes. It supplies the sectionwise contraction inequality for Steiner symmetrization.

An order-connected subset of the real line of positive finite volume agrees almost everywhere with a nonempty bounded open interval (Set.OrdConnected.exists_ae_eq_Ioo): finite volume bounds it, and it lies between the open and the closed interval spanned by its infimum and supremum.

Pulling real Lebesgue measure on (0,T] back to ℝ≥0 commutes with restriction, and the resulting finite-horizon measure has total mass T.

On a finite coordinate space ι → ℝ, permuting the coordinates and changing their signs preserves Lebesgue measure (TauCeti.volume_preserving_signedPerm).

The Lebesgue measure of a finite union of pairwise disjoint intervals Ι (a i) (b i) is the sum of their lengths (TauCeti.volume_biUnion_uIoc_eq_ofReal_sum).

theorem NNReal.comap_volume_restrict_Ioc (T : NNReal) : MeasureTheory.Measure.comap toReal (MeasureTheory.volume.restrict (Set.Ioc 0 ↑T)) = (MeasureTheory.Measure.comap toReal MeasureTheory.volume).restrict (Set.Ioc 0 T)

Pulling Lebesgue measure on (0,T] back to ℝ≥0 is the restriction of its pullback.

theorem NNReal.comap_volume_restrict_Ioc_univ (T : NNReal) : (MeasureTheory.Measure.comap toReal (MeasureTheory.volume.restrict (Set.Ioc 0 ↑T))) Set.univ = ↑T

The pullback of Lebesgue measure on (0,T] to ℝ≥0 has total mass T.

theorem TauCeti.volume_eball_sdiff_le (s u : Set ℝ) : MeasureTheory.volume (Metric.eball 0 (MeasureTheory.volume s / 2) \ Metric.eball 0 (MeasureTheory.volume u / 2)) ≤ MeasureTheory.volume (s \ u)

Centering intervals can only decrease the length of a one-sided difference.

theorem TauCeti.volume_preserving_signedPerm {ι : Type u_1} [Fintype ι] (e : Equiv.Perm ι) (c : ι → ℝ) (hc : ∀ (i : ι), |c i| = 1) : MeasureTheory.MeasurePreserving (fun (x : ι → ℝ) (i : ι) => c i * x (e i)) MeasureTheory.volume MeasureTheory.volume

A permutation of the coordinates combined with sign changes, x ↦ fun i => c i * x (e i) with |c i| = 1, preserves Lebesgue measure on ι → ℝ.

theorem TauCeti.volume_biUnion_uIoc_eq_ofReal_sum {ι : Type u_1} (I : Finset ι) (a b : ι → ℝ) (h : (↑I).PairwiseDisjoint fun (i : ι) => Set.uIoc (a i) (b i)) : MeasureTheory.volume (⋃ i ∈ I, Set.uIoc (a i) (b i)) = ENNReal.ofReal (∑ i ∈ I, (max (a i) (b i) - min (a i) (b i)))

The measure of a finite union of pairwise disjoint intervals Ι (a i) (b i) is the sum of their lengths max (a i) (b i) - min (a i) (b i).

theorem Set.OrdConnected.exists_ae_eq_Ioo {I : Set ℝ} (hI : I.OrdConnected) (h0 : MeasureTheory.volume I ≠ 0) (hfin : MeasureTheory.volume I ≠ ⊤) : ∃ (a : ℝ) (b : ℝ), a < b ∧ I =ᵐ[MeasureTheory.volume] Ioo a b

An order-connected subset of ℝ of positive finite volume agrees almost everywhere with a nonempty bounded open interval.