Documentation

Lean 4 Proof

theorem technology_reduces_monitoring {c_base A₁ A₂ I : ℝ}
    (hc : 0 < c_base) (hA₁ : 0 < A₁) (_hA₂ : 0 < A₂) (hI : 0 < I)
    (hA : A₁ < A₂) :
    monitoringCost c_base A₂ I < monitoringCost c_base A₁ I := by
  simp only [monitoringCost]
  exact div_lt_div_of_pos_left hc (mul_pos hA₁ hI)
    (mul_lt_mul_of_pos_right hA hI)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/MonitoringCost.lean:63

Module Section

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

In the same file