Value Function Deriv

def proved Microeconomics

Documentation

Lean 4 Proof

def valueFunctionDeriv (J ρ c : ℝ) : ℝ :=
  marginalK J ρ * perCapitaBenefit J ρ c +
  curvatureKReal J ρ * ((1 / ρ - 1) * J ^ (1 / ρ - 2) * c)

Dependency Graph

Used by

underentry_proved marginal_externality_pos valueFunction_increasing hasDerivAt_valueFunction fold_underentry underentry_at_private_optimum pigouvian_subsidy_decomposition valueFunctionDeriv_pos strategic_complementarity_full

Location

thesis/CESProofs/EntryExit/Calculus.lean:75

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)