Documentation

Lean 4 Proof

theorem gain_decreasing_in_friction {K_eff₁ K_eff₂ a_base F_prev β : ℝ}
    (ha : 0 < a_base) (hF : 0 < F_prev) (_hβ : 0 < β)
    (hK : K_eff₁ < K_eff₂) :
    a_base * K_eff₁ * F_prev ^ β < a_base * K_eff₂ * F_prev ^ β := by
  apply mul_lt_mul_of_pos_right _ (rpow_pos_of_pos hF β)
  exact mul_lt_mul_of_pos_left hK ha

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:70

Module Section

Proposition: Endogenous Crossing

In the same file