Documentation

Lean 4 Proof

theorem correlation_robustness_degrades_faster (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T Tstar : ℝ} (_hT : 0 ≤ T) (_hTs : 0 < Tstar) (_hTlt : T < Tstar) :
    -- K_eff² < K_eff when 0 < K_eff < 1 (which happens near T*)
    -- More precisely: (1-T/T*)² < (1-T/T*) when 0 < T < T*
    let f := 1 - T / Tstar
    0 < f → f < 1 → f ^ 2 < f := fun hf hf1 => by
  nlinarith [sq_nonneg (1 - T / Tstar), sq_nonneg (T / Tstar)]

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:83

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file