English
If f is antilipschitz with constant K, then μH^d(f^{-1}(s)) ≤ K^d μH^d(s).
Русский
Если f является антиподвижной с константой K, то μ_H^d(f^{-1}(s)) ≤ K^d μ_H^d(s).
LaTeX
$$$\mu_H^{d}(f^{-1}(s)) \le (K)^{d} \mu_H^{d}(s)$$$
Lean4
theorem hausdorffMeasure_preimage_le (hf : AntilipschitzWith K f) (hd : 0 ≤ d) (s : Set Y) :
μH[d] (f ⁻¹' s) ≤ (K : ℝ≥0∞) ^ d * μH[d] s :=
by
rcases eq_or_ne K 0 with (rfl | h0)
· rcases eq_empty_or_nonempty (f ⁻¹' s) with (hs | ⟨x, hx⟩)
· simp only [hs, measure_empty, zero_le]
have : f ⁻¹' s = { x } := by
haveI : Subsingleton X := hf.subsingleton
have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)
exact (subsingleton_iff_singleton hx).1 this
rw [this]
rcases eq_or_lt_of_le hd with (rfl | h'd)
· simp only [ENNReal.rpow_zero, one_mul]
rw [hausdorffMeasure_zero_singleton]
exact one_le_hausdorffMeasure_zero_of_nonempty ⟨f x, hx⟩
· haveI := noAtoms_hausdorff X h'd
simp only [zero_le, measure_singleton]
have hKd0 : (K : ℝ≥0∞) ^ d ≠ 0 := by simp [h0]
have hKd : (K : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hKd0 hKd, ← ENNReal.tsum_mul_left]
refine iSup₂_le fun ε ε0 => ?_
refine le_iSup₂_of_le (ε / K) (by simp [ε0.ne']) ?_
refine le_iInf₂ fun t hst => le_iInf fun htε => ?_
replace hst : f ⁻¹' s ⊆ _ := preimage_mono hst; rw [preimage_iUnion] at hst
refine iInf₂_le_of_le _ hst (iInf_le_of_le (fun n => ?_) ?_)
· exact (hf.ediam_preimage_le _).trans (ENNReal.mul_le_of_le_div' <| htε n)
· refine ENNReal.tsum_le_tsum fun n => iSup_le_iff.2 fun hft => ?_
simp only [nonempty_of_nonempty_preimage hft, ciSup_pos]
rw [← ENNReal.mul_rpow_of_nonneg _ _ hd]
exact ENNReal.rpow_le_rpow (hf.ediam_preimage_le _) hd
