cubicArea

formal source

 119
 120/-- Area at a hinge: if the hinge carries a single edge `(i, j)`,
 121    return `(κ/2) · (h.weight (i, j))`; otherwise return 0. -/
 122def cubicArea {n : ℕ} (_L : EdgeLengthField n) (h : HingeDatum n) : ℝ :=
 123  match h.edges with
 124  | [(i, j)] => jcost_to_regge_factor * h.weight (i, j) / 2
 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