Value Function

def proved Microeconomics

Documentation

Lean 4 Proof

def valueFunction (J ρ c : ℝ) : ℝ :=
  curvatureKReal J ρ * perCapitaBenefit J ρ c

Dependency Graph

Used by

valueFunction_welfare_contribution entry_driven_by_value_function underentry_proved valueFunction_increasing welfare_gap_lower_bound higher_J_raises_value self_reinforcing_entry hasDerivAt_valueFunction fold_underentry welfare_gap_full socialWelfare underentry_at_private_optimum valueFunction_pos network_persistence_buffer pareto_ranking_full valueFunction_at_one value_function_welfare_contribution pareto_ranking_strengthened

Location

thesis/CESProofs/EntryExit/Calculus.lean:71

Module Section

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