Documentation

Lean 4 Proof

theorem pareto_exponent_decreasing {q₁ q₂ : ℝ} (hq1 : 1 < q₁) (hq2 : q₁ < q₂) :
    1 / (q₂ - 1) < 1 / (q₁ - 1) := by
  apply div_lt_div_of_pos_left one_pos (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Potential/QEquilibrium.lean:109

Module Section

Propositions 3-4: q-Exponential Equilibrium and Tail Behavior

In the same file