Path metric

Stream: maths

[Rémi Bottinelli]

Hey, would it make sense to have a generic notion of “path metric” on a space as below ?
Possible uses would be the path metric on a graph, but also the “intrinsic path metric” on a metric space (using rectifiable paths).
What would a good API look like?

import data.real.ennreal
import topology.metric_space.emetric_space
import combinatorics.quiver.basic
import combinatorics.simple_graph.basic
import combinatorics.simple_graph.connectivity

noncomputable theory

open_locale classical ennreal

open emetric ennreal


@[class]
structure paths (α : Type*) extends quiver α :=
  (inv : Π {a b : α}, (a ⟶ b) → (b ⟶ a))
  (comp : Π {a b c : α}, (a ⟶ b) → (b ⟶ c) → (a ⟶ c))

@[class]
structure paths_with_lengths (α : Type*) extends (paths α) :=
  (L : Π {a b : α}, (a ⟶ b) → ennreal)
  (Lrefl : Π (a : α), infi (@L a a) = (0 : ennreal))
  (Lsymm : Π {a b : α}, Π p : a ⟶ b, L (inv p) ≤ L p)
  (Ltran : Π {a b c : α}, Π p : a ⟶ b, Π q : b ⟶ c, L (comp p q) ≤ L p + L q)


section path_metric

variables {α : Type*} [pl : paths_with_lengths α]

abbreviation ℓ {a b : α} (p : a ⟶ b) := pl.L p -- can we make this work


def pl_edist (a b : α) : ennreal := infi (λ (p : a ⟶ b), (pl.L p : ennreal))
instance my_edist [pl : paths_with_lengths α] : has_edist α := ⟨pl_edist⟩

lemma edist_finite (a b : α) (p : a ⟶ b) (Hp : pl.L p < ⊤) : edist a b < ⊤ :=
  infi_lt_iff.mpr (⟨p, Hp⟩)
lemma edist_antisymm (a b : α) (ε : ennreal) (H : ε > 0) (Hab : Π p : a ⟶ b, pl.L p ≥ ε) :
  edist a b ≥ ε := le_infi Hab
lemma edist_antisymm' (a b : α) (ε : ennreal) (H : ε > 0) (Hab : Π p : a ⟶ b, pl.L p ≥ ε) :
  edist a b > 0 := gt_of_ge_of_gt (edist_antisymm a b ε H Hab) H



lemma edist_min (a b : α) (pmin : a ⟶ b) (Hmin : ∀ p : a ⟶ b, pl.L pmin ≤ pl.L p) :
  edist a b = pl.L pmin :=
has_le.le.antisymm (infi_le (λ p : a ⟶ b, pl.L p) pmin) (le_infi Hmin)

lemma edist_min_nat (a b : α) (hnat : ∀ p : a ⟶ b, ∃ np : ℕ, pl.L p = np)
  (hnempty : nonempty (a ⟶ b)) :
∃ p : a ⟶ b, edist a b = pl.L p :=
begin
  let Lℕ : set ℕ := {n : ℕ | ∃ (p : a ⟶ b), pl.L p = n},
  have hLℕ : ∃ n, n ∈ Lℕ, by
  { let p := nonempty.some hnempty,
    rcases hnat p with ⟨np, pgood⟩,
    exact ⟨np,p,pgood⟩,},
  let n := nat.find hLℕ,
  rcases nat.find_spec hLℕ with ⟨p,pgood⟩,
  have : ∀ q : a ⟶ b, pl.L p ≤ pl.L q, by {
    intro q,
    rcases hnat q with ⟨nq,qgood⟩,
    have : nq ∈ Lℕ, from ⟨q,qgood⟩,
    have : n ≤ nq, from nat.find_min' hLℕ ‹nq∈Lℕ›,
    rw [qgood,pgood],
    exact coe_nat_le_coe_nat.mpr ‹n≤nq›,
  },
  use p,
  exact edist_min a b p this,
end

lemma my_edist_refl [pl : paths_with_lengths α] (a : α) : edist a a = 0 := pl.Lrefl a

