Documentation

Lean 4 Proof

theorem complementary_sectors_highest_return {J : ℕ} (hJ : 2 ≤ J)
    {rho1 rho2 : ℝ} (hrho : rho1 < rho2) {dT Tstar : ℝ}
    (hdT : 0 < dT) (hTs : 0 < Tstar) :
    monitoringReturn (curvatureK J rho2) dT Tstar <
    monitoringReturn (curvatureK J rho1) dT Tstar :=
  monitoring_return_proportional_to_K hdT hTs (curvatureK_decreasing_in_rho hJ hrho)

Dependency Graph

Location

thesis/CESProofs/Applications/MonitoringCost.lean:156

Module Section

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

In the same file