Schwarz rearrangement #

For a measure μ on a normed space and f : E → ℝ≥0∞, the Schwarz rearrangement schwarzRearrangement μ f is the radially nonincreasing function whose strict superlevel set {t < f*} is {x | μ (ball 0 ‖x‖) < μ {t < f}}:

schwarzRearrangement μ f x = ⨆ {t | μ (ball 0 ‖x‖) < μ {f > t}}, t.

For an additive Haar measure on a nontrivial finite-dimensional real normed space, a superlevel set of finite measure is the centered open ball with the same measure, while one of infinite measure is the whole space. Equimeasurability also holds in dimension zero. For Lebesgue measure on a Euclidean space this is the symmetric decreasing rearrangement. The definition is made directly from the distribution function t ↦ μ {f > t}, with no measurability, integrability or finiteness hypotheses. For an additive Haar measure, a superlevel set of infinite measure is replaced by the whole space, and one of measure zero by the empty set. Consequently the rearrangement depends only on the a.e. class of f, and it is defined pointwise at every point, so no further choice of representative is involved.

Its strict superlevel sets are {x | μ (ball 0 ‖x‖) < μ {f > t}} (TauCeti.setOf_lt_schwarzRearrangement). For an additive Haar measure on a finite-dimensional real normed space these sets have the same measure as {f > t}: the rearrangement is equimeasurable with f (TauCeti.addHaar_setOf_lt_schwarzRearrangement). For a.e.-measurable f, the layer-cake formula then gives equality of all ∫⁻ f ^ p for 0 < p, hence of every eLpNorm with finite exponent, while equality of essential suprema gives the case p = ∞. Rearrangement is monotone under a.e. inequality, idempotent, and it sends the indicator of a set s to the indicator of {x | μ (ball 0 ‖x‖) < μ s}. In a nontrivial finite-dimensional real normed space with additive Haar measure, this set is the centered open ball of measure μ s when that measure is finite, and the whole space when it is infinite. The Hardy--Littlewood inequality says that rearranging two nonnegative functions can only increase the integral of their product.

Schwarz rearrangement is a contraction for every Lᵖ distance with 1 ≤ p ≤ ∞, measured by the extended distance on ℝ≥0∞. Two rearranged superlevel sets are concentric, so the measure of their difference is the truncated difference of the original level measures. A level-by-level formula for ∫⁻ (f - g) then gives the one-sided L¹ contraction, and writing (f - g) ^ p as a mixture of the hinges f - g - r extends it to 1 < p; adding a constant commutes with rearrangement, which gives the case p = ∞.

Main definitions and results #

TauCeti.schwarzRearrangement: the Schwarz rearrangement of an ℝ≥0∞-valued function.
TauCeti.lt_schwarzRearrangement_iff: its superlevel sets.
TauCeti.measurable_schwarzRearrangement: it is always measurable.
TauCeti.schwarzRearrangement_mono_ae, TauCeti.schwarzRearrangement_congr_ae: order preservation and independence of the representative.
TauCeti.addHaar_setOf_lt_schwarzRearrangement: equimeasurability.
TauCeti.addHaar_inter_setOf_lt_schwarzRearrangement: intersections of two rearranged superlevel sets have the smaller of the original level measures.
TauCeti.lintegral_rpow_schwarzRearrangement, TauCeti.eLpNorm_schwarzRearrangement, TauCeti.memLp_schwarzRearrangement_iff: equality of integrals of powers and of Lᵖ seminorms, and preservation of every Lᵖ class.
MeasureTheory.Integrable.ae_schwarzRearrangement_ofReal_ne_top, MeasureTheory.Integrable.toReal_schwarzRearrangement: almost-everywhere finiteness and integrability of the real-valued rearrangement of the positive part of an integrable function.
TauCeti.lintegral_mul_le_lintegral_schwarzRearrangement_mul: the Hardy--Littlewood rearrangement inequality.
TauCeti.schwarzRearrangement_add_const: rearrangement commutes with adding a constant.
TauCeti.addHaar_sdiff_setOf_lt_schwarzRearrangement: differences of two rearranged superlevel sets have the truncated difference of the original level measures.
TauCeti.lintegral_sub_rpow_schwarzRearrangement_le, TauCeti.lintegral_edist_rpow_schwarzRearrangement_le, TauCeti.edist_schwarzRearrangement_le_essSup, TauCeti.eLpNorm_edist_schwarzRearrangement_le: one-sided and two-sided Lᵖ contraction for 1 ≤ p ≤ ∞.

References #

E. H. Lieb and M. Loss, Analysis, 2nd ed., Graduate Studies in Mathematics 14, AMS, 2001, Sections 3.3--3.5; Theorem 3.5 is the nonexpansivity of rearrangement.