lipschitzWith_ψ

lemma lipschitzWith_ψ (hD : 1 ≤ D) : LipschitzWith (4 * D) (ψ D) := by  have max_eq_4D : max 0 (4 * D : ℝ≥0) = 4 * D := max_eq_right (by positivity)  have max_eq_4D' : max (4 * D) 4 = 4 * D := by apply max_eq_left; linarith  suffices LipschitzWith (4 * D) (fun (x : ℝ) ↦ min 1 <| min (4 * D * x - 1) (2 - 4 * x)) from    max_eq_4D ▸ (LipschitzWith.const 0).max this  suffices LipschitzWith (4 * D) (fun (x : ℝ) ↦ min (4 * D * x - 1) (2 - 4 * x)) from    max_eq_4D ▸ (LipschitzWith.const 1).min this  have lw1 : LipschitzWith (4 * D) (fun (x : ℝ) ↦ 4 * D * x - 1) := by    refine LipschitzWith.of_le_add_mul (4 * D) (fun x y ↦ ?_)    suffices 4 * D * (x - y) ≤ 4 * D * dist x y by norm_cast at this ⊢; linarith    exact (mul_le_mul_iff_right₀ (by positivity)).2 <| sub_le_dist x y  have lw2 : LipschitzWith 4 (fun (x : ℝ) ↦ 2 - 4 * x) := by    refine LipschitzWith.of_le_add_mul 4 (fun x y ↦ ?_)    suffices 4 * (y - x) ≤ 4 * dist x y by norm_cast at this ⊢; linarith    gcongr    exact dist_comm x y ▸ sub_le_dist y x  have := lw1.min lw2  norm_cast at this ⊢  convert max_eq_4D' ▸ this