Documentation

Lean 4 Proof

theorem curvatureK_pos {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) :
    0 < curvatureK J ρ := by
  simp only [curvatureK]
  apply div_pos
  · apply mul_pos
    · linarith
    · have hJ1 : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
      linarith
  · exact_mod_cast (by omega : 0 < J)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Defs.lean:141

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file