lipschitzWith_thickenedIndicator — Mathlib

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

Похожие утверждения