Mathlib Map

Theorems · Theorem · measure theory

Complex.volume_sum_rpow_lt_one

∀ (ι : Type u_1) [inst : Fintype ι] {p : ℝ},
  1 ≤ p →
    MeasureTheory.volume {x | ∑ i, ‖x i‖ ^ p < 1} =
      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 289 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Fintype
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Complex.volume_sum_rpow_lt · cited by 1Complex.volume_sum_rpow_ltDFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetReal · cited by 25697RealMeasureTheory.Measure · cited by 10939MeasureTheory.MeasureENNReal · cited by 9879ENNRealFintype · cited by 7736FintypeSet.ofPred · cited by 6101Set.ofPredComplex · cited by 5565ComplexNorm.norm · cited by 5413Norm.normFinset.sum · cited by 5195Finset.sumFinset.univ · cited by 3473Finset.univFact · cited by 2726FactNat.cast_one · cited by 2501Nat.cast_oneFinset.card · cited by 2327Finset.cardFinset.sum_congr · cited by 2323Finset.sum_congrComplex.volume_sum_rpow_lt_oneCITED BYCITES

Cites61

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coestatement and proof · cited by 62,936
  • Setstatement and proof · cited by 53,352
  • Realstatement and proof · cited by 25,697
  • MeasureTheory.Measurestatement and proof · cited by 10,939
  • ENNRealstatement and proof · cited by 9,879
  • Fintypestatement and proof · cited by 7,736
  • Set.ofPredstatement and proof · cited by 6,101
  • Complexstatement and proof · cited by 5,565
  • Norm.normstatement and proof · cited by 5,413
  • Finset.sumstatement and proof · cited by 5,195
  • Finset.univstatement and proof · cited by 3,473
  • Factproof · cited by 2,726

Cited by1

Results whose statement or proof uses this declaration.