Documentation

Lean 4 Proof

theorem hysteresis_wider_for_complements {ρ₁ ρ₂ : ℝ}
    (_hρ₁ : ρ₁ < 1) (_hρ₂ : ρ₂ < 1) (hρ : ρ₁ < ρ₂)
    {bf : ℝ} (hbf : 0 < bf) :
    hysteresisWidth ρ₂ bf < hysteresisWidth ρ₁ bf :=
  hysteresisWidth_increasing_in_complementarity hρ hbf

Dependency Graph

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:96

Module Section

Paper 3c, Section 3: First-Order Regime Shift

In the same file