cubicDeficit_singleton

formal source

 125  | _ => 0
 126
 127/-- Value of `cubicDeficit` on a singleton hinge. -/
 128theorem cubicDeficit_singleton {n : ℕ} (L : EdgeLengthField n)
 129    (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 130    cubicDeficit L (singletonHinge i j w hw)
 131    = (recoverEps L i - recoverEps L j) ^ 2 := by
 132  show (match (singletonHinge i j w hw).edges with
 133        | [(i', j')] => (recoverEps L i' - recoverEps L j') ^ 2
 134        | _ => 0) = _
 135  rw [singletonHinge_edges]
 136
 137/-- Value of `cubicArea` on a singleton hinge. -/
 138theorem cubicArea_singleton {n : ℕ} (L : EdgeLengthField n)
 139    (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 140    cubicArea L (singletonHinge i j w hw)
 141    = jcost_to_regge_factor * w / 2 := by
 142  show (match (singletonHinge i j w hw).edges with
 143        | [(i', j')] =>
 144            jcost_to_regge_factor * (singletonHinge i j w hw).weight (i', j') / 2
 145        | _ => 0) = _
 146  rw [singletonHinge_edges]
 147  simp only
 148  rw [singletonHinge_weight]
 149
 150/-- `cubicArea` is nonnegative. -/
 151theorem cubicArea_nonneg {n : ℕ} (L : EdgeLengthField n) (h : HingeDatum n) :
 152    0 ≤ cubicArea L h := by
 153  unfold cubicArea
 154  -- Case-split on `h.edges`; only the single-pair case is nonzero.
 155  rcases h.edges with _ | ⟨e1, es⟩
 156  · simp
 157  · rcases es with _ | ⟨e2, es'⟩
 158    · -- `[e1]` case