Documentation

Lean 4 Proof

theorem technology_widens_integration {c_base A₁ A₂ I K_eff T : ℝ}
    (hc : 0 < c_base) (hA₁ : 0 < A₁) (hA₂ : 0 < A₂) (hI : 0 < I)
    (hT : 0 < T) (hA : A₁ < A₂) :
    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 technology_reduces_monitoring hc hA₁ hA₂ hI hA

Dependency Graph

Location

thesis/CESProofs/Applications/MonitoringCost.lean:105

Module Section

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

In the same file