theorem
proved
tactic proof
defectDist_quasi_triangle_local
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
407 have hright :
408 defectDist x y * defectDist y z ≤ defectDist x y * J M := by
409 exact mul_le_mul_of_nonneg_left hyz_bound hxy_nonneg
410 have hsum :
411 defectDist x y * defectDist y z + defectDist x y * defectDist y z ≤
412 J M * defectDist y z + defectDist x y * J M := by
413 exact add_le_add hleft hright
414 nlinarith [hsum]
415 calc
416 defectDist x z
417 ≤ 2 * defectDist x y + 2 * defectDist y z + 2 * defectDist x y * defectDist y z := hsub'
418 _ ≤ 2 * defectDist x y + 2 * defectDist y z + J M * (defectDist x y + defectDist y z) := by
419 nlinarith [hcross]
420 _ = (2 + J M) * (defectDist x y + defectDist y z) := by ring
421 _ = ((M + 2 + M⁻¹) / 2) * (defectDist x y + defectDist y z) := by
422 rw [quasiTriangleConstant_eq]
423
424/-- Proposition 2.6, global form: no finite quasi-triangle constant works on
425 all positive triples. -/