Documentation

Lean 4 Proof

theorem canard_delay (epsilon Tdot : ℝ)
    (h_eps : 0 < epsilon) (hTdot : 0 < Tdot) :
    -- tau_delay ~ 1 / sqrt(epsilon * Tdot)
    0 < 1 / Real.sqrt (epsilon * Tdot) := by
  exact div_pos one_pos (Real.sqrt_pos_of_pos (mul_pos h_eps hTdot))

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:292

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file