English
If x is a function from an index set ι to ℝ and r > 0, then the Hausdorff dimension of the ball around x with radius r equals the cardinality of ι, i.e., dim_H(B(x,r)) = |ι|.
Русский
Пусть x ∈ ι → ℝ и r > 0. Тогда размерность Хаусдорфа шарa вокруг x радиуса r равна кардиналу множества ι: dim_H(B(x,r)) = |ι|.
LaTeX
$$$\\dim_H(\\mathrm{Ball}(x,r)) = |\\iota|$$$
Lean4
theorem dimH_ball_pi (x : ι → ℝ) {r : ℝ} (hr : 0 < r) : dimH (Metric.ball x r) = Fintype.card ι :=
by
cases isEmpty_or_nonempty ι
· rwa [dimH_subsingleton, eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff]
exact fun x _ y _ => Subsingleton.elim x y
· rw [← ENNReal.coe_natCast]
have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by
rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]
refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_ <;> rw [NNReal.coe_natCast, this]
· simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)]
· exact ENNReal.ofReal_ne_top
