Documentation

Lean 4 Proof

theorem eulerSteadyStateReturn_pos {τ_K ρ_time : ℝ}
    (hρ : 0 < ρ_time) (hτ : τ_K < 1) :
    0 < eulerSteadyStateReturn τ_K ρ_time := by
  simp only [eulerSteadyStateReturn]
  exact div_pos hρ (by linarith)

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/Accumulation.lean:142

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file