English
Under suitable regularity of g, the sublevel measure equality μ({g ≤ r}) = μ({g < r}) holds for all r.
Русский
При подходящей регулярности функции g верно равенство меры подуровня μ({g ≤ r}) = μ({g < r}) для всех r.
LaTeX
$$$\mu\{ x : g(x) \le r \} = \mu\{ x : g(x) < r \}$$$
Lean4
theorem volume_ball (x : E) (r : ℝ) :
volume (Metric.ball x r) = (.ofReal r) ^ finrank ℝ E * .ofReal (√π ^ finrank ℝ E / Gamma (finrank ℝ E / 2 + 1)) :=
by
rw [← ((stdOrthonormalBasis ℝ E).measurePreserving_repr_symm).measure_preimage measurableSet_ball.nullMeasurableSet]
have : Nonempty (Fin (finrank ℝ E)) := Fin.pos_iff_nonempty.mp finrank_pos
have := EuclideanSpace.volume_ball (Fin (finrank ℝ E)) ((stdOrthonormalBasis ℝ E).repr x) r
simp_rw [Fintype.card_fin] at this
convert this
simp only [LinearIsometryEquiv.preimage_ball, LinearIsometryEquiv.symm_symm]
