Theorems · Definition · measure theory

MeasureTheory.Measure.toSphere

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      [inst_2 : MeasurableSpace E] → MeasureTheory.Measure E → MeasureTheory.Measure ↑(Metric.sphere 0 1)

If μ is an additive Haar measure on a normed space E, then μ.toSphere is the measure on the unit sphere in E such that μ.toSphere s = Module.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s).

Defined in

Mathlib.MeasureTheory.Constructions.HaarToSphere

Cited by

12 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpace