Lean 4 Proof

theorem cycle_period_pos {tau_rho tau_T tau_cross1 tau_cross2 : ℝ}
    (h1 : 0 < tau_rho) (h2 : 0 < tau_T)
    (h3 : 0 < tau_cross1) (h4 : 0 < tau_cross2) :
    0 < cyclePeriodEstimate tau_rho tau_T tau_cross1 tau_cross2 := by
  simp only [cyclePeriodEstimate]; linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:234

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file