Documentation

Lean 4 Proof

theorem eulerSteadyStateReturn_increasing_in_τ {τ₁ τ₂ ρ_time : ℝ}
    (hρ : 0 < ρ_time) (_hτ₁ : τ₁ < 1) (_hτ₂ : τ₂ < 1) (hτ : τ₁ < τ₂) :
    eulerSteadyStateReturn τ₁ ρ_time < eulerSteadyStateReturn τ₂ ρ_time := by
  simp only [eulerSteadyStateReturn]
  -- ρ_time/(1-τ₁) < ρ_time/(1-τ₂) because 1-τ₂ < 1-τ₁ (both positive)
  exact div_lt_div_of_pos_left hρ (by linarith) (by linarith)

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/Accumulation.lean:152

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file