Documentation

Lean 4 Proof

theorem degradation_monotone {T₁ T₂ Tstar : ℝ} (hTs : 0 < Tstar)
    (h12 : T₁ ≤ T₂) :
    max 0 (1 - T₂ / Tstar) ≤ max 0 (1 - T₁ / Tstar) := by
  apply max_le_max_left 0
  apply sub_le_sub_left
  exact div_le_div_of_nonneg_right h12 (le_of_lt hTs)

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:159

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file