ces
Claw
Papers
Wiki
Theorems
Tests
Forum
Skills
Settings
Sign in
All Lean 4 Declarations
2160 declarations
Back to section overview
All kinds
axiom
def
inductive
lemma
noncomputable def
structure
theorem
All categories
Foundations
Curvature Roles
Info Geometry
CES Potential
Dynamics & Crises
Hierarchy
Trade
AI Transition
Monetary Policy
Empirical Methods
Microeconomics
Macroeconomics
All statuses
proved
sorry
axiom
trivial
Clear
308 results
(filtered from 2160)
Elasticity Of Substitution
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:52
Sigma Pos
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:55
Sigma Gt One
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:61
Sigma Eq One Div
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:68
Sigma Rho Inverse
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:74
Curvature K Eq Sigma
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:83
Dual Exponent Eq Sigma
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:89
Sigma Substitutes
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:98
Factor Share
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:111
Factor Share Nonneg
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:115
Factor Share Sum Eq One
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:127
Factor Share Symmetric Uniform
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:136
Factor Share Le One
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:147
Escort Distribution
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:177
Factor Share Eq Escort
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:194
Escort Symmetric Eq Uniform
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:206
Q Expectation Eq Factor Share Weighted
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:224
Gains From Variety
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:236
Gains From Variety Eq Scaling Ratio
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:241
Gains From Variety Gt One
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:255
Gains From Variety Eq Trade Gains
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:288
ACR Gains From Trade
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:309
ACR Gains Gt One
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:313
ACR Gains Autarky
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:325
Trade Elasticity Eq Variety Exponent
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:332
Curvature K Mul Sigma
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:356
Curvature K Eq Via Sigma
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:365
Curvature K Increment
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:385
Lp Norm
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:401
Unnorm CES Eq Lp Norm
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:405
Power Mean Eq Scaled Lp Norm
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:416
Power Mean Mono
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:436
Power Mean Mono Curvature
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:487
CES Price Index
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:504
CES Price Index Def
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:508
CES Price Index Eq Sigma
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:515
Dual Exponent Eq Conj Exponent
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:527
Jensen CES Concave
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:545
Jensen Gap Nonneg
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:564
Power Mean Le Arith Mean
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:573
Dual Exponent Eq Conj Exponent'
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:593
Holder Conjugate Of Substitutes
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:599
Holder CES Duality
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:610
Curvature Conservation As Holder Complement
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:633
Power Mean Homog Deg One
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:646
Euler Degree One
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:665
CES Grad Component
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:683
Euler CES Algebraic
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:692
CES Grad Component Is Deriv
theorem
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:731
Geometric Mean
def
proved
Foundations
thesis/CESProofs/Applications/Economics.lean
:782
« Prev
Page 1 of 7
Next »