Documentation

Lean 4 Proof

theorem ngm_entry_increases_with_gain {phi_deriv₁ phi_deriv₂ Fbar sigma : ℝ}
    (hF : 0 < Fbar) (hs : 0 < sigma) (hphi : phi_deriv₁ < phi_deriv₂) :
    phi_deriv₁ * Fbar / sigma < phi_deriv₂ * Fbar / sigma := by
  apply div_lt_div_of_pos_right _ hs
  exact mul_lt_mul_of_pos_right hphi hF

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:79

Module Section

Proposition: Endogenous Crossing

In the same file