Documentation

Lean 4 Proof

theorem criticalFriction_increasing_in_J {J₁ J₂ ρ c d_sq : ℝ}
    (hJ₁ : 1 < J₁) (hJ₁₂ : J₁ < J₂) (hρ : ρ < 1) (hc : 0 < c) (hd : 0 < d_sq) :
    criticalFrictionReal J₁ ρ c d_sq < criticalFrictionReal J₂ ρ c d_sq := by
  have hJ₂ : 1 < J₂ := by linarith
  rw [criticalFrictionReal_eq J₁ ρ c d_sq hJ₁ (by linarith),
      criticalFrictionReal_eq J₂ ρ c d_sq hJ₂ (by linarith)]
  apply div_lt_div_of_pos_right _ (by linarith)
  have hc2 : 0 < c ^ 2 := sq_pos_of_pos hc
  nlinarith [mul_pos hc2 hd]

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:97

Module Section

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

In the same file