Layer-cake formulas for products, distances, and moments

For two nonnegative measurable functions, their product integral is the double integral of the measures of intersections of their strict superlevel sets. This is the two-function form of the layer-cake formula and is useful for comparing pairings through level-set geometry.

This file expresses the L¹ distance between two almost everywhere measurable real functions as the integral, over all levels, of the measure of the symmetric difference of their sublevel sets. Consequently, along a subsequence of an L¹-convergent sequence the superlevel sets converge in measure at almost every level. Averaging the same identity over the levels shows that, if finitely many functions are close in L¹ to a nonnegative function p, then some superlevel set of p has small total boundary relative to its measure; for counting measure this produces Følner sets from almost invariant finitely supported functions. Thresholding a real function at a level t with δ ≤ t ≤ 1 - δ, where δ > 0, approximates a set in measure with error at most its L¹ distance from the set's indicator divided by δ. It also expresses the integral of the positive part (g - f)⁺ as the integral, over all levels s, of the measure of the set where f ≤ s < g: the one-sided form, which sees which of the two functions lies above the level. Its extended version expresses the integral of the truncated difference f - g of two ℝ≥0∞-valued functions through the differences of their strict superlevel sets.

For 1 < p it writes the power |x - y| ^ p as a mixture of hinges: it is the integral over the thresholds r > 0, with weight p (p - 1) r ^ (p - 2), of (y - x - r)⁺ + (x - y - r)⁺. Integrated against a measure, this turns the p-th moment of a difference into a mixture of one-sided integrals of the form above. The same mixture represents d ^ p for every d : ℝ≥0∞, with truncated subtraction.

Finally, it records the signed layer-cake representation of a real number, a = ∫ (1_{t < a} - 1_{t < 0}) dt, which applied pointwise to a real function u writes it as the integral over all levels t of the indicators of its superlevel sets {u > t}, corrected by 1_{t < 0} so that the integrand is integrable.

The truncated power formula ∫ min(f, k) ^ p = p ∫_0^k m {f > t} t ^ (p - 1) dt is recorded together with the measurability of the distribution function t ↦ m {f > t}. The truncation lets a layer-cake argument work with finite quantities; monotone convergence removes it again, and the truncated integrals ∫ g ^ q min(g, k) ^ δ increase to ∫ g ^ (q + δ) as k → ∞.

For positive real powers on a finite measure space, it also characterizes integrability by the weighted strict tail μ.real {x | t < f x} * t ^ (p - 1), either on (0, ∞) or at infinity. The weighted tail is measurable without any measurability assumption on f, and its contribution from bounded thresholds is integrable. For measures on the nonnegative half-line, the integral of the shifted tail is the extended integral of a truncated difference. A finite first moment therefore makes every shifted tail integrable.

Main statements

• TauCeti.lintegral_mul_eq_lintegral_lintegral_measure_inter — the integral of a product of nonnegative functions, as a double integral of intersections of superlevel sets;
• TauCeti.lintegral_enorm_sub_eq_lintegral_measure_symmDiff — the L¹ distance of two real functions, level by level;
• MeasureTheory.Measure.lintegral_enorm_sub_eq_lintegral_measure_symmDiff_setOf_lt — the same identity with strict superlevel sets;
• MeasureTheory.Measure.measure_symmDiff_setOf_lt_indicator_le — a uniform bound on the measure error of thresholding at levels separated from 0 and 1, in terms of the L¹ distance from a set's indicator;
• MeasureTheory.Measure.exists_pos_sum_measure_symmDiff_lt_mul_measure — a superlevel set of p whose total boundary relative to finitely many L¹-close functions is small compared with its measure;
• MeasureTheory.Measure.exists_strictMono_ae_tendsto_measure_symmDiff_setOf_lt — along a subsequence of an L¹-convergent sequence, the superlevel sets converge in measure at almost every level;
• MeasureTheory.Measure.measurable_measure_ofReal_lt — the distribution function t ↦ m {f > t} is measurable;
• MeasureTheory.Measure.lintegral_min_rpow_eq — the integral of a truncated power min f k ^ p, level by level up to the cap k;
• MeasureTheory.Measure.tendsto_lintegral_mul_min_rpow — the truncated integrals ∫ g ^ q min(g, k) ^ δ increase to ∫ g ^ (q + δ) as k → ∞;
• TauCeti.lintegral_ofReal_sub_eq_lintegral_measure — the integral of a positive part (g - f)⁺, level by level;
• TauCeti.lintegral_sub_eq_lintegral_measure_sdiff — the integral of a truncated difference f - g of extended functions, level by level;
• TauCeti.ofReal_rpow_eq_lintegral_mul_ofReal_sub, TauCeti.rpow_eq_lintegral_mul_sub and TauCeti.edist_rpow_eq_lintegral — a real or extended power d ^ p, and the power |x - y| ^ p of a distance, as mixtures of hinges.
• TauCeti.lintegral_ofReal_sub_sub_eq and TauCeti.lintegral_edist_rpow_eq — their integrated forms for a measure on pairs of real variables;
• TauCeti.integral_indicator_Iio_sub_indicator_Iio_zero — the signed layer-cake representation a = ∫ (1_{t < a} - 1_{t < 0}) dt of a real number, with TauCeti.integral_abs_indicator_Iio_sub_indicator_Iio_zero computing the L¹ norm |a| of its integrand;
• TauCeti.integrable_rpow_iff_integrableOn_weighted_tail and TauCeti.integrable_rpow_iff_integrableAtFilter_weighted_tail — the weighted-tail integrability criteria for positive real-power moments.

