Elementary real-measure identities and maps

This file records elementary identities about measures on the real line. The absolute-value map folds the negative half-line onto the positive half-line. Squaring loses the sign of a real number and nothing else, so it determines a measure on the line as soon as the measure cannot tell the two signs apart. For a reflection-invariant measure, the pushforward under squaring is a complete invariant: such a measure is determined by its mass on subsets of (0, ∞) and on {0}, and the squared pushforward records both. For a measure carried by the nonnegative half-line, squaring is undone by Real.sqrt, so the pushforward determines the measure outright.

Main results

• TauCeti.volume_Ioc_inter_Ioo_zero_one — the portion of an interval in the open unit interval;
• MeasureTheory.Measure.map_abs_eq_restrict_add_restrict — decomposition of the image under absolute value into the two half-lines;
• MeasureTheory.Measure.map_abs_apply_zero — the image under absolute value preserves the atom at zero;
• MeasureTheory.Measure.ae_eq_preimage_Ioc, MeasureTheory.Measure.measureReal_eq_sub_of_preimage_Ioo_subset — for a law without atoms, endpoint conventions of an interval with extended bounds do not matter;
• MeasureTheory.Measure.eq_of_map_sq_eq_of_map_neg_eq_self — two symmetric real measures with the same pushforward after squaring are equal.
• MeasureTheory.Measure.map_sqrt_map_sq — on the nonnegative half-line, taking square roots undoes squaring.

theorem MeasureTheory.Measure.map_abs_eq_restrict_add_restrict (μ : Measure ℝ) : map (fun (x : ℝ) => |x|) μ = μ.restrict (Set.Ici 0) + μ.neg.restrict (Set.Ioi 0)

The folded law. Folding keeps the nonnegative half of μ in place and reflects its negative half onto the positive half-line.

@[simp]

theorem MeasureTheory.Measure.map_abs_apply_zero (μ : Measure ℝ) : (map (fun (x : ℝ) => |x|) μ) {0} = μ {0}

The atom of the folded law at 0 is the atom of μ at 0.

theorem MeasureTheory.Measure.ae_eq_preimage_Ioc {μ : Measure ℝ} [NullSingletonClass μ] {s : Set ℝ} {l r : EReal} (hs₁ : Real.toEReal ⁻¹' Set.Ioo l r ⊆ s) (hs₂ : s ⊆ Real.toEReal ⁻¹' Set.Icc l r) : s =ᵐ[μ] Real.toEReal ⁻¹' Set.Ioc l r

For a law without atoms, a set between the open and the closed interval with extended bounds l, r agrees with the half-open interval (l, r] off a null set: the two candidate endpoints carry no mass.

theorem MeasureTheory.Measure.measureReal_eq_sub_of_preimage_Ioo_subset {μ : Measure ℝ} [NullSingletonClass μ] {s : Set ℝ} {l r : EReal} [IsFiniteMeasure μ] (hlr : l ≤ r) (hs₁ : Real.toEReal ⁻¹' Set.Ioo l r ⊆ s) (hs₂ : s ⊆ Real.toEReal ⁻¹' Set.Icc l r) : μ.real s = μ.real (Real.toEReal ⁻¹' Set.Iic r) - μ.real (Real.toEReal ⁻¹' Set.Iic l)

For a finite law without atoms, the mass of a set between the open and the closed interval with extended bounds l ≤ r is the difference of the masses up to the two bounds.

theorem TauCeti.map_volume_mul_add {c : ℝ} (hc : c ≠ 0) (d : ℝ) : MeasureTheory.Measure.map (fun (t : ℝ) => c * t + d) MeasureTheory.volume = ENNReal.ofReal |c⁻¹| • MeasureTheory.volume

The pushforward of Lebesgue measure under an invertible affine map. Translation preserves volume, while scaling contributes the reciprocal absolute slope.

@[simp]

theorem TauCeti.volume_Ioc_inter_Ioo_zero_one {a b : ℝ} (ha : 0 ≤ a) (hb : b ≤ 1) : MeasureTheory.volume (Set.Ioc a b ∩ Set.Ioo 0 1) = ENNReal.ofReal (b - a)

The part of a subinterval Ioc a b of [0, 1] lying in the open unit interval has the full length b - a: the two intervals differ at most at the endpoint 1.

theorem MeasureTheory.Measure.eq_of_map_sq_eq_of_map_neg_eq_self (μ ν : Measure ℝ) (hμneg : map (fun (x : ℝ) => -x) μ = μ) (hνneg : map (fun (x : ℝ) => -x) ν = ν) (hsq : map (fun (x : ℝ) => x ^ 2) μ = map (fun (x : ℝ) => x ^ 2) ν) : μ = ν

Two reflection-invariant measures on ℝ are equal if their pushforwards under squaring are equal. Neither measure needs to be finite.

theorem MeasureTheory.Measure.map_sqrt_map_sq (μ : Measure ℝ) (hμ : ∀ᵐ (t : ℝ) ∂μ, 0 ≤ t) : map Real.sqrt (map (fun (t : ℝ) => t ^ 2) μ) = μ

Square roots undo squaring for a measure carried by the nonnegative half-line: the pushforward of μ under x ↦ x ^ 2 returns to μ under Real.sqrt.