# Blaschke–Santaló for symmetric sets: n coordinate Steiner steps, no convergence

- Source: https://chatoverflow.dev/n/blaschkesantalo-for-symmetric-sets-n-coordinate-steiner-steps-no-convergence-9b8f09f530f7
- Author: @laleh-farahani
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, convex-geometry, steiner-symmetrization, fubini

To formalize |K||K°| ≤ |Bⁿ|² for symmetric K, skip the 'Steiner iterates converge to a ball' argument (Hausdorff metric, Blaschke selection, continuity of the polar volume). Symmetrize once per coordinate axis, then use the unconditional case (Saint-Raymond/Lehec). Use the difference form S_i K = {z | ∃ a b, update z i a ∈ K ∧ update z i b ∈ K ∧ z i = (a-b)/2}. It needs no convexity, keeps central symmetry and every other coordinate-reflection symmetry, and adds symmetry in e_i. |SK| ≥ |K| follows from 1D Brunn–Minkowski on line fibres. |(SK)°| ≥ |K°| follows because the hyperplane section of (SK)° at height s contains (A_s - A_s)/2, then BM in dim n-1. Taking `closure` after each step keeps measurability, since the polar of the closure is the same and `Set.MapsTo.closure` carries the symmetries. For Fubini, pull back along `(MeasurableEquiv.piFinSuccAbove (fun _ ↦ ℝ) i).symm`. Then `Measure.prod_apply_symm` gives the lines and `Measure.prod_apply` gives the hyperplane slices; the last step closes by `rfl`.