Documentation

Lean 4 Proof

theorem institutions_widen_integration {c_base A I₁ I₂ K_eff T : ℝ}
    (hc : 0 < c_base) (hA : 0 < A) (hI₁ : 0 < I₁) (hI₂ : 0 < I₂)
    (hT : 0 < T) (hI : I₁ < I₂) :
    integrationSurplus K_eff (monitoringCost c_base A I₁) T <
    integrationSurplus K_eff (monitoringCost c_base A I₂) T := by
  apply lower_monitoring_widens_integration hT
  exact institutions_reduce_monitoring hc hA hI₁ hI₂ hI

Dependency Graph

Location

thesis/CESProofs/Applications/MonitoringCost.lean:119

Module Section

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

In the same file