English
In the real coordinate space, the Hausdorff measure with dimension equal to the cardinal of a finite index coincides with the Lebesgue volume.
Русский
В реальном пространстве мера Хаусдорфа с размерностью равной размерности индекса совпадает с Lebesgue-объемом.
LaTeX
$$$\mu_H^{|ι|}(\mathbb{R}^{ι}) = \mathrm{volume}$$$
Lean4
/-- In the space `ι → ℝ`, the Hausdorff measure coincides exactly with the Lebesgue measure. -/
@[simp]
theorem hausdorffMeasure_pi_real {ι : Type*} [Fintype ι] : (μH[Fintype.card ι] : Measure (ι → ℝ)) = volume := by
classical
-- it suffices to check that the two measures coincide on products of rational intervals
refine
(pi_eq_generateFrom (fun _ => Real.borel_eq_generateFrom_Ioo_rat.symm) (fun _ => Real.isPiSystem_Ioo_rat)
(fun _ => Real.finiteSpanningSetsInIooRat _) ?_).symm
simp only [mem_iUnion, mem_singleton_iff]
-- fix such a product `s` of rational intervals, of the form `Π (a i, b i)`.
intro s hs
choose a b H using hs
obtain rfl : s = fun i => Ioo (α := ℝ) (a i) (b i) := funext fun i => (H i).2
replace H := fun i => (H i).1
apply
le_antisymm
_
-- first check that `volume s ≤ μH s`
· have Hle : volume ≤ (μH[Fintype.card ι] : Measure (ι → ℝ)) :=
by
refine le_hausdorffMeasure _ _ ∞ ENNReal.coe_lt_top fun s _ => ?_
rw [ENNReal.rpow_natCast]
exact Real.volume_pi_le_diam_pow s
rw [← volume_pi_pi fun i => Ioo (a i : ℝ) (b i)]
exact
Measure.le_iff'.1 Hle
_
/- For the other inequality `μH s ≤ volume s`, we use a covering of `s` by sets of small diameter
`1/n`, namely cubes with left-most point of the form `a i + f i / n` with `f i` ranging between
`0` and `⌈(b i - a i) * n⌉`. Their number is asymptotic to `n^d * Π (b i - a i)`. -/
have I : ∀ i, 0 ≤ (b i : ℝ) - a i := fun i => by simpa only [sub_nonneg, Rat.cast_le] using (H i).le
let γ := fun n : ℕ => ∀ i : ι, Fin ⌈((b i : ℝ) - a i) * n⌉₊
let t : ∀ n : ℕ, γ n → Set (ι → ℝ) := fun n f => Set.pi univ fun i => Icc (a i + f i / n) (a i + (f i + 1) / n)
have A : Tendsto (fun n : ℕ => 1 / (n : ℝ≥0∞)) atTop (𝓝 0) := by
simp only [one_div, ENNReal.tendsto_inv_nat_nhds_zero]
have B : ∀ᶠ n in atTop, ∀ i : γ n, diam (t n i) ≤ 1 / n :=
by
refine eventually_atTop.2 ⟨1, fun n hn => ?_⟩
intro f
refine diam_pi_le_of_le fun b => ?_
simp only [Real.ediam_Icc, add_div, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), le_refl,
add_sub_add_left_eq_sub, add_sub_cancel_left, ENNReal.ofReal_one, ENNReal.ofReal_natCast]
have C : ∀ᶠ n in atTop, (Set.pi univ fun i : ι => Ioo (a i : ℝ) (b i)) ⊆ ⋃ i : γ n, t n i :=
by
refine eventually_atTop.2 ⟨1, fun n hn => ?_⟩
have npos : (0 : ℝ) < n := Nat.cast_pos.2 hn
intro x hx
simp only [mem_Ioo, mem_univ_pi] at hx
simp only [t, mem_iUnion, mem_univ_pi]
let f : γ n := fun i =>
⟨⌊(x i - a i) * n⌋₊, by
apply Nat.floor_lt_ceil_of_lt_of_pos
· gcongr
exact (hx i).right
· refine mul_pos ?_ npos
simpa only [Rat.cast_lt, sub_pos] using H i⟩
refine ⟨f, fun i => ⟨?_, ?_⟩⟩
·
calc
(a i : ℝ) + ⌊(x i - a i) * n⌋₊ / n ≤ (a i : ℝ) + (x i - a i) * n / n :=
by
gcongr
exact Nat.floor_le (mul_nonneg (sub_nonneg.2 (hx i).1.le) npos.le)
_ = x i := by field_simp; ring
·
calc
x i = (a i : ℝ) + (x i - a i) * n / n := by field_simp; ring
_ ≤ (a i : ℝ) + (⌊(x i - a i) * n⌋₊ + 1) / n := by
gcongr
exact (Nat.lt_floor_add_one _).le
calc
μH[Fintype.card ι] (Set.pi univ fun i : ι => Ioo (a i : ℝ) (b i)) ≤
liminf (fun n : ℕ => ∑ i : γ n, diam (t n i) ^ ((Fintype.card ι) : ℝ)) atTop :=
hausdorffMeasure_le_liminf_sum _ (Set.pi univ fun i => Ioo (a i : ℝ) (b i)) (fun n : ℕ => 1 / (n : ℝ≥0∞)) A t B C
_ ≤ liminf (fun n : ℕ => ∑ i : γ n, (1 / (n : ℝ≥0∞)) ^ Fintype.card ι) atTop :=
by
refine liminf_le_liminf ?_ ?_
· filter_upwards [B] with _ hn
apply Finset.sum_le_sum fun i _ => _
simp only [ENNReal.rpow_natCast]
intro i _
exact pow_le_pow_left' (hn i) _
· isBoundedDefault
_ = liminf (fun n : ℕ => ∏ i : ι, (⌈((b i : ℝ) - a i) * n⌉₊ : ℝ≥0∞) / n) atTop := by
simp only [γ, Finset.card_univ, Nat.cast_prod, one_mul, Fintype.card_fin, Finset.sum_const, nsmul_eq_mul,
Fintype.card_pi, div_eq_mul_inv, Finset.prod_mul_distrib, Finset.prod_const]
_ = ∏ i : ι, volume (Ioo (a i : ℝ) (b i)) :=
by
simp only [Real.volume_Ioo]
apply Tendsto.liminf_eq
refine ENNReal.tendsto_finset_prod_of_ne_top _ (fun i _ => ?_) fun i _ => ?_
· apply
Tendsto.congr' _
((ENNReal.continuous_ofReal.tendsto _).comp
((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))
apply eventually_atTop.2 ⟨1, fun n hn => _⟩
intro n hn
simp only [ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), comp_apply, ENNReal.ofReal_natCast]
· simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]
