Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:97

Module Section

Aggregation-invariant class results from Paper 1, Section 5:

In the same file