Documentation

Lean 4 Proof

def knockoutRetained (J : ℕ) (ρ : ℝ) (m : ℕ) : ℝ :=
  if ρ > 0 then ((↑J - ↑m) / ↑J : ℝ) ^ (1 / ρ) else if m = 0 then 1 else 0

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:62

Module Section

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

In the same file