Documentation

Lean 4 Proof

theorem lower_monitoring_widens_integration {K_eff c₀₁ c₀₂ T : ℝ}
    (hT : 0 < T) (hc : c₀₁ < c₀₂) :
    integrationSurplus K_eff c₀₂ T < integrationSurplus K_eff c₀₁ T := by
  simp only [integrationSurplus]
  linarith [mul_lt_mul_of_pos_right hc hT]

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/MonitoringCost.lean:92

Module Section

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

In the same file