Documentation

Lean 4 Proof

theorem solowGoldenRule_savings {A α ρ δ : ℝ} (hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0) (hδ : 0 < δ)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L)
    {s : ℝ} (hs : 0 < s)
    (hss : capitalAccumulation s δ (twoFactorCES A α ρ K L) K = 0)
    (hgr : marginalProductK A α ρ K L = δ) :
    s = capitalShare α ρ K L :=
  goldenRule_savings_eq_capitalShare hA hα hα1 hρ hs hδ hK hL hss hgr

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:381

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file