Documentation

Lean 4 Proof

theorem Keff_linear_near_critical {J : ℕ} {ρ T Tstar : ℝ}
    (hT : 0 < Tstar) (hTlt : T < Tstar) :
    effectiveCurvatureKeff J ρ T Tstar =
    curvatureK J ρ * (1 - T / Tstar) := by
  unfold effectiveCurvatureKeff
  have h : 0 < 1 - T / Tstar := by rw [sub_pos, div_lt_one hT]; exact hTlt
  rw [max_eq_right h.le]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:273

Module Section

Renormalization Group for CES:

In the same file