Documentation

Lean 4 Proof

theorem bridge_W_uniform_depreciation
    {P_cycle sigma beta_n : ℝ} (hP : 0 < P_cycle) (hsig : 0 < sigma)
    (hb : 0 < beta_n) :
    0 < P_cycle / (sigma * beta_n) := by
  exact div_pos hP (mul_pos hsig hb)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:149

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file