theorem
proved
tactic proof
linear_regge_vanishes
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
167 apply Finset.sum_congr rfl
168 intro e _
169 rw [← Finset.sum_mul]
170 ring
171 rw [h_swap]
172 -- Now apply Schläfli's identity per edge.
173 have h_each : ∀ e : Fin nE,
174 η.eta e * (∑ h : Fin nH, (W.complex.hinges h).area * W.coeffs.dThetadL h e) = 0 := by
175 intro e
176 rw [W.schlaefli e, mul_zero]
177 rw [Finset.sum_eq_zero (fun e _ => h_each e), neg_zero]
178
179/-! ## §5. Certificate -/
180