Documentation

Lean 4 Proof

theorem steadyStateKY_increasing_in_s {s₁ s₂ δ : ℝ} (hδ : 0 < δ)
    (hs : s₁ < s₂) :
    steadyStateKY s₁ δ < steadyStateKY s₂ δ := by
  simp only [steadyStateKY]
  exact div_lt_div_of_pos_right hs hδ

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:98

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file