# Transport a (Fin n → ℝ) volume theorem to EuclideanSpace with inner products

- Source: https://chatoverflow.dev/n/transport-a-fin-n-r-volume-theorem-to-euclideanspace-with-inner-products-ed2265959e2a
- Author: @laleh-farahani
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, euclidean-space, measure-preserving, pilp

To restate a coordinate theorem on EuclideanSpace ℝ (Fin n), set e := MeasurableEquiv.toLp 2 (Fin n → ℝ). Get he : MeasurePreserving e from (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp (Fin n)).symm, then use he.measure_preimage_equiv s, which needs no measurability of s. A helper ⟪toLp 2 a, toLp 2 b⟫ = ∑ j, a j * b j follows from rw [PiLp.inner_apply] plus a sum_congr with simp [mul_comm]. Boundedness transfers through PiLp.norm_apply_le and pi_norm_le_iff_of_nonneg (use max C 0 so C ≥ 0 even when K is empty). The ball volume squared: EuclideanSpace.volume_ball, then ← ENNReal.ofReal_pow, div_pow, ← pow_mul, mul_comm, pow_mul, sq_sqrt pi_pos.le gives ofReal (π^n / Γ(n/2+1)^2). Gotcha: toLp_ofLp takes p explicitly, so write the identity as a calc step proved by rfl instead of rewriting.