Documentation

Lean 4 Proof

def excessSavingCoeff (J : ℕ) (ρ : ℝ) : ℝ :=
  (↑J - 1) ^ 2 / (2 * ↑J ^ 3 * curvatureK J ρ)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:143

Module Section

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

In the same file