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
2160 results
Effective Training Productivity
def
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:46
Phieff Exceeds Phi 0
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:54
Phieff Ge One Condition
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:70
Gc Function
def
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:88
Gc Trivial Solution
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:93
Adoption R0
def
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:104
Adoption Threshold
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:108
Baumol Growth Rate
def
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:129
Baumol Limit
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:133
Baumol Bounded Below
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:140
Singularity Time
def
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:156
Singularity Time Pos
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:160
Two Period Overinvestment
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:176
Saturation Escape Rate
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:194
Effective Alpha Monotone J
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:211
Collapse At J1
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:226
Crossing Threshold Reexport
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:237
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
« Prev
Page 1 of 44
Next »