defectDist_quasi_triangle_local

formal source

 373
 374/-- Proposition 2.6, local form: on bounded edge-ratios, the defect distance
 375    satisfies the quasi-triangle bound with the paper's constant `K_M`. -/
 376theorem defectDist_quasi_triangle_local {M x y z : ℝ} (hM : 1 ≤ M)
 377    (hx : 0 < x) (hy : 0 < y) (hz : 0 < z)
 378    (hxy_lower : 1 / M ≤ x / y) (hxy_upper : x / y ≤ M)
 379    (hyz_lower : 1 / M ≤ y / z) (hyz_upper : y / z ≤ M) :
 380    defectDist x z ≤ ((M + 2 + M⁻¹) / 2) * (defectDist x y + defectDist y z) := by
 381  have hMpos : 0 < M := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hM
 382  have hxy_pos : 0 < x / y := div_pos hx hy
 383  have hyz_pos : 0 < y / z := div_pos hy hz
 384  have hratio : (x / y) * (y / z) = x / z := by
 385    field_simp [hy.ne', hz.ne']
 386  have hsub :
 387      J ((x / y) * (y / z)) ≤
 388        2 * J (x / y) + 2 * J (y / z) + 2 * J (x / y) * J (y / z) := by
 389    simpa [J] using (Jcost_submult (x := x / y) (y := y / z) hxy_pos hyz_pos)
 390  have hsub' :
 391      defectDist x z ≤
 392        2 * defectDist x y + 2 * defectDist y z + 2 * defectDist x y * defectDist y z := by
 393    unfold defectDist
 394    simpa [hratio] using hsub
 395  have hxy_bound : defectDist x y ≤ J M :=
 396    defectDist_le_J_of_ratio_bounds hM hx hy hxy_lower hxy_upper
 397  have hyz_bound : defectDist y z ≤ J M :=
 398    defectDist_le_J_of_ratio_bounds hM hy hz hyz_lower hyz_upper
 399  have hxy_nonneg : 0 ≤ defectDist x y := defectDist_nonneg x y hx hy
 400  have hyz_nonneg : 0 ≤ defectDist y z := defectDist_nonneg y z hy hz
 401  have hM_nonneg : 0 ≤ J M := J_nonneg M hMpos
 402  have hcross :
 403      2 * defectDist x y * defectDist y z ≤ J M * (defectDist x y + defectDist y z) := by
 404    have hleft :
 405        defectDist x y * defectDist y z ≤ J M * defectDist y z := by
 406      exact mul_le_mul_of_nonneg_right hxy_bound hyz_nonneg