Documentation

Lean 4 Proof

theorem institutions_reduce_monitoring {c_base A I₁ I₂ : ℝ}
    (hc : 0 < c_base) (hA : 0 < A) (hI₁ : 0 < I₁) (_hI₂ : 0 < I₂)
    (hI : I₁ < I₂) :
    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_left hI hA)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/MonitoringCost.lean:78

Module Section

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

In the same file