Documentation

Lean 4 Proof

theorem asymmetry_exceeds_one (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {ε : ℝ} (hε : 0 < ε) :
    1 < asymmetryRatio J ρ ε := by
  simp only [asymmetryRatio]
  linarith [curvatureK_pos hJ hρ, mul_pos (curvatureK_pos hJ hρ) hε]

Dependency Graph

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:49

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file