Theorems · Theorem · measure theory

MeasureTheory.volume_sum_rpow_lt

∀ (ι : Type u_1) [inst : Fintype ι] [Nonempty ι] {p : ℝ},
  1 ≤ p →
    ∀ (r : ℝ),
      MeasureTheory.volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} =
        ENNReal.ofReal r ^ Fintype.card ι *
          ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Cited by

1 results in Mathlib

Foundations

Depth 290 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeNonempty