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
97 results
(filtered from 2160)
Has Deriv At Curvature K Real
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:27
Marginal K Strict Anti On
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:40
Has Deriv At Per Capita Benefit
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:50
Per Capita Benefit Pos
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:60
Value Function
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:71
Value Function Deriv
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:75
Has Deriv At Value Function
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:80
Value Function Deriv Pos
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:94
Value Function At One
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:106
Value Function Increasing
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:112
Value Function Pos
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:148
Per Capita Surplus
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:164
Per Capita Surplus Alt
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:167
Per Capita Surplus At One
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:173
Per Capita Surplus At Two
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:178
Per Capita Surplus Pos
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:184
Per Capita Surplus Deriv
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:193
Has Deriv At Per Capita Surplus
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:197
Per Capita Surplus Deriv Pos
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:224
Per Capita Surplus Deriv Neg
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:232
Per Capita Surplus Increasing Below Peak
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:240
Per Capita Surplus Decreasing Above Peak
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:261
Per Capita Surplus Le Peak
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:291
Per Capita Surplus Eq K Div J
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:303
Social Welfare
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:315
Marginal Externality Pos
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:320
Underentry At Private Optimum
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:329
Pigouvian Subsidy Decomposition
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:339
Pareto Ranking Strengthened
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:353
Welfare Gap Lower Bound
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Calculus.lean
:362
Curvature K Real Increasing
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:24
Curvature K Real Concave Derivative
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:42
Curvature K Real Bounded
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:52
Curvature K Real One
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:63
Curvature K Real Nonneg
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:68
Curvature K Real Pos
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:76
Critical Friction Linear In J
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:90
Critical Friction Increasing In J
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:97
Minimum Viable Friction
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:110
Curvature K Factorization
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:123
Smirl Tradeoff Vs Romer Escape
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:133
Equal Weight Entry Improves K
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:166
Equal Weight Entry Maximizes K
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:176
K Deficit From Concentration
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:182
K Positive Nondegenerate
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/CurvatureInJ.lean
:192
Curvature K Real
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Defs.lean
:27
Curvature K Real Eq Nat
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Defs.lean
:30
Critical Friction Real
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Defs.lean
:41
Critical Friction Real Eq
theorem
proved
Microeconomics
thesis/CESProofs/EntryExit/Defs.lean
:46
Effective K Real
def
proved
Microeconomics
thesis/CESProofs/EntryExit/Defs.lean
:57
« Prev
Page 1 of 2
Next »