Documentation

Marginis.FranklinMcNicholl2020

Franklin and McNicholl define a metric on a graph by: d_G(v₀,v₁) = 0 if v₀ = v₁ 1 if (v₀,v₁) ∈ E; 2 otherwise

They say this is "clearly" a metric. We prove this formally and generalize it, by replacing 1 and 2 by real numbers 0 < a ≤ 2b, b ≤ 2a (the fact that 0 < b follows but does not need to be mentioned).

noncomputable instance franklinMcNichollMetric {U : Type} (G : SimpleGraph U) (a : ) (b : ) (h₀ : 0 < a) (h₁ : a b + b) (h₂ : b a + a) :
Equations