Documentation

Lean 4 Proof

theorem curvatureK_real_nonneg {J ρ : ℝ} (hJ : 1 ≤ J) (hρ : ρ ≤ 1) :
    0 ≤ curvatureK_real J ρ := by
  simp only [curvatureK_real]
  apply div_nonneg
  · exact mul_nonneg (by linarith) (by linarith)
  · linarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:66

Module Section

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

In the same file