Outer regularity of Hausdorff measure

Stream: Is there code for X?

[Bhavik Mehta]

Do we have a proof that the Hausdorff measure is outer regular (docs#MeasureTheory.Measure.OuterRegular)?

[Aaron Liu]

For docs#MeasureTheory.Measure.hausdorffMeasure, I don't think it is in general. Are you maybe thinking of a special case?

[Bhavik Mehta]

It's a pretty standard result as far as I can tell: https://math.stackexchange.com/questions/3632955/is-hausdorff-measure-regular, https://math.stackexchange.com/questions/128085/is-the-hausdorff-outer-measure-regular

[Bhavik Mehta]

It's also in standard textbooks on this, eg Falconer Geometry of Fractal Sets

[Aaron Liu]

I took a look at the stackexchange posts, these seem to be proving slightly different things.

[Kalle Kytölä]

I'm not aware of it exactly in that form, but I think results around docs#instHasOuterApproxClosedOfPseudoMetrizableSpace should hopefully be of some use. I see that the type classes don't match exactly, though: the above requires docs#PseudoMetrizableSpace whereas docs#MeasureTheory.Measure.hausdorffMeasure has docs#EMetricSpace. And local finiteness presumably needs to be used, too (I used this so far only for finite measures). [UPDATE: And maybe there are a few further steps, so after all these may not shorten a direct proof by a lot.]

[Bhavik Mehta]

Unfortunately I don't have local finiteness here either...

[Aaron Liu]

Bhavik Mehta said:

It's a pretty standard result as far as I can tell: https://math.stackexchange.com/questions/3632955/is-hausdorff-measure-regular, https://math.stackexchange.com/questions/128085/is-the-hausdorff-outer-measure-regular

I seem to have disproved it here?

import Mathlib

open MeasureTheory Measure

example : ¬(μH[0] : Measure ℝ).OuterRegular := by
  intro h
  apply OuterRegular.outerRegular at h
  specialize h (measurableSet_singleton 0) 2
  rw [hausdorffMeasure_zero_singleton] at h
  specialize h (by norm_num)
  obtain ⟨U, hU, ho, h2⟩ := h
  obtain h0 | hinf := hausdorffMeasure_zero_or_top zero_lt_one U
  · rw [hausdorffMeasure_real, ho.measure_zero_iff_eq_empty] at h0
    simp [h0] at hU
  · simp [hinf] at h2

[Yaël Dillies]

Yes, it won't be outer-regular according to the usual topology. You will need to take a topology where lower-dimensional sets are open

[Bhavik Mehta]

Aaron Liu said:

Bhavik Mehta said:

It's a pretty standard result as far as I can tell: https://math.stackexchange.com/questions/3632955/is-hausdorff-measure-regular, https://math.stackexchange.com/questions/128085/is-the-hausdorff-outer-measure-regular

I seem to have disproved it here?

import Mathlib

open MeasureTheory Measure

example : ¬(μH[0] : Measure ℝ).OuterRegular := by
  intro h
  apply OuterRegular.outerRegular at h
  specialize h (measurableSet_singleton 0) 2
  rw [hausdorffMeasure_zero_singleton] at h
  specialize h (by norm_num)
  obtain ⟨U, hU, ho, h2⟩ := h
  obtain h0 | hinf := hausdorffMeasure_zero_or_top zero_lt_one U
  · rw [hausdorffMeasure_real, ho.measure_zero_iff_eq_empty] at h0
    simp [h0] at hU
  · simp [hinf] at h2

Ah, I should have said that I can assume s > 0 :)

[Bhavik Mehta]

Ah, I instead need to weaken to Gdelta (in the usual topology) rather than open, that's what was missing

[Bhavik Mehta]

And now this result is sorry-free (it turned out I can allow s = 0 too!)

example {s : ℝ} (hs : 0 ≤ s) (E : Set X) :
    ∃ G : Set X, IsGδ G ∧ E ⊆ G ∧ μH[s] G = μH[s] E := by