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

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.