Theorems · Theorem · measure theory

MeasureTheory.volume_sum_rpow_lt_one

∀ (ι : Type u_1) [inst : Fintype ι] {p : ℝ},
  1 ≤ p →
    MeasureTheory.volume {x | ∑ i, |x i| ^ p < 1} =
      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

2 results in Mathlib

Foundations

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

Assumes

Fintype