theorem
proved
linear_regge_vanishes
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Geometry.DeficitLinearization on GitHub at line 136.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
133
134/-- The linear (first-order) part of the Regge action vanishes under
135 Schläfli's identity. -/
136theorem linear_regge_vanishes {nH nE : ℕ}
137 (W : WellShapedData nH nE) (η : EdgePerturbation nE) :
138 (∑ h : Fin nH, (W.complex.hinges h).area *
139 linearizedDeficit W.coeffs η h) = 0 := by
140 unfold linearizedDeficit
141 -- Rewrite the sum: move the minus sign out, then swap summation order.
142 have h_swap :
143 (∑ h : Fin nH, (W.complex.hinges h).area *
144 -(∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
145 = - ∑ e : Fin nE,
146 η.eta e * (∑ h : Fin nH, (W.complex.hinges h).area * W.coeffs.dThetadL h e) := by
147 rw [show (∑ h : Fin nH, (W.complex.hinges h).area *
148 -(∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
149 = -(∑ h : Fin nH, (W.complex.hinges h).area *
150 (∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
151 from by
152 rw [← Finset.sum_neg_distrib]
153 apply Finset.sum_congr rfl
154 intro h _; ring]
155 rw [show (∑ h : Fin nH, (W.complex.hinges h).area *
156 (∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
157 = ∑ h : Fin nH, ∑ e : Fin nE,
158 (W.complex.hinges h).area * W.coeffs.dThetadL h e * η.eta e
159 from by
160 apply Finset.sum_congr rfl
161 intro h _
162 rw [Finset.mul_sum]
163 apply Finset.sum_congr rfl
164 intro e _; ring]
165 rw [Finset.sum_comm]
166 congr 1