Documentation

Lean 4 Proof

theorem adjustmentTimescale_diverges {τ₀ T Tstar : ℝ}
    (hτ : 0 < τ₀) (hTs : 0 < Tstar) (hTlt : T < Tstar) :
    0 < adjustmentTimescale τ₀ T Tstar := by
  simp only [adjustmentTimescale]
  apply div_pos hτ
  rw [sub_pos, div_lt_one hTs]
  exact hTlt

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:212

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file