Roadmap to high school geometry

Stream: maths

[Kenny Lau]

Can someone come up with a road map towards proving that the surface area of the standard sphere in R^3 is 4π?

[Kenny Lau]

By standard sphere I mean { x : R^3 | x^2+y^2+z^2=1 }, and by surface area I mean Hausdorff measure 2

[Aaron Liu]

Sphere is docs#Metric.sphere and Hausdorff measure is docs#MeasureTheory.Measure.hausdorffMeasure

[Kenny Lau]

Thanks.

[Kenny Lau]

@Joseph Myers Would you like to add something to this conversation?

[Joseph Myers]

I don't know enough about the measure theory parts of mathlib to know how this should be done once we've sorted out Hausdorff measure normalization.

[Kenny Lau]

The issue is that I've basically only learnt about Lebesgue measure, so I have completely no idea how Hausdorff measure works mathematically at all.

[Kenny Lau]

@Joseph Myers do you know who I should ask?

[Kenny Lau]

I currently have this code:

import Mathlib

open Real MeasureTheory Measure

/-- The standard Lebesgue measure on `ℝ²`. -/
noncomputable abbrev lbMeasure : Measure (ℝ × ℝ) :=
  (Basis.finTwoProd ℝ).addHaar

/-- The unit square. -/
def unitSquare : Set (ℝ × ℝ) :=
  { p | 0 ≤ p.1 ∧ p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1 }

/-- The Lebesgue measure of the unit square is `1`. -/
lemma lbMeasure_unitSquare : lbMeasure unitSquare = 1 := by
  convert (Basis.addHaar_eq_iff (Basis.finTwoProd ℝ) _).1 rfl
  ext p
  simp only [unitSquare, Set.mem_setOf_eq, Basis.coe_parallelepiped, mem_parallelepiped_iff,
    Set.mem_Icc, Fin.sum_univ_two, Fin.isValue, Basis.finTwoProd_zero, Prod.smul_mk, smul_eq_mul,
    mul_one, mul_zero, Basis.finTwoProd_one, Prod.mk_add_mk, add_zero, zero_add, Pi.le_def]
  exact ⟨fun h ↦ ⟨![p.1, p.2], by simp [Fin.forall_fin_succ, h]⟩,
    fun ⟨t, ht⟩ ↦ ht.2 ▸ ⟨ht.1.1 0, ht.1.2 0, ht.1.1 1, ht.1.2 1⟩⟩

[Kenny Lau]

I would like to link this thread to #Is there code for X? > Circumference of a circle / surface area of a sphere . (As in, if you're in this thread, please check out the other thread.)

[Kenny Lau]

What is actually the standard way to write "R^3" in this context?

[Aaron Liu]

Maybe EuclideanSpace ℝ (Fin 3)?

[Aaron Liu]

Or Fin 3 → ℝ, depending on the situation

[Eric Wieser]

I think your lbMeasure is just volume

[Kenny Lau]

Eric Wieser said:

I think your lbMeasure is just volume

I think you might be right. Real.volume_pi_ball:

@[simp]
nonrec theorem volume_pi_ball (a : ι → ℝ) {r : ℝ} (hr : 0 < r) :
    volume (Metric.ball a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by
  simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]
  exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm

[Edward van de Meent]

do note that the metric on ι → ℝ is the maximum of differences of each component, meaning the theorem you're linking tells the volume of a (hyper)cube with edge length 2r. You will probably need to use some WithLp type alias

[Snir Broshi]

EuclideanSpace ℝ (Fin n) aliases WithLp 2 ..., so that's the one

[Snir Broshi]

And the theorem for volume of euclidean balls is EuclideanSpace.volume_ball
Doesn't help with spheres though

[Kenny Lau]

So, here's the knowledge I gathered within yesterday, that I try to summarise for anyone who wants to join in the middle and contribute:

1. We have three canonical normed spaces:

• WithLp p (Fin n → ℝ) which is R^n with the Lp metric.
• EuclideanSpace ℝ (Fin n)which is L2 metric, denoted (ℝ^n, L2)
• Bare Pi type (Fin n → ℝ) with supremum norm, denoted (ℝ^n, sup)

2. Fortunately, nobody cares about Lp, so canonical Lebesgue measure (which is called MeasureTheory.volume, denoted μ) is only defined on (ℝ^n, L2) and (ℝ^n, sup).
3. Hausdorff measure (denoted μH[s]) is also defined on (ℝ^n, L2) and (ℝ^n, sup). (For "newcomers", there is a Hausdorff measure of "dimension s" for any real number s, where e.g. intuitively the s=2 measures "surface area" in ℝ^3.)
4. It can be shown (10 line proof) that the unit n-cube has μ=1 in both (ℝ^n, L2) and (ℝ^n, sup), using OrthonormalBasis.volume_parallelepiped for L2 and [to be done for sup]
5. The unit n-ball in (ℝ^n, L2) has μ = π^(n/2) / Γ(n/2 + 1): EuclideanSpace.volume_ball

