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
1607 results
(filtered from 2160)
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 Trivial Solution
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:93
Adoption Threshold
theorem
proved
Curvature Roles
thesis/CESProofs/Applications/AITransition.lean
:108
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 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
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 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
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 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 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
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
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
« Prev
Page 1 of 33
Next »