Documentation

Lean 4 Proof

theorem curvatureKReal_increasing {ρ : ℝ} (hρ : ρ < 1) :
    ∀ J₁ J₂ : ℝ, 0 < J₁ → J₁ < J₂ →
    curvatureKReal J₁ ρ < curvatureKReal J₂ ρ := by
  intro J₁ J₂ hJ₁ hJ₁₂
  simp only [curvatureKReal]
  have h1ρ : 0 < 1 - ρ := by linarith
  have hJ₂ : 0 < J₂ := by linarith
  -- (1-ρ)(J₁-1)/J₁ < (1-ρ)(J₂-1)/J₂
  -- ⟺ (J₁-1)/J₁ < (J₂-1)/J₂  (since 1-ρ > 0)
  -- ⟺ (J₁-1)J₂ < (J₂-1)J₁    (cross multiply)
  -- ⟺ J₁J₂ - J₂ < J₁J₂ - J₁
  -- ⟺ J₁ < J₂  ✓
  rw [div_lt_div_iff₀ hJ₁ hJ₂]
  nlinarith

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:24

Module Section

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

In the same file