lemma my_edist_symm_le [pl : paths_with_lengths α] (a b : α) : edist a b ≤ edist b a :=
begin
  apply @infi_mono' _ _ _ _(λ (p : a ⟶ b), pl.L p) (λ (q : b ⟶ a), pl.L q),
  rintro p,
  use pl.inv p,
  exact (pl.Lsymm p),
end

lemma my_edist_symm [pl : paths_with_lengths α] (a b : α) : edist a b = edist b a :=
has_le.le.antisymm (my_edist_symm_le a b) (my_edist_symm_le b a)

lemma infi_good {α : Type*} (f : α → ennreal) (hinfi : ¬ infi f = ⊤) (ε : ennreal) (εp : ε > 0) :
  ∃ a : α, f a ≤ infi f + ε :=
begin
  sorry,
end

lemma my_edist_triangle [pl : paths_with_lengths α] (a b c : α) : edist a c ≤ edist a b + edist b c :=
begin
  suffices : ∀ ε > 0, edist a c ≤ edist a b + edist b c + ε, by {
    apply ennreal.le_of_forall_pos_le_add,
    rintro ε hε hsum,
    exact this ε (by {norm_cast, use hε}),},
  rintros ε hε,
  by_cases abt : edist a b = ⊤,
  { rw abt, simp only [ennreal.top_add, le_top], },
  by_cases bct : edist b c = ⊤,
  { rw bct, simp only [ennreal.add_top, ennreal.top_add, le_top], },
  -- rw infi_eq_top.not at abt,
  /-have : edist a b = ⊤ ↔ ∀ (p : a ⟶ b), pl.L p = ⊤, by apply infi_eq_top,
  have := iff.not this, rw this at abt,
  have : edist b c = ⊤ ↔ ∀ (p : b ⟶ c), pl.L p = ⊤, by apply infi_eq_top,
  have := iff.not this, rw this at bct,
  push_neg at abt bct,-/

  have : ∃ (p : a ⟶ b), pl.L p ≤ edist a b + ε/2, by
  { sorry,--unfold edist, unfold pl_edist,
    --apply infi_good (λ (p : a ⟶ b), pl.L p) abt (ε/2),
  },
  obtain ⟨p,hp⟩ := this,
  have : ∃ (q : b ⟶ c), pl.L q ≤ edist b c + ε/2, by sorry,
  obtain ⟨q,hq⟩ := this,

  let pq := pl.comp p q,
  have : pl.L pq ≤ edist a b + edist b c + ε, by
  calc pl.L pq  ≤ pl.L p + pl.L q          : pl.Ltran p q
            ... ≤ (edist a b + ε/2) + pl.L q : add_le_add_right hp (pl.L q)
            ... ≤ (edist a b + ε/2) + (edist b c + ε/2) : add_le_add_left hq (edist a b + ε/2)
            ... = edist a b + edist b c + ε : by {nth_rewrite_rhs 0 ←ennreal.add_halves ε,sorry},
  exact infi_le_of_le pq this,
end


instance my_pem [pl : paths_with_lengths α] : pseudo_emetric_space α :=
{ to_has_edist := my_edist
, edist_self := my_edist_refl
, edist_comm := my_edist_symm
, edist_triangle := my_edist_triangle}


end path_metric


section for_graphs

variables {V : Type*} (G : simple_graph V)

instance lol : paths_with_lengths V := {
  hom := G.walk,
  inv := (λ a b p, p.reverse),
  comp := (λ a b c p q, p.append q),
  L := (λ a b p, p.length),
  Lrefl := (λ a, by { rw ←le_zero_iff, convert infi_le _ (simple_graph.walk.nil' a), simp,}),
  Lsymm := (λ a b p, le_of_eq (by {norm_cast, exact simple_graph.walk.length_reverse p})),
  Ltran := (λ a b c p q, le_of_eq (by { norm_cast, exact simple_graph.walk.length_append p q, }))}

end for_graphs