theorem
proved
equilibriumDomain_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Applied.UniversalEquilibriumResponseC7 on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26 | healthState
27 deriving DecidableEq, Repr, Fintype
28
29theorem equilibriumDomain_count : Fintype.card EquilibriumDomain = 3 := by
30 decide
31
32noncomputable def responseCoefficient (_ : EquilibriumDomain) : ℝ :=
33 jcostHessianCoefficient
34
35theorem responseCoefficient_universal (D : EquilibriumDomain) :
36 responseCoefficient D = 1 := by
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