Documentation

Lean 4 Proof

theorem generalKeff_above_critical
    {J : ℕ} {ρ : ℝ} {a : Fin J → ℝ} {T Tstar : ℝ}
    (hTs : 0 < Tstar) (hT : Tstar ≤ T) :
    generalEffectiveCurvatureKeff J ρ a T Tstar = 0 := by
  unfold generalEffectiveCurvatureKeff
  have h : 1 - T / Tstar ≤ 0 := by
    rw [sub_nonpos]
    rwa [le_div_iff₀ hTs, one_mul]
  rw [max_eq_left h, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:343

Module Section

## General-Weight Effective Curvature Theorems

In the same file