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

Page 1 of 2