Documentation

Lean 4 Proof

theorem wright_law_decreasing {c₀ α Q₁ Q₂ : ℝ}
    (hc₀ : 0 < c₀) (hα : 0 < α) (hQ₁ : 0 < Q₁) (_hQ₂ : 0 < Q₂) (hQ : Q₁ < Q₂) :
    c₀ * Q₂ ^ (-α) < c₀ * Q₁ ^ (-α) := by
  apply mul_lt_mul_of_pos_left _ hc₀
  exact Real.rpow_lt_rpow_of_neg hQ₁ hQ (by linarith)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:40

Module Section

Proposition: Endogenous Crossing

In the same file