English
If f is Hölder on s with exponent r>0 and constants C, then μH^d(f(s)) ≤ C^d μH^{r d}(s) for d ≥ 0.
Русский
Если f является Hölder на s с показателью r>0 и константой C, то для любых d ≥ 0 выполняется μ_H^d(f(s)) ≤ C^d μ_H^{r d}(s).
LaTeX
$$$h :\; \text{HolderOnWith } C\, r\, f\, s \Rightarrow \forall d\ge 0:\; \mu_H^{d}(f''s) \le (C)^{d} \mu_H^{r d}(s)$$$
Lean4
/-- If `f : X → Y` is Hölder continuous on `s` with a positive exponent `r`, then
`μH[d] (f '' s) ≤ C ^ d * μH[r * d] s`. -/
theorem hausdorffMeasure_image_le (h : HolderOnWith C r f s) (hr : 0 < r) {d : ℝ} (hd : 0 ≤ d) :
μH[d] (f '' s) ≤ (C : ℝ≥0∞) ^ d * μH[r * d] s := by
-- We start with the trivial case `C = 0`
rcases (zero_le C).eq_or_lt with (rfl | hC0)
· rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
· simp only [measure_empty, nonpos_iff_eq_zero, mul_zero, image_empty]
have : f '' s = {f x} :=
have : (f '' s).Subsingleton := by simpa [diam_eq_zero_iff] using h.ediam_image_le
(subsingleton_iff_singleton (mem_image_of_mem f hx)).1 this
rw [this]
rcases eq_or_lt_of_le hd with (rfl | h'd)
· simp only [ENNReal.rpow_zero, one_mul, mul_zero]
rw [hausdorffMeasure_zero_singleton]
exact one_le_hausdorffMeasure_zero_of_nonempty ⟨x, hx⟩
· haveI := noAtoms_hausdorff Y h'd
simp only [zero_le, measure_singleton]
-- Now assume `C ≠ 0`
· have hCd0 : (C : ℝ≥0∞) ^ d ≠ 0 := by simp [hC0.ne']
have hCd : (C : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hCd0 hCd, ← ENNReal.tsum_mul_left]
refine iSup_le fun R => iSup_le fun hR => ?_
have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top hr
rcases ENNReal.nhds_zero_basis_Iic.eventually_iff.1 (this.eventually (gt_mem_nhds hR)) with ⟨δ, δ0, H⟩
refine
le_iSup₂_of_le δ δ0 <|
iInf₂_mono' fun t hst ↦
⟨fun n => f '' (t n ∩ s), ?_,
iInf_mono' fun htδ ↦ ⟨fun n => (h.ediam_image_inter_le (t n)).trans (H (htδ n)).le, ?_⟩⟩
· grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]
· refine ENNReal.tsum_le_tsum fun n => ?_
simp only [iSup_le_iff, image_nonempty]
intro hft
simp only [Nonempty.mono ((t n).inter_subset_left) hft, ciSup_pos]
rw [ENNReal.rpow_mul, ← ENNReal.mul_rpow_of_nonneg _ _ hd]
exact ENNReal.rpow_le_rpow (h.ediam_image_inter_le _) hd
