Documentation

Lean 4 Proof

theorem curvatureKReal_bounded {J ρ : ℝ} (hJ : 1 < J) (hρ : ρ < 1) :
    curvatureKReal J ρ < 1 - ρ := by
  simp only [curvatureKReal]
  have hJpos : 0 < J := by linarith
  have h1ρ : 0 < 1 - ρ := by linarith
  -- (1-ρ)(J-1)/J < (1-ρ) ⟺ (J-1)/J < 1 ⟺ J-1 < J
  rw [div_lt_iff₀ hJpos]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:52

Module Section

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

In the same file