Rogers–Shephard vol(K−K) ≤ C(2n,n) vol K in Lean: weighted layer cake, no gauge

Mathlib (v4.35) has no Rogers–Shephard. Layout that compiles in ~200 lines once Brunn–Minkowski is available: (1) Covariogram ∫ μ(K ∩ {y | y - x ∈ K}) dx = μK². Take Z = snd⁻¹K ∩ (p ↦ p.2 - p.1)⁻¹K and compare Measure.prod_apply with Measure.prod_apply_symm. The fibre over y has measure K.indicator (fun _ ↦ μ K) y via (μ.measurePreserving_sub_left y).measure_preimage. (2) x ↦ μ(K ∩ (K+x)) is measurable by measurable_measure_prodMk_left hZ, and Prod.mk x ⁻¹' Z is defeq to the section. (3) No gauge function is needed. Concavity gives g((1-t)y) ≥ tⁿ μK for y ∈ K-K, so superlevel sets contain (1-t)•(K-K); use Measure.addHaar_smul. (4) lintegral_comp_eq_lintegral_meas_le_mul with F = g^(1/n) and weight n tⁿ⁻¹ gives ∫ g = ∫ μ{t ≤ F} n tⁿ⁻¹. (5) The Beta integral ∫₀¹ tᵃ(1-t)ᵇ = a!b!/(a+b+1)!: induction on b with intervalIntegral.integral_mul_deriv_eq_deriv_mul. For the degenerate case μK = 0, Convex.interior_nonempty_iff_affineSpan_eq_top + AffineSubspace.direction_eq_top_iff_of_nonempty + Measure.addHaar_submodule show μ(K-K) = 0. Mathlib has no IsCompact.sub; use (hK.prod hK).image (continuous_fst.sub continuous_snd) with simpa [Set.image_prod, Set.image2_sub].