Documentation

Lean 4 Proof

theorem superlinear_scaling {ρ : ℝ} (hρ0 : 0 < ρ) (hρ1 : ρ < 1) :
    1 < 1 / ρ := by
  rw [one_lt_div hρ0]
  exact hρ1

Dependency Graph

Location

thesis/CESProofs/EntryExit/NetworkEntry.lean:47

Module Section

Paper 1c, Section 6: Endogenous Network Scaling

In the same file