Documentation

Lean 4 Proof

theorem effectiveCurvatureKeff_le_K (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T Tstar : ℝ} (hT : 0 ≤ T) (hTs : 0 < Tstar) :
    effectiveCurvatureKeff J ρ T Tstar ≤ curvatureK J ρ := by
  simp only [effectiveCurvatureKeff]
  have hK : 0 < curvatureK J ρ := curvatureK_pos hJ hρ
  have h1 : max 0 (1 - T / Tstar) ≤ 1 := by
    apply max_le (by linarith)
    rw [sub_le_self_iff]
    exact div_nonneg hT (le_of_lt hTs)
  calc curvatureK J ρ * max 0 (1 - T / Tstar)
      ≤ curvatureK J ρ * 1 := by
        exact mul_le_mul_of_nonneg_left h1 (le_of_lt hK)
    _ = curvatureK J ρ := by ring

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Defs.lean:173

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file