Documentation

Lean 4 Proof

theorem superadditivity_with_friction (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T Tstar : ℝ} (hT : 0 ≤ T) (hTs : 0 < Tstar) :
    effectiveCurvatureKeff J ρ T Tstar ≤ curvatureK J ρ :=
  effectiveCurvatureKeff_le_K hJ hρ hT hTs

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:61

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file