Documentation

Lean 4 Proof

theorem curvatureK_real_concave_derivative {J ρ : ℝ}
    (hJ : 0 < J) (hρ : ρ < 1) :
    -2 * (1 - ρ) / J ^ 3 < 0 := by
  apply div_neg_of_neg_of_pos
  · nlinarith
  · positivity

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:40

Module Section

Paper 1c, Section 2: K(J) as the Network Engine

In the same file