Steiner symmetrization of Lebesgue-measurable sets

Steiner symmetrization in a unit direction replaces each parallel line section by the open centered interval of the same length. We use extended-radius balls in ℝ: a null section becomes empty and an infinite-length section becomes the whole line. Thus the construction is defined without boundedness or finiteness assumptions.

The symmetral of a Lebesgue-measurable set is Lebesgue-measurable and has the same volume. It is independent, up to null sets, of the input representative. Symmetrization is monotone, idempotent, and contracts the volume of symmetric differences, equivalently the L¹ distance between indicators. The contraction permits approximation of arbitrary measurable sets before iterating symmetrizations.

Membership has a coordinate-free form: x lies in the symmetral exactly when |⟪e, x⟫| is less than half the length of the line section through x. From it we obtain the covariance laws. Translating the input translates the symmetral by the component of the translation orthogonal to e, so translations along e have no effect. Nonzero dilations commute with symmetrization, and a linear isometric equivalence carries the symmetral in direction e to the symmetral of the image in the image direction. Finally, symmetrization preserves convexity: by the one-dimensional Brunn–Minkowski inequality, section lengths of a convex set are concave along segments joining points with nonempty sections.

The normalization uses Real.volume_eball and the measure-preserving orthogonal coordinates from TauCeti.MeasureTheory.Measure.Lebesgue.OrthogonalSlices.

def TauCeti.steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) : Set E

Steiner symmetrization along the unit direction e, centered on its orthogonal hyperplane. The section of length ℓ is the open centered interval of radius ℓ / 2; this includes empty intervals for ℓ = 0 and the whole line for ℓ = ∞.

theorem TauCeti.steinerSymmetrization_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) : steinerSymmetrization e he s = {x : E | ((orthogonalLineEquiv e he).symm x).2 ∈ Metric.eball 0 (MeasureTheory.volume {t : ℝ | ↑((orthogonalLineEquiv e he).symm x).1 + t • e ∈ s} / 2)}

The coordinate description of a Steiner symmetral.

@[simp]

theorem TauCeti.mem_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) (y : ↥(ℝ ∙ e)ᗮ) (t : ℝ) : ↑y + t • e ∈ steinerSymmetrization e he s ↔ t ∈ Metric.eball 0 (MeasureTheory.volume {u : ℝ | ↑y + u • e ∈ s} / 2)

Membership in a Steiner symmetral in orthogonal line coordinates.

theorem TauCeti.lineSection_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) (y : ↥(ℝ ∙ e)ᗮ) : {t : ℝ | ↑y + t • e ∈ steinerSymmetrization e he s} = Metric.eball 0 (MeasureTheory.volume {t : ℝ | ↑y + t • e ∈ s} / 2)

Every parallel section of the symmetral is the centered interval of the prescribed length.

theorem TauCeti.volume_lineSection_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) (y : ↥(ℝ ∙ e)ᗮ) : MeasureTheory.volume {t : ℝ | ↑y + t • e ∈ steinerSymmetrization e he s} = MeasureTheory.volume {t : ℝ | ↑y + t • e ∈ s}

Symmetrization preserves the length of every parallel section, even infinite ones.

theorem TauCeti.ordConnected_lineSection_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) (y : ↥(ℝ ∙ e)ᗮ) : {t : ℝ | ↑y + t • e ∈ steinerSymmetrization e he s}.OrdConnected

All parallel sections of a Steiner symmetral are intervals.

@[simp]

theorem TauCeti.steinerSymmetrization_idem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) : steinerSymmetrization e he (steinerSymmetrization e he s) = steinerSymmetrization e he s

Applying the same Steiner symmetrization twice has no further effect.

theorem TauCeti.steinerSymmetrization_mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) : Monotone (steinerSymmetrization e he)

Steiner symmetrization preserves inclusion.

@[simp]

theorem TauCeti.steinerSymmetrization_empty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) : steinerSymmetrization e he ∅ = ∅

@[simp]

theorem TauCeti.steinerSymmetrization_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) : steinerSymmetrization e he Set.univ = Set.univ

theorem TauCeti.mem_steinerSymmetrization_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) (x : E) : x ∈ steinerSymmetrization e he s ↔ inner ℝ e x ∈ Metric.eball 0 (MeasureTheory.volume {t : ℝ | x + t • e ∈ s} / 2)

Coordinate-free membership in a Steiner symmetral: the longitudinal coordinate ⟪e, x⟫ lies in the centered interval whose length is that of the line section through x.

theorem TauCeti.steinerSymmetrization_vadd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (v : E) (s : Set E) : steinerSymmetrization e he (v +ᵥ s) = (v - inner ℝ e v • e) +ᵥ steinerSymmetrization e he s

