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
2024 results
(filtered from 2160)
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 41
Next »