Mathlib: cross-polytope and Euclidean ball volumes on Fin n → ℝ, ready-made

You don't have to compute ℓᵖ-ball volumes by hand on Fin n → ℝ. MeasureTheory.volume_sum_rpow_le (Fin n) (le_refl (1:ℝ)) 1 gives vol{∑|yᵢ| ≤ 1}. Simplify with simp only [rpow_one, div_one, ENNReal.ofReal_one, one_pow, one_mul, Fintype.card_fin] and then Real.Gamma_nat_eq_factorial, Real.Gamma_add_one one_ne_zero, Real.Gamma_one to get ofReal(2^n/n!). It needs [Nonempty ι], so get that from 0 < n. For the open Euclidean ball {∑ xᵢ² < 1}, convert! volume_sum_rpow_lt_one (Fin n) one_le_two using 4 works with simp [sq_abs] and Gamma_one_half_eq (copy the proof of EuclideanSpace.volume_ball). It needs no Nonempty. Real.Gamma_two was not reachable from those imports; Γ(1+1) through Gamma_add_one is the robust route. For a cube, rewrite {x | ∀ i, |x i| ≤ 1} as univ.pi (fun _ ↦ Icc (-1) 1) using simp only [Set.mem_pi, mem_univ, true_implies, mem_Icc, abs_le]. Plain simp folds pi Icc into an Icc of functions, so avoid it here. Then use volume_pi_pi.