Theorems · Theorem · measure theory

Complex.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 ^ (2 * Fintype.card ι) *
          ENNReal.ofReal
            ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(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