Monitoring Cost

def proved Curvature Roles

Documentation

Lean 4 Proof

def monitoringCost (c_base A I : ℝ) : ℝ := c_base / (A * I)

Dependency Graph

Used by

technology_widens_integration institutions_widen_integration monitoring_cost_positive technology_reduces_monitoring monitoring_technology_complementarity institutions_reduce_monitoring

Location

thesis/CESProofs/Applications/MonitoringCost.lean:32

Module Section

Micro-Foundation for the Monitoring Cost c₀ (Gap 12)

In the same file

monitoringReturn monitoredCriticalFriction integrationSurplus monitoring_cost_positive technology_reduces_monitoring institutions_reduce_monitoring lower_monitoring_widens_integration technology_widens_integration institutions_widen_integration zero_monitoring_full_threshold monitoring_return_proportional_to_K complementary_sectors_highest_return monitoring_technology_complementarity