English
For any d > 0, the Hausdorff measure μH[d] has no atoms.
Русский
Для любого d > 0 хаусдорфова мера μH[d] не имеет атомов.
LaTeX
$$$ \text{NoAtoms }(μH[d]) $$$
Lean4
/-- If `d₁ < d₂`, then for any set `s` we have either `μH[d₂] s = 0`, or `μH[d₁] s = ∞`. -/
theorem hausdorffMeasure_zero_or_top {d₁ d₂ : ℝ} (h : d₁ < d₂) (s : Set X) : μH[d₂] s = 0 ∨ μH[d₁] s = ∞ :=
by
by_contra! H
suffices ∀ c : ℝ≥0, c ≠ 0 → μH[d₂] s ≤ c * μH[d₁] s
by
rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩
exact hc.not_ge (this c (pos_iff_ne_zero.1 hc0))
intro c hc
refine le_iff'.1 (mkMetric_mono_smul ENNReal.coe_ne_top (mod_cast hc) ?_) s
have : 0 < ((c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) :=
by
rw [← ENNReal.coe_rpow_of_ne_zero hc, pos_iff_ne_zero, Ne, ENNReal.coe_eq_zero, NNReal.rpow_eq_zero_iff]
exact mt And.left hc
filter_upwards [Ico_mem_nhdsGE this]
rintro r ⟨hr₀, hrc⟩
lift r to ℝ≥0 using ne_top_of_lt hrc
rw [Pi.smul_apply, smul_eq_mul, ←
ENNReal.div_le_iff_le_mul (Or.inr ENNReal.coe_ne_top) (Or.inr <| mt ENNReal.coe_eq_zero.1 hc)]
rcases eq_or_ne r 0 with (rfl | hr₀)
· rcases lt_or_ge 0 d₂ with (h₂ | h₂)
· simp only [h₂, ENNReal.zero_rpow_of_pos, zero_le, ENNReal.zero_div, ENNReal.coe_zero]
· simp only [h.trans_le h₂, ENNReal.div_top, zero_le, ENNReal.zero_rpow_of_neg, ENNReal.coe_zero]
· have : (r : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using hr₀
rw [← ENNReal.rpow_sub _ _ this ENNReal.coe_ne_top]
refine (ENNReal.rpow_lt_rpow hrc (sub_pos.2 h)).le.trans ?_
rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]
