singletonHinge_weight

formal source

 100      · simp [h]
 101  }
 102
 103theorem singletonHinge_weight {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 104    (singletonHinge i j w hw).weight (i, j) = w := by
 105  unfold singletonHinge; simp
 106
 107theorem singletonHinge_edges {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 108    (singletonHinge i j w hw).edges = [(i, j)] := by
 109  unfold singletonHinge; rfl
 110
 111/-! ## §3. The cubic deficit functional via pattern matching -/
 112
 113/-- Deficit at a hinge: if the hinge carries a single edge `(i, j)`,
 114    return `(ε_i − ε_j)²`; otherwise return 0. -/
 115def cubicDeficit {n : ℕ} (L : EdgeLengthField n) (h : HingeDatum n) : ℝ :=
 116  match h.edges with
 117  | [(i, j)] => (recoverEps L i - recoverEps L j) ^ 2
 118  | _ => 0
 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