English
Same as Volume ClosedBall, for a finite index ι and radius r ≥ 0, vol of the product of closed balls equals ENNReal.ofReal((2r)^{|ι|}).
Русский
Аналогично Volume ClosedBall: для конечного индекса и радиуса r ≥ 0 объём произведения закрытых шаров равен ENNReal.ofReal((2r)^{|ι|}).
LaTeX
$$$$ \\mathrm{volume}(\\mathrm{Metric.closedBall}\\ a\\ r) = \\mathrm{ENNReal.ofReal}((2 \\cdot r)^{|\\iota|}). $$$$
Lean4
/-- A transvection preserves Lebesgue measure. -/
theorem volume_preserving_transvectionStruct [DecidableEq ι] (t : TransvectionStruct ι ℝ) :
MeasurePreserving (toLin' t.toMatrix) := by
/- We use `lmarginal` to conveniently use Fubini's theorem.
Along the coordinate where there is a shearing, it acts like a
translation, and therefore preserves Lebesgue. -/
have ht : Measurable (toLin' t.toMatrix) := (toLin' t.toMatrix).continuous_of_finiteDimensional.measurable
refine ⟨ht, ?_⟩
refine (pi_eq fun s hs ↦ ?_).symm
have h2s : MeasurableSet (univ.pi s) := .pi countable_univ fun i _ ↦ hs i
simp_rw [← pi_pi, ← lintegral_indicator_one h2s]
rw [lintegral_map (measurable_one.indicator h2s) ht, volume_pi]
refine lintegral_eq_of_lmarginal_eq { t.i } ((measurable_one.indicator h2s).comp ht) (measurable_one.indicator h2s) ?_
simp_rw [lmarginal_singleton]
ext x
cases t with
| mk t_i t_j t_hij t_c =>
simp [transvection, single_mulVec, t_hij.symm, ← Function.update_add,
lintegral_add_right_eq_self fun xᵢ ↦ indicator (univ.pi s) 1 (Function.update x t_i xᵢ)]
