Exact source: MathlibAnnex/MeasureTheory/Measure/EquivalentSeminormBall.lean
Pinned GitHub source · Raw UTF-8 source
Back to Maximal minors scaled by the reference ball volume
1import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Topology2import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar3import Mathlib.MeasureTheory.Measure.OpenPos45/-!6# Lebesgue volume of an equivalent seminorm ball78This API uses the original Lebesgue volume on finite real Pi coordinates.9Its normalization is fixed; the measure is not an arbitrary rescaled Haar measure.10-/1112namespace MathlibAnnex.EquivalentSeminorm1314open MeasureTheory1516variable {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))1718/-- Real Lebesgue volume of the model closed unit ball. -/19noncomputable def closedUnitBallVolume : ℝ := (volume M.closedUnitBall).toReal2021/-- The model ball has finite positive volume, also when `n = 0`. -/22theorem closedUnitBallVolume_pos : 0 < M.closedUnitBallVolume := by23 unfold closedUnitBallVolume24 have hpos : volume M.closedUnitBall ≠ 0 :=25 (MeasureTheory.Measure.measure_pos_of_nonempty_interior volume26 ⟨0, M.zero_mem_interior_closedUnitBall⟩).ne'27 have htop : volume M.closedUnitBall ≠ ⊤ := M.isCompact_closedUnitBall.measure_ne_top28 exact ENNReal.toReal_pos hpos htop2930end MathlibAnnex.EquivalentSeminorm