structure
definition
UniversalResponseCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Applied.UniversalEquilibriumResponseC7 on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
37 unfold responseCoefficient
38 exact jcostHessianCoefficient_eq_one
39
40structure UniversalResponseCert where
41 three_domains : Fintype.card EquilibriumDomain = 3
42 universal_response : ∀ D : EquilibriumDomain, responseCoefficient D = 1
43 kernel : JCostHessianCert
44
45noncomputable def universalResponseCert : UniversalResponseCert where
46 three_domains := equilibriumDomain_count
47 universal_response := responseCoefficient_universal
48 kernel := jcostHessianCert
49
50end UniversalEquilibriumResponseC7
51end Applied
52end IndisputableMonolith