Documentation

Lean 4 Proof

theorem ces_third_derivative_pos (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) :
    0 < cesThirdDerivValue J ρ c := by
  simp only [cesThirdDerivValue]
  apply mul_pos
  · exact div_pos (curvatureK_pos hJ hρ) (mul_pos (by positivity) (sq_pos_of_pos hc))
  · have hJ1 : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
    have hJge2 : (2 : ℝ) ≤ ↑J := by exact_mod_cast hJ
    nlinarith [mul_nonneg (by linarith : (0 : ℝ) ≤ 1 - ρ) (by linarith : (0 : ℝ) ≤ ↑J - 2)]

Dependency Graph

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:28

Module Section

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

In the same file