le_two_mul_dist_ofPreNNDist — Mathlib

English

Let d be a symmetric, nonnegative function with zero diagonal; dist is the largest pseudometric dominated by d. Then dist ≤ d and dist(x,y) ≤ d(x,y) for all x,y.

Русский

Пусть d симметрична и неотрицательна, с нулевой диагональю; dist — наибольшая псевдометрическая величина, не превосходящая d. Тогда dist ≤ d и dist(x,y) ≤ d(x,y) для всех x,y.

LaTeX

$$$\\forall X\\, d, dist, dist\\_self, dist\\_comm, x,y:\\; dist x y ≤ d x y$$$

Lean4

/-- Consider a function `d : X → X → ℝ≥0` such that `d x x = 0` and `d x y = d y x` for all `x`,
`y`. Let `dist` be the largest pseudometric distance such that `dist x y ≤ d x y`, see
`PseudoMetricSpace.ofPreNNDist`. Suppose that `d` satisfies the following triangle-like
inequality: `d x₁ x₄ ≤ 2 * max (d x₁ x₂, d x₂ x₃, d x₃ x₄)`. Then `d x y ≤ 2 * dist x y` for all
`x`, `y`. -/
theorem le_two_mul_dist_ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x, d x x = 0) (dist_comm : ∀ x y, d x y = d y x)
    (hd : ∀ x₁ x₂ x₃ x₄, d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))) (x y : X) :
    ↑(d x y) ≤ 2 * @dist X (@PseudoMetricSpace.toDist X (PseudoMetricSpace.ofPreNNDist d dist_self dist_comm)) x y := by
  /- We need to show that `d x y` is at most twice the sum `L` of `d xᵢ xᵢ₊₁` over a path
      `x₀=x, ..., xₙ=y`. We prove it by induction on the length `n` of the sequence. Find an edge that
      splits the path into two parts of almost equal length: both `d x₀ x₁ + ... + d xₖ₋₁ xₖ` and
      `d xₖ₊₁ xₖ₊₂ + ... + d xₙ₋₁ xₙ` are less than or equal to `L / 2`.
      Then `d x₀ xₖ ≤ L`, `d xₖ xₖ₊₁ ≤ L`, and `d xₖ₊₁ xₙ ≤ L`, thus `d x₀ xₙ ≤ 2 * L`. -/

  rw [dist_ofPreNNDist, ← NNReal.coe_two, ← NNReal.coe_mul, NNReal.mul_iInf, NNReal.coe_le_coe]
  refine le_ciInf fun l => ?_
  have hd₀_trans : Transitive fun x y => d x y = 0 :=
    by
    intro a b c hab hbc
    rw [← nonpos_iff_eq_zero]
    simpa only [nonpos_iff_eq_zero, hab, hbc, dist_self c, max_self, mul_zero] using hd a b c c
  haveI : IsTrans X fun x y => d x y = 0 := ⟨hd₀_trans⟩
  suffices ∀ n, length l = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum by exact this _ rfl
  intro n hn
  induction n using Nat.strong_induction_on generalizing x y l with
  | h n ihn =>
    simp only at ihn
    subst n
    set L := zipWith d (x :: l) (l ++ [y])
    have hL_len : length L = length l + 1 := by simp [L]
    rcases eq_or_ne (d x y) 0 with hd₀ | hd₀
    · simp only [hd₀, zero_le]
    rsuffices ⟨z, z', hxz, hzz', hz'y⟩ : ∃ z z' : X, d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
    · exact (hd x z z' y).trans (mul_le_mul_left' (max_le hxz (max_le hzz' hz'y)) _)
    set s : Set ℕ := {m : ℕ | 2 * (take m L).sum ≤ L.sum}
    have hs₀ : 0 ∈ s := by simp [s]
    have hsne : s.Nonempty := ⟨0, hs₀⟩
    obtain ⟨M, hMl, hMs⟩ : ∃ M ≤ length l, IsGreatest s M :=
      by
      have hs_ub : length l ∈ upperBounds s := by
        intro m hm
        rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]
        intro hLm
        rw [mem_setOf_eq, take_of_length_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero, sum_eq_zero_iff, ←
            forall_iff_forall_mem, forall_zipWith, ← isChain_cons_append_singleton_iff_forall₂] at hm <;>
          [skip; simp]
        exact hd₀ (hm.rel_cons (mem_append.2 <| Or.inr <| mem_singleton_self _))
      have hs_bdd : BddAbove s := ⟨length l, hs_ub⟩
      exact ⟨sSup s, csSup_le hsne hs_ub, ⟨Nat.sSup_mem hsne hs_bdd, fun k => le_csSup hs_bdd⟩⟩
    have hM_lt : M < length L := by rwa [hL_len, Nat.lt_succ_iff]
    have hM_ltx : M < length (x :: l) := lt_length_left_of_zipWith hM_lt
    have hM_lty : M < length (l ++ [y]) := lt_length_right_of_zipWith hM_lt
    refine ⟨(x :: l)[M], (l ++ [y])[M], ?_, ?_, ?_⟩
    ·
      cases M with
      | zero => simp [dist_self]
      | succ M =>
        rw [Nat.succ_le_iff] at hMl
        have hMl' : length (take M l) = M := length_take.trans (min_eq_left hMl.le)
        refine (ihn _ hMl _ _ _ hMl').trans ?_
        convert hMs.1.out
        rw [take_zipWith, take, take_succ, getElem?_append_left hMl, getElem?_eq_getElem hMl, ← Option.coe_def,
          Option.toList_some, take_append_of_le_length hMl.le, getElem_cons_succ]
    · exact single_le_sum (fun x _ => zero_le x) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, getElem_zipWith⟩)
    · rcases hMl.eq_or_lt with (rfl | hMl)
      · simp only [getElem_append_right le_rfl, getElem_singleton, dist_self, zero_le]
      rw [getElem_append_left hMl]
      have hlen : length (drop (M + 1) l) = length l - (M + 1) := length_drop
      have hlen_lt : length l - (M + 1) < length l := Nat.sub_lt_of_pos_le M.succ_pos hMl
      refine (ihn _ hlen_lt _ y _ hlen).trans ?_
      rw [cons_getElem_drop_succ]
      have hMs' : L.sum ≤ 2 * (L.take (M + 1)).sum := not_lt.1 fun h => (hMs.2 h.le).not_gt M.lt_succ_self
      rw [← sum_take_add_sum_drop L (M + 1), two_mul, add_le_add_iff_left, ← add_le_add_iff_right,
        sum_take_add_sum_drop, ← two_mul] at hMs'
      convert hMs'
      rwa [drop_zipWith, drop, drop_append_of_le_length]

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