Documentation

Lean 4 Proof

def criticalFailures (J : ℕ) (ρ α : ℝ) : ℕ :=
  ⌈(↑J : ℝ) * (1 - α ^ ρ)⌉₊

Dependency Graph

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:100

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file