theorem TauCeti.lintegral_mul_eq_lintegral_lintegral_measure_inter {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.Measure α) {f g : α → ENNReal} (hf : AEMeasurable f m) (hg : AEMeasurable g m) : ∫⁻ (x : α), f x * g x ∂m = ∫⁻ (s : ℝ) (t : ℝ) in Set.Ioi 0, m ({x : α | ENNReal.ofReal t < f x} ∩ {x : α | ENNReal.ofReal s < g x})

Two-function layer cake. The integral of the product of two nonnegative functions is the double integral of the measures of the intersections of their strict superlevel sets:

∫⁻ x, f x * g x ∂m = ∫⁻ t > 0, ∫⁻ s > 0, m ({ofReal t < f} ∩ {ofReal s < g}).

The formula allows infinite values and requires no finiteness or σ-finiteness assumption on the measure.

theorem TauCeti.lintegral_enorm_sub_eq_lintegral_measure_symmDiff {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.Measure α) [MeasureTheory.SFinite m] {f g : α → ℝ} (hf : AEMeasurable f m) (hg : AEMeasurable g m) : ∫⁻ (a : α), ‖f a - g a‖ₑ ∂m = ∫⁻ (s : ℝ), m (symmDiff {a : α | f a ≤ s} {a : α | g a ≤ s})

The area between two graphs. The L¹ distance of two almost everywhere measurable real functions is the integral, over the levels s, of the measure of the set where exactly one of the two functions is at most s.

theorem MeasureTheory.Measure.lintegral_min_rpow_eq {α : Type u_1} [MeasurableSpace α] (m : Measure α) {f : α → ENNReal} (hf : AEMeasurable f m) (k : NNReal) {p : ℝ} (hp : 0 < p) : ∫⁻ (x : α), min (f x) ↑k ^ p ∂m = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioo 0 ↑k, m {x : α | ENNReal.ofReal t < f x} * ENNReal.ofReal (t ^ (p - 1))

The layer cake formula for a truncation. For p > 0 and a cap k, the integral of min f k ^ p is p times the integral of m {t < f} t ^ (p - 1) over the heights 0 < t < k.

theorem MeasureTheory.Measure.measurable_measure_ofReal_lt {α : Type u_1} [MeasurableSpace α] (m : Measure α) (f : α → ENNReal) : Measurable fun (t : ℝ) => m {x : α | ENNReal.ofReal t < f x}

The distribution function t ↦ m {f > t} is measurable, being antitone.

theorem MeasureTheory.Measure.tendsto_lintegral_mul_min_rpow {α : Type u_1} [MeasurableSpace α] (m : Measure α) {g : α → ENNReal} (hg : Measurable g) {q δ : ℝ} (hq : 0 ≤ q) (hδ : 0 < δ) : Filter.Tendsto (fun (k : ℕ) => ∫⁻ (x : α), g x ^ q * min (g x) ↑↑k ^ δ ∂m) Filter.atTop (nhds (∫⁻ (x : α), g x ^ (q + δ) ∂m))

Removing a truncation. As k → ∞, the integrals of g ^ q min(g, k) ^ δ increase to the integral of g ^ (q + δ).