• I tried to trace down what the core idea of the proof was, and my current understanding is that it uses the crucial fact that even though a cube and a ball look different, a cube with size r and a ball with radius r both cover the whole space as r → ∞. Of course the volume itself diverges, but if you scale it by exp(-r) then the integral converges, and from that you can transform the volume to an integral on the whole space ℝ^n.

6. We know that the Lebesgue measure on (ℝ^n, L2) and (ℝ^n, sup) are Haar measures. It should be a 1-line proof that the Hausdorff measure on (ℝ^n, L2) and (ℝ^n, sup) with s=n are also Haar measures, using MeasureTheory.isAddHaarMeasure_hausdorffMeasure.
7. It is a 3-line proof that μH[n] = μ for (ℝ^n, sup)! Using MeasureTheory.hausdorffMeasure_pi_real.

[Kenny Lau]

For the convenience of the reader I have summarised the above summary into a table:

image.png

[Kenny Lau]

[I will replace this message with a link to Lean code containing the above information]

[Kenny Lau]

I don't currently have an argument for this yet, but I imagine it would be useful to actually use the Hausdorff measure on L2? So it would be worth it to actually compute the μH[n] of n-cube in L2, which is proved e.g. in Section 2.2 of Evans, Lawrence C.; Gariepy, Ronald F.; Measure theory and fine properties of functions. But is notoriously very involved in the actual calculation.

[Kenny Lau]

If I recall undergrad / A-level maths, I think the surface area was just defined via a parametrisation, (possibly along with a proof that it is independent of parametrisation, maybe differential geometry covers this), rather than via Hausdorff measure!

As in, the surface area of the northern hemisphere would literally defined to be an integral over the unit disc in R^2, and would not be connected at all with the Hausdorff measure!

[Kenny Lau]

image.png

[Kenny Lau]

@Bhavik Mehta @Jz Pan if you're interested ^

[Sébastien Gouëzel]

Kenny Lau said:

2. Fortunately, nobody cares about Lp, so canonical Lebesgue measure (which is called MeasureTheory.volume, denoted μ) is only defined on (ℝ^n, L2) and (ℝ^n, sup).

It's definitely not true that nobody cares about Lp! What is true is that product spaces naturally have a measure (the product measure) and that inner product spaces naturally have a measure (the one that gives measure 1 to any parallelepiped spanned by an orthonormal basis). We didn't define a volume specifically on EuclideanSpace.

[Kenny Lau]

@Sébastien Gouëzel but Lp is not an inner product space right?

[Kenny Lau]

Can you produce the code checking that Lp does have a measure?

[Sébastien Gouëzel]

Looks like I wasn't clear. Lp is not an inner product space (except for p=2), so it doesn't have a volume. What I was saying is that it turns out that, for p=2, Lp has an inner product space structure, so it has a volume, but not because we have given it a special treatment: it benefits from general typeclasses that have been developed elsewhere.

[Kenny Lau]

import Mathlib

variable (n : ℕ) (s : ℝ)

#check MeasureTheory.volume (α := WithLp 3 (Fin n → ℝ)) -- error
#check MeasureTheory.volume (α := EuclideanSpace ℝ (Fin n))
#check MeasureTheory.volume (α := Fin n → ℝ)

#check EuclideanSpace.volume_preserving_measurableEquiv

#check MeasureTheory.Measure.hausdorffMeasure (X := WithLp 3 (Fin n → ℝ)) -- error
#check MeasureTheory.Measure.hausdorffMeasure (X := EuclideanSpace ℝ (Fin n))
#check MeasureTheory.Measure.hausdorffMeasure (X := Fin n → ℝ)


open MeasureTheory Measure


section Haar

example : (volume (α := EuclideanSpace ℝ (Fin n))).IsAddHaarMeasure := inferInstance
example : (volume (α := Fin n → ℝ)).IsAddHaarMeasure := inferInstance

instance : (μH[n] : Measure (EuclideanSpace ℝ (Fin n))).IsAddHaarMeasure := by
  convert isAddHaarMeasure_hausdorffMeasure (E := EuclideanSpace ℝ (Fin n)); simp

instance : (μH[n] : Measure (Fin n → ℝ)).IsAddHaarMeasure := by
  convert inferInstanceAs (volume (α := Fin n → ℝ)).IsAddHaarMeasure
  convert hausdorffMeasure_pi_real; simp

