Monitoring Cost Positive

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem monitoring_cost_positive {c_base A I : ℝ}
    (hc : 0 < c_base) (hA : 0 < A) (hI : 0 < I) :
    0 < monitoringCost c_base A I :=
  div_pos hc (mul_pos hA hI)

Dependency Graph

Location

thesis/CESProofs/Applications/MonitoringCost.lean:51

Module Section

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

In the same file

monitoringCost monitoringReturn monitoredCriticalFriction integrationSurplus 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