theorem MeasureTheory.Measure.measure_symmDiff_setOf_lt_indicator_le {α : Type u_1} [MeasurableSpace α] (m : Measure α) {u : α → ℝ} {s : Set α} (hu : AEStronglyMeasurable u m) (hs : NullMeasurableSet s m) {δ t : ℝ} (hδ : 0 < δ) (hδt : δ ≤ t) (htδ : t ≤ 1 - δ) : m (symmDiff {x : α | t < u x} s) ≤ (∫⁻ (x : α), ‖u x - s.indicator 1 x‖ₑ ∂m) / ENNReal.ofReal δ

Thresholding a real function at a level separated from 0 and 1 by δ > 0 approximates a set in measure, with error at most its L¹ distance from the indicator divided by δ. The function need not take values in [0, 1].

theorem MeasureTheory.Measure.lintegral_enorm_sub_eq_lintegral_measure_symmDiff_setOf_lt {α : Type u_1} [MeasurableSpace α] (m : Measure α) [SFinite m] {f g : α → ℝ} (hf : AEMeasurable f m) (hg : AEMeasurable g m) : ∫⁻ (a : α), ‖f a - g a‖ₑ ∂m = ∫⁻ (s : ℝ), m (symmDiff {a : α | s < f a} {a : α | s < g a})

The area between two graphs, through superlevel sets. The L¹ distance of two almost everywhere measurable real functions is the integral, over the levels s, of the measure of the set where exactly one of the two functions exceeds s.

theorem MeasureTheory.Measure.measurable_measure_symmDiff_setOf_lt {α : Type u_1} [MeasurableSpace α] (m : Measure α) [SFinite m] {f g : α → ℝ} (hf : AEMeasurable f m) (hg : AEMeasurable g m) : Measurable fun (s : ℝ) => m (symmDiff {a : α | s < f a} {a : α | s < g a})

The measure of the set where exactly one of two almost everywhere measurable real functions exceeds the level s is a measurable function of s.

theorem MeasureTheory.Measure.exists_pos_sum_measure_symmDiff_lt_mul_measure {α : Type u_1} [MeasurableSpace α] (m : Measure α) [SFinite m] {ι : Type u_2} (K : Finset ι) {p : α → ℝ} {q : ι → α → ℝ} (hp : AEMeasurable p m) (hq : ∀ i ∈ K, AEMeasurable (q i) m) {ε : ENNReal} (h : ∑ i ∈ K, ∫⁻ (x : α), ‖q i x - p x‖ₑ ∂m < ε * ∫⁻ (x : α), ENNReal.ofReal (p x) ∂m) : ∃ t > 0, ∑ i ∈ K, m (symmDiff {x : α | t < q i x} {x : α | t < p x}) < ε * m {x : α | t < p x}

A superlevel set with small boundary. Let p be an almost everywhere measurable real function and let q i, for i ∈ K, be finitely many functions whose total L¹ distance to p is less than ε times the extended nonnegative integral of the positive part of p. Then at some level t > 0 the superlevel set {p > t} has total boundary ∑ i ∈ K, m ({q i > t} ∆ {p > t}) less than ε times its measure.

theorem MeasureTheory.Measure.exists_strictMono_ae_tendsto_measure_symmDiff_setOf_lt {α : Type u_1} [MeasurableSpace α] (m : Measure α) [SFinite m] {f : ℕ → α → ℝ} {g : α → ℝ} (hf : ∀ (n : ℕ), AEMeasurable (f n) m) (hg : AEMeasurable g m) (h : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), ‖f n a - g a‖ₑ ∂m) Filter.atTop (nhds 0)) : ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (s : ℝ), Filter.Tendsto (fun (j : ℕ) => m (symmDiff {a : α | s < f (ns j) a} {a : α | s < g a})) Filter.atTop (nhds 0)

Superlevel sets along an L¹-convergent sequence. If f n → g in L¹(m), then along a subsequence the strict superlevel sets {f n > s} converge in measure to {g > s} at almost every level s: m ({f (ns j) > s} ∆ {g > s}) → 0.

theorem TauCeti.lintegral_ofReal_sub_eq_lintegral_measure {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.Measure α) [MeasureTheory.SFinite m] {f g : α → ℝ} (hf : AEMeasurable f m) (hg : AEMeasurable g m) : ∫⁻ (a : α), ENNReal.ofReal (g a - f a) ∂m = ∫⁻ (s : ℝ), m {a : α | f a ≤ s ∧ s < g a}

