cubicArea_singleton

formal source

 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
 159      obtain ⟨i, j⟩ := e1
 160      simp
 161      have hκ : 0 ≤ jcost_to_regge_factor := le_of_lt jcost_to_regge_factor_pos
 162      have hw : 0 ≤ h.weight (i, j) := h.weight_nonneg _
 163      have : 0 ≤ jcost_to_regge_factor * h.weight (i, j) := mul_nonneg hκ hw
 164      linarith
 165    · -- `e1 :: e2 :: es'` case: all longer lists
 166      simp
 167
 168/-- The cubic deficit functional. -/