Documentation

Lean 4 Proof

theorem pareto_exponent_pos {q : ℝ} (hq : 1 < q) : 0 < 1 / (q - 1) :=
  div_pos one_pos (by linarith)

Dependency Graph

Location

thesis/CESProofs/Potential/QEquilibrium.lean:105

Module Section

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

In the same file