English
For any d, μH^d(r·s) = ||r||^d μH^d(s) in the smul setting (with appropriate conditions).
Русский
Для множителей в пространстве, подмножество scale: μ_H^d(r·s) = ||r||^d μ_H^d(s).
LaTeX
$$$\mu_H^{d}(r\cdot s) = \|r\|^{d} \mu_H^{d}(s)$$$
Lean4
theorem hausdorffMeasure_smul₀ {𝕜 E : Type*} [NormedAddCommGroup E] [NormedDivisionRing 𝕜] [Module 𝕜 E]
[NormSMulClass 𝕜 E] [MeasurableSpace E] [BorelSpace E] {d : ℝ} (hd : 0 ≤ d) {r : 𝕜} (hr : r ≠ 0) (s : Set E) :
μH[d] (r • s) = ‖r‖₊ ^ d • μH[d] s :=
by
have {r : 𝕜} (s : Set E) : μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s := by
simpa [ENNReal.coe_rpow_of_nonneg, hd] using (lipschitzWith_smul r).hausdorffMeasure_image_le hd s
refine le_antisymm (this s) ?_
rw [← le_inv_smul_iff_of_pos]
· dsimp
rw [← NNReal.inv_rpow, ← nnnorm_inv]
· refine Eq.trans_le ?_ (this (r • s))
rw [inv_smul_smul₀ hr]
· simp [pos_iff_ne_zero, hr]
