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

Producer Profit

defprovedCurvature Roles

Documentation

Lean 4 Proof

def producerProfit (R J c_min : ℝ) : ℝ := R / J - c_min

Dependency Graph

Used by

above_healthy_repels below_healthy_attracts collapse_when_underfunded healthy_eq_zero_profit

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:135

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 healthyEquilibrium 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