Documentation

Lean 4 Proof

theorem tail_compact (q T : ℝ) (hq : q < 1) (hT : 0 < T) :
    0 < T / (1 - q) :=
  div_pos hT (by linarith)

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:103

Module Section

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

In the same file