Commit 2023-11-13 17:14 69a0d133

View on Github →

feat: polar coords integral in a normed space (#7693)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

added theorem Ioo_smul_sphere_zero

added theorem set_smul_sphere_zero

Created Mathlib/Analysis/NormedSpace/SphereNormEquiv.lean

Modified Mathlib/LinearAlgebra/Finrank.lean

Created Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

added def MeasureTheory.Measure.finiteSpanningSetsIn_volumeIoiPow_range_Iio

added theorem MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd

added def MeasureTheory.Measure.toSphere

added theorem MeasureTheory.Measure.toSphere_apply'

added theorem MeasureTheory.Measure.toSphere_apply_aux

added theorem MeasureTheory.Measure.toSphere_apply_univ'

added theorem MeasureTheory.Measure.toSphere_apply_univ

added def MeasureTheory.Measure.volumeIoiPow

added theorem MeasureTheory.Measure.volumeIoiPow_apply_Iio

added theorem MeasureTheory.integral_fun_norm_addHaar

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.apply_eq_zero_of_isEmpty

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

deleted theorem Metric.sphere_isEmpty_of_subsingleton