end Haar


section UnitCube

/-- The (closed) unit cube in ℝ^ι, as [0,1]^ι. -/
@[simp] def unitCube (ι : Type*) : Set (ι → ℝ) :=
  { x | ∀ i, x i ∈ Set.Icc 0 1 }

theorem pi_eq_unitCube (ι : Type*) [Fintype ι] :
    Set.univ.pi (fun _ ↦ Set.Icc 0 1) = unitCube ι := by
  ext x; rw [Set.mem_pi]; simp

theorem piIcc01_eq_unit (ι : Type*) [Fintype ι] :
    TopologicalSpace.PositiveCompacts.piIcc01 ι = unitCube ι := by
  rw [← pi_eq_unitCube]; rfl

theorem parallelepiped_eq_unitCube (ι : Type*) [Fintype ι] :
    (Pi.basisFun ℝ ι).parallelepiped = unitCube ι := by
  simp_rw [Basis.coe_parallelepiped, parallelepiped_basis_eq, Pi.basisFun_repr, unitCube]

/-- `μ (unitCube ι) = 1` on `(ℝ^ι, sup)`. -/
theorem volume_unitCube (ι : Type*) [Fintype ι] :
    MeasureTheory.volume (unitCube ι) = 1 := by
  rw [← pi_eq_unitCube, MeasureTheory.volume_pi_pi, Real.volume_Icc]; simp

/-- `μ (unitCube ι) = 1` on `(ℝ^ι, L₂)`. -/
theorem volume_Euclidean_unitCube (ι : Type*) [Fintype ι] :
    MeasureTheory.volume (EuclideanSpace.measurableEquiv ι ⁻¹' unitCube ι) = 1 := by
  rw [(EuclideanSpace.volume_preserving_measurableEquiv ι).measure_preimage_equiv, volume_unitCube]

/-- `μH[n] (unitCube ι) = 1` on `(ℝ^n, sup)`. -/
theorem hausdorffMeasure_unitCube (n : ℕ) :
    μH[n] (unitCube (Fin n)) = 1 := by
  convert volume_unitCube (Fin n); simpa using hausdorffMeasure_pi_real (ι := Fin n)

/-- `μH[n] (unitCube ι)` is positive and finie on `(ℝ^n, L₂)`. -/
theorem hausdorffMeasure_Euclidean_unitCube_pos (n : ℕ) :
    0 < μH[n] (EuclideanSpace.measurableEquiv (Fin n) ⁻¹' unitCube (Fin n)) := by
  rw [← piIcc01_eq_unit, ← MeasurableEquiv.image_symm,
    ← TopologicalSpace.PositiveCompacts.coe_map (by exact continuous_id) (by exact .id)]
  exact measure_pos_of_nonempty_interior _ (TopologicalSpace.PositiveCompacts.interior_nonempty _)

/-- `μH[n] (unitCube ι)` is positive and finie on `(ℝ^n, L₂)`. -/
theorem hausdorffMeasure_Euclidean_unitCube_finite (n : ℕ) :
    μH[n] (EuclideanSpace.measurableEquiv (Fin n) ⁻¹' unitCube (Fin n)) < ⊤ := by
  rw [← piIcc01_eq_unit, ← MeasurableEquiv.image_symm,
    ← TopologicalSpace.PositiveCompacts.coe_map (by exact continuous_id) (by exact .id)]
  exact IsFiniteMeasureOnCompacts.lt_top_of_isCompact
    (TopologicalSpace.PositiveCompacts.isCompact _)

end UnitCube

#check EuclideanSpace.volume_ball

[Kenny Lau]

as promised, here is the Lean code for (most of) the claims above in the above table

[Kenny Lau]

@Sébastien Gouëzel so, my question is, we have a correctly normalised μH[s] on (R^n, sup), then the question is what extra benefit does using μH[s] on (R^n, L2) give us?

[Eric Wieser]

Note that unitCube is Set.Icc 0 1

[Kenny Lau]

Yes, but I thought my definition has better defeq

[Wrenna Robson]

@Kenny Lau Hamming is another canonical normed space.

[Kenny Lau]

but does it have a measure

[Wrenna Robson]

Hmm. docs#Hamming.instNorm

[Wrenna Robson]

So I don't think so probably because it isn't a NormedSpace (except weirdly I think for the underlying field being ZMod 2).

[Wrenna Robson]

In some ways it's like a very weird L0 norm but I'm not sure that's very helpful most of the time.

[Kenny Lau]

you're confusing measure with metric?

[Yaël Dillies]

Of course it has a measure. It's the product measure

[Wrenna Robson]

Kenny Lau said:

you're confusing measure with metric?

Yes - sorry!