ratio_rigidity_iff

formal source

  89  (∀ edges, J(x_v/x_w) = 0)  ↔  x is constant.
  90
  91This is the machine-verified version of Result 1. -/
  92theorem ratio_rigidity_iff {adj : V → V → Prop}
  93    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
  94    {x : V → ℝ} (hpos : ∀ v, 0 < x v) :
  95    (∀ v w, adj v w → Jcost (x v / x w) = 0) ↔
  96    (∀ v w : V, x v = x w) :=
  97  ⟨ratio_rigidity hconn hpos,
  98   fun hconst v w _ => constant_implies_zero_cost (hconst v w) (hpos w)⟩
  99
 100/-! ### Corollary: edge cost characterizations -/
 101
 102/-- J(x_v/x_w) = 0 iff x_v = x_w, for positive x. -/
 103theorem edge_cost_zero_iff {x : V → ℝ} {v w : V}
 104    (hv : 0 < x v) (hw : 0 < x w) :
 105    Jcost (x v / x w) = 0 ↔ x v = x w := by
 106  constructor
 107  · intro h
 108    have h1 := Jcost_zero_iff_one (div_pos hv hw) h
 109    rwa [div_eq_iff (ne_of_gt hw), one_mul] at h1
 110  · intro h
 111    rw [h, div_self (ne_of_gt hw)]
 112    exact Jcost_unit0
 113
 114end IndisputableMonolith.Papers.GCIC.GraphRigidity