English
The function thickenedIndicator δ_pos E is Lipschitz with constant δ^{-1} (in NNReal sense).
Русский
Функция thickenedIndicator δ_pos E является равномерно непрерывной (липшицевой) с константой δ^{-1} в смысле NNReal.
LaTeX
$$$\text{LipschitzWith}(δ^{-1},\, \operatorname{thickenedIndicator}(δ,E))$$$
Lean4
theorem lipschitzWith_thickenedIndicator {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) :
LipschitzWith δ.toNNReal⁻¹ (thickenedIndicator δ_pos E) :=
by
intro x y
wlog h : infEdist x E ≤ infEdist y E generalizing x y
· specialize this y x (le_of_not_ge h)
rwa [edist_comm, edist_comm x]
simp_rw [edist_dist, NNReal.dist_eq, thickenedIndicator_apply, coe_toNNReal_eq_toReal]
rw [← ENNReal.toReal_sub_of_le (thickenedIndicatorAux_mono_infEdist _ h) (by finiteness)]
simp only [thickenedIndicatorAux, abs_toReal, ne_eq, sub_eq_top_iff, one_ne_top, false_and, not_false_eq_true,
and_true, ofReal_toReal]
rw [ENNReal.coe_inv (by simp [δ_pos]), ENNReal.ofReal, div_eq_mul_inv, div_eq_mul_inv]
by_cases h_le : infEdist y E * (↑δ.toNNReal)⁻¹ ≤ 1
·
calc
1 - infEdist x E * (↑δ.toNNReal)⁻¹ - (1 - infEdist y E * (↑δ.toNNReal)⁻¹)
_ ≤ infEdist y E * (↑δ.toNNReal)⁻¹ - infEdist x E * (↑δ.toNNReal)⁻¹ := by
rw [ENNReal.sub_sub_sub_cancel_left (by finiteness) h_le]
_ ≤ (↑δ.toNNReal)⁻¹ * edist x y :=
by
rw [← ENNReal.sub_mul (by simp [δ_pos]), mul_comm, edist_comm]
gcongr
simp only [tsub_le_iff_right]
exact infEdist_le_edist_add_infEdist
· simp only [tsub_le_iff_right]
rw [tsub_eq_zero_of_le (not_le.mp h_le).le, add_zero, mul_comm]
calc
1
_ ≤ infEdist y E * (↑δ.toNNReal)⁻¹ := (not_le.mp h_le).le
_ ≤ edist x y * (↑δ.toNNReal)⁻¹ + infEdist x E * (↑δ.toNNReal)⁻¹ :=
by
rw [← add_mul, edist_comm]
gcongr
exact infEdist_le_edist_add_infEdist