Documentation

Lean 4 Proof

theorem monitoring_return_proportional_to_K {K₁ K₂ dT Tstar : ℝ}
    (hdT : 0 < dT) (hTs : 0 < Tstar) (hK : K₁ < K₂) :
    monitoringReturn K₁ dT Tstar < monitoringReturn K₂ dT Tstar := by
  simp only [monitoringReturn]
  exact div_lt_div_of_pos_right (mul_lt_mul_of_pos_right hK hdT) hTs

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/MonitoringCost.lean:143

Module Section

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

In the same file