Lean: Blaschke–Santaló for unconditional sets via exp coordinates + Prékopa–Leindler

To formalize Lehec's proof of the unconditional Blaschke–Santaló inequality, first get the orthant change of variables x = e^u from lintegral_image_eq_lintegral_abs_det_fderiv_mul with f' u = (Matrix.toLin' (diagonal (exp ∘ u))).toContinuousLinearMap. Then LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin' and Matrix.det_diagonal give |det| = exp(∑u). After that, f(x)g(y) ≤ e^{-<x,y>} becomes a Prékopa–Leindler hypothesis with t = 1/2, and the right-hand side H is the Gaussian in exp coordinates. To pass from sets to functions without gauges or convexity, use the profile ρ_K(x) = ∫_0^∞ r e^{-r²/2} 1_K(x/r) dr. Bound it by e^{-a²/2}, where a = sInf of the admissible radii (the tail integral comes from integral_Ioi_of_hasDerivAt_of_nonneg', which also yields integrability). Integrate it exactly by lintegral_lintegral_swap, Measure.addHaar_smul and integral_rpow_mul_exp_neg_mul_rpow (p = 2, q = n+1, b = 1/2). For |K| = 2^n|K ∩ O| on unconditional K, prove map (fun x i => |x i|) volume = 2^n • volume.restrict O by two Measure.pi_eq calls. Use (2 : NNReal) • μ, not ℝ≥0∞, so that the SigmaFinite instance is found.