The positive part of a difference, level by level. For two almost everywhere measurable real functions f and g, the integral of the positive part of g - f is the integral, over the levels s, of the measure of the set where f ≤ s < g.

theorem TauCeti.lintegral_sub_eq_lintegral_measure_sdiff {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.Measure α) [MeasureTheory.SFinite m] {f g : α → ENNReal} (hf : AEMeasurable f m) (hg : AEMeasurable g m) : ∫⁻ (x : α), f x - g x ∂m = ∫⁻ (s : ℝ) in Set.Ioi 0, m ({x : α | ENNReal.ofReal s < f x} \ {x : α | ENNReal.ofReal s < g x})

Truncated difference, level by level. For two almost everywhere measurable functions f g : α → ℝ≥0∞, the integral of the truncated difference f - g is the integral, over the levels s > 0, of the measure of the set where g ≤ ofReal s < f. Infinite values are allowed; in particular ∞ - ∞ = 0 is matched by the empty level sets.

theorem TauCeti.lintegral_ofReal_sub_sub_eq (m : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.SFinite m] (r : ℝ) : ∫⁻ (z : ℝ × ℝ), ENNReal.ofReal (z.2 - z.1 - r) ∂m = ∫⁻ (a : ℝ), m (Set.Iic a ×ˢ Set.Ioi (a + r))

The expected hinge cost (y - x - r)⁺ is the integral, over the levels a, of the mass given to the quadrant Iic a ×ˢ Ioi (a + r).

theorem TauCeti.ofReal_sub_sub_add_ofReal_sub_sub {r : ℝ} (hr : 0 ≤ r) (x y : ℝ) : ENNReal.ofReal (y - x - r) + ENNReal.ofReal (x - y - r) = ENNReal.ofReal (|x - y| - r)

For a nonnegative threshold r, the two hinges of a pair of reals add up to the single hinge (|x - y| - r)⁺ of their distance, since at most one of y - x - r and x - y - r is positive.

theorem TauCeti.ofReal_rpow_eq_lintegral_mul_ofReal_sub {p d : ℝ} (hp : 1 < p) (hd : 0 ≤ d) : ENNReal.ofReal (d ^ p) = ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (p * (p - 1) * r ^ (p - 2)) * ENNReal.ofReal (d - r)

Powers are mixtures of hinges. For 1 < p and d ≥ 0, d ^ p = ∫_{r > 0} p (p - 1) r ^ (p - 2) (d - r)⁺ dr.

theorem TauCeti.rpow_eq_lintegral_mul_sub {p : ℝ} (hp : 1 < p) (d : ENNReal) : d ^ p = ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (p * (p - 1) * r ^ (p - 2)) * (d - ENNReal.ofReal r)

Extended powers are mixtures of hinges. For 1 < p and d : ℝ≥0∞, d ^ p = ∫_{r > 0} p (p - 1) r ^ (p - 2) (d - r) dr, with truncated subtraction.

theorem TauCeti.edist_rpow_eq_lintegral {p : ℝ} (hp : 1 < p) (x y : ℝ) : edist x y ^ p = ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (p * (p - 1) * r ^ (p - 2)) * (ENNReal.ofReal (y - x - r) + ENNReal.ofReal (x - y - r))

The power of a distance as a mixture of hinges. For 1 < p, the power |x - y| ^ p is the integral, over the thresholds r > 0 with weight p (p - 1) r ^ (p - 2), of the two hinges (y - x - r)⁺ + (x - y - r)⁺.

theorem TauCeti.lintegral_edist_rpow_eq {p : ℝ} (hp : 1 < p) (m : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.SFinite m] : ∫⁻ (z : ℝ × ℝ), edist z.1 z.2 ^ p ∂m = ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (p * (p - 1) * r ^ (p - 2)) * (∫⁻ (z : ℝ × ℝ), ENNReal.ofReal (z.2 - z.1 - r) ∂m + ∫⁻ (z : ℝ × ℝ), ENNReal.ofReal (z.1 - z.2 - r) ∂m)

The p-th moment of the distance between pairs of real variables, for 1 < p, is the corresponding mixture of their two expected hinge costs.

The signed layer-cake representation of a real number

theorem TauCeti.indicator_Iio_sub_indicator_Iio_zero (a : ℝ) : (fun (t : ℝ) => (Set.Iio a).indicator 1 t - (Set.Iio 0).indicator 1 t) = (Set.Ico 0 a).indicator 1 - (Set.Ico a 0).indicator 1

1_{t < a} - 1_{t < 0}, as a function of t, is the signed indicator of the interval between 0 and a.

theorem TauCeti.integrable_indicator_Iio_sub_indicator_Iio_zero (a : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => (Set.Iio a).indicator 1 t - (Set.Iio 0).indicator 1 t) MeasureTheory.volume

The signed indicator t ↦ 1_{t < a} - 1_{t < 0} is Lebesgue integrable.

@[simp]

theorem TauCeti.integral_indicator_Iio_sub_indicator_Iio_zero (a : ℝ) : ∫ (t : ℝ), (Set.Iio a).indicator 1 t - (Set.Iio 0).indicator 1 t = a

The signed layer-cake representation of a real number: ∫ (1_{t < a} - 1_{t < 0}) dt = a.

@[simp]

theorem TauCeti.integral_abs_indicator_Iio_sub_indicator_Iio_zero (a : ℝ) : ∫ (t : ℝ), |(Set.Iio a).indicator 1 t - (Set.Iio 0).indicator 1 t| = |a|

The L¹ norm of the signed indicator t ↦ 1_{t < a} - 1_{t < 0} is |a|: ∫ |1_{t < a} - 1_{t < 0}| dt = |a|. This is stated with |·|, the simp-normal form of the norm on ℝ, so that simp also evaluates the ‖·‖ form of the integral.

Real-power moments and weighted tails

theorem TauCeti.measurable_weighted_tail {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (f : Ω → ℝ) (p : ℝ) : Measurable fun (t : ℝ) => μ.real {x : Ω | t < f x} * t ^ (p - 1)

The real-valued strict tail weighted by a real power is measurable in the threshold. No measurability of f or finiteness of μ is required.

theorem TauCeti.integrable_rpow_iff_integrableOn_weighted_tail {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} {p : ℝ} (hf : AEMeasurable f μ) (hfn : 0 ≤ᵐ[μ] f) (hp : 0 < p) : MeasureTheory.Integrable (fun (x : Ω) => f x ^ p) μ ↔ MeasureTheory.IntegrableOn (fun (t : ℝ) => μ.real {x : Ω | t < f x} * t ^ (p - 1)) (Set.Ioi 0) MeasureTheory.volume

The layer-cake integrability test for positive real powers on a finite measure space. The function may be nonnegative only almost everywhere.

theorem TauCeti.integrableOn_weighted_tail_Ioc {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p : ℝ} (f : Ω → ℝ) (hp : 0 < p) {b : ℝ} : MeasureTheory.IntegrableOn (fun (t : ℝ) => μ.real {x : Ω | t < f x} * t ^ (p - 1)) (Set.Ioc 0 b) MeasureTheory.volume

On a finite measure space, the tail weighted by t ^ (p - 1) is integrable over every bounded interval (0, b] when 0 < p, without any measurability assumption on f.

theorem TauCeti.integrable_rpow_iff_integrableAtFilter_weighted_tail {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} {p : ℝ} (hf : AEMeasurable f μ) (hfn : 0 ≤ᵐ[μ] f) (hp : 0 < p) : MeasureTheory.Integrable (fun (x : Ω) => f x ^ p) μ ↔ MeasureTheory.IntegrableAtFilter (fun (t : ℝ) => μ.real {x : Ω | t < f x} * t ^ (p - 1)) Filter.atTop MeasureTheory.volume

On a finite measure space, only the behavior of the weighted tail at infinity matters for the existence of a positive real-power moment.

theorem MeasureTheory.Measure.lintegral_Ioi_tail_add (F : Measure NNReal) (x : NNReal) : ∫⁻ (t : ℝ) in Set.Ioi 0, F (Set.Ioi (t.toNNReal + x)) = ∫⁻ (u : NNReal), ↑(u - x) ∂F

The integral of the shifted tail of a half-line measure is the extended integral of its truncated distance above the threshold. No finiteness or normalization is required.

theorem MeasureTheory.Measure.integrableOn_Ioi_measureReal_tail_add (F : Measure NNReal) (x : NNReal) (hmean : ∫⁻ (u : NNReal), ↑u ∂F ≠ ⊤) : IntegrableOn (fun (t : ℝ) => F.real (Set.Ioi (t.toNNReal + x))) (Set.Ioi 0) volume

A finite extended first moment makes every shifted tail integrable on the positive half-line. The measure need not be finite or normalized.