Documentation

Lean 4 Proof

theorem adjustmentTimescale_monotone {τ₀ T₁ T₂ Tstar : ℝ}
    (hτ : 0 < τ₀) (hTs : 0 < Tstar) (_hT1 : T₁ < Tstar) (_hT2 : T₂ < Tstar)
    (h12 : T₁ ≤ T₂) :
    adjustmentTimescale τ₀ T₁ Tstar ≤ adjustmentTimescale τ₀ T₂ Tstar := by
  simp only [adjustmentTimescale]
  apply div_le_div_of_nonneg_left (le_of_lt hτ)
  · rw [sub_pos, div_lt_one hTs]; linarith
  · 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:221

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file