structure
definition
DeficitLinearizationCert
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 181.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
178
179/-! ## §5. Certificate -/
180
181structure DeficitLinearizationCert where
182 linear_vanishes : ∀ {nH nE : ℕ}
183 (W : WellShapedData nH nE) (η : EdgePerturbation nE),
184 (∑ h : Fin nH, (W.complex.hinges h).area *
185 linearizedDeficit W.coeffs η h) = 0
186
187/-- The certificate is inhabited by the proved `linear_regge_vanishes`. -/
188theorem deficitLinearizationCert : DeficitLinearizationCert where
189 linear_vanishes := fun W η => linear_regge_vanishes W η
190
191end
192
193end DeficitLinearization
194end Geometry
195end IndisputableMonolith