def monitoringReturn (K dT Tstar : ℝ) : ℝ := K * dT / Tstar
thesis/CESProofs/Applications/MonitoringCost.lean:36
Micro-Foundation for the Monitoring Cost c₀ (Gap 12)