Translating the input translates the symmetral by the component of the translation orthogonal to the direction.

@[simp]

theorem TauCeti.steinerSymmetrization_smul_vadd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (c : ℝ) (s : Set E) : steinerSymmetrization e he (c • e +ᵥ s) = steinerSymmetrization e he s

Translation along the direction of symmetrization does not change the symmetral.

theorem TauCeti.steinerSymmetrization_vadd_of_inner_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) {v : E} (hv : inner ℝ e v = 0) (s : Set E) : steinerSymmetrization e he (v +ᵥ s) = v +ᵥ steinerSymmetrization e he s

Translation orthogonal to the direction of symmetrization commutes with symmetrization.

theorem TauCeti.steinerSymmetrization_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) {c : ℝ} (hc : c ≠ 0) (s : Set E) : steinerSymmetrization e he (c • s) = c • steinerSymmetrization e he s

Steiner symmetrization commutes with nonzero dilations.

theorem TauCeti.steinerSymmetrization_image_linearIsometryEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (e : E) (he : ‖e‖ = 1) (L : E ≃ₗᵢ[ℝ] F) (s : Set E) : steinerSymmetrization (L e) ⋯ (⇑L '' s) = ⇑L '' steinerSymmetrization e he s

Steiner symmetrization is equivariant under linear isometric equivalences, which move the direction of symmetrization along with the set.

@[simp]

theorem TauCeti.preimage_reflection_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) (s : Set E) : ⇑(ℝ ∙ e)ᗮ.reflection ⁻¹' steinerSymmetrization e he s = steinerSymmetrization e he s

A Steiner symmetral is symmetric under the reflection in the hyperplane orthogonal to the direction of symmetrization.

theorem TauCeti.convex_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E) (he : ‖e‖ = 1) {s : Set E} (hs : Convex ℝ s) : Convex ℝ (steinerSymmetrization e he s)

Steiner symmetrization preserves convexity.

theorem TauCeti.measurableSet_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (e : E) (he : ‖e‖ = 1) {s : Set E} (hs : MeasurableSet s) : MeasurableSet (steinerSymmetrization e he s)

Borel sets have Borel Steiner symmetrals, without a finite-dimensionality assumption.

theorem TauCeti.steinerSymmetrization_ae_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (he : ‖e‖ = 1) {s u : Set E} (h : s =ᵐ[MeasureTheory.volume] u) : steinerSymmetrization e he s =ᵐ[MeasureTheory.volume] steinerSymmetrization e he u

Replacing the input by an a.e. equal set changes the symmetral only on a null set.

theorem TauCeti.nullMeasurableSet_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (he : ‖e‖ = 1) {s : Set E} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) : MeasureTheory.NullMeasurableSet (steinerSymmetrization e he s) MeasureTheory.volume

Steiner symmetrization preserves Lebesgue measurability.

@[simp]

theorem TauCeti.volume_steinerSymmetrization {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (he : ‖e‖ = 1) {s : Set E} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) : MeasureTheory.volume (steinerSymmetrization e he s) = MeasureTheory.volume s

Steiner symmetrization preserves volume, with no boundedness or finiteness assumptions.

theorem TauCeti.volume_steinerSymmetrization_sdiff_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (he : ‖e‖ = 1) {s u : Set E} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume) : MeasureTheory.volume (steinerSymmetrization e he s \ steinerSymmetrization e he u) ≤ MeasureTheory.volume (s \ u)

Steiner symmetrization contracts the volume of one-sided differences.

theorem TauCeti.volume_steinerSymmetrization_symmDiff_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (he : ‖e‖ = 1) {s u : Set E} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume) : MeasureTheory.volume (symmDiff (steinerSymmetrization e he s) (steinerSymmetrization e he u)) ≤ MeasureTheory.volume (symmDiff s u)

The volume of the symmetric difference, or L¹ distance between indicators, does not increase under Steiner symmetrization. Infinite-volume inputs are permitted.

theorem TauCeti.eLpNorm_indicator_steinerSymmetrization_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (e : E) (he : ‖e‖ = 1) {s u : Set E} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume) : MeasureTheory.eLpNorm (((steinerSymmetrization e he s).indicator fun (x : E) => 1) - (steinerSymmetrization e he u).indicator fun (x : E) => 1) 1 MeasureTheory.volume ≤ MeasureTheory.eLpNorm ((s.indicator fun (x : E) => 1) - u.indicator fun (x : E) => 1) 1 MeasureTheory.volume

The L¹ seminorm distance between real indicators contracts under Steiner symmetrization.