File tree Expand file tree Collapse file tree
Mathlib/Geometry/Euclidean/Volume Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -71,9 +71,9 @@ scoped[MeasureTheory] notation "μHE[" d "]" => MeasureTheory.Measure.euclideanH
7171/-- show the scaling factor equals to the ratio between the volume of `d`-dimensional
7272`Metric.ball` with Euclidean metric and with sup metric (i.e. a cube), or explicity,
7373$\pi^{d/2} / (2^d \Gamma (d/2+1))$. -/
74- proof_wanted MeasureTheory.Measure.addHaarScalarFactor_hausdorffMeasure_eq (d : ℕ):
75- addHaarScalarFactor (volume : Measure (EuclideanSpace ℝ (Fin d))) μH[d] =
76- volume (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1 ) / volume (Metric.ball (0 : Fin d -> ℝ) 1 )
74+ proof_wanted MeasureTheory.Measure.addHaarScalarFactor_hausdorffMeasure_eq (d : ℕ) :
75+ addHaarScalarFactor (volume : Measure (EuclideanSpace ℝ (Fin d))) μH[d] =
76+ volume (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1 ) / volume (Metric.ball (0 : Fin d -> ℝ) 1 )
7777
7878theorem MeasureTheory.Measure.euclideanHausdorffMeasure_def (d : ℕ) :
7979 (μHE[d] : Measure X) =
You can’t perform that action at this time.
0 commit comments