Documentation

Lean 4 Proof

theorem Keff_zero_at_critical {J : ℕ} {ρ Tstar : ℝ} (hT : 0 < Tstar) :
    effectiveCurvatureKeff J ρ Tstar Tstar = 0 := by
  unfold effectiveCurvatureKeff
  rw [div_self (ne_of_gt hT), sub_self, max_eq_left (le_refl 0), mul_zero]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:284

Module Section

Renormalization Group for CES:

In the same file