Sections / Section 17: Welfare, Trade, Applications / healthyEquilibrium

Healthy Equilibrium

defprovedCurvature Roles

Documentation

Lean 4 Proof

def healthyEquilibrium (R c_min : ℝ) : ℝ := R / c_min

Dependency Graph

Used by

above_healthy_repels bifurcation_condition below_healthy_attracts healthy_eq_zero_profit healthy_eq_positive

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:139

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file

diversity_premium_monotone_J diversity_exponent_superlinear diversity_exponent_negative totalRevenue totalRevenue_zero totalRevenue_one totalRevenue_between marketplace_rescue producerProfit healthy_eq_zero_profit healthy_eq_positive below_healthy_attracts above_healthy_repels collapse_when_underfunded bifurcation_condition frontLoadedRevenue frontLoaded_one frontLoaded_worse_than_linear convexAvgCost convex_consumer_approx