def twoFactorCES (A α ρ K L : ℝ) : ℝ :=
  A * (cesInner α ρ K L) ^ (1 / ρ)

def capitalShare (α ρ K L : ℝ) : ℝ :=
  α * K ^ ρ / cesInner α ρ K L

theorem euler_two_factor {A α ρ : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L) :
    marginalProductK A α ρ K L * K + marginalProductL A α ρ K L * L =
    twoFactorCES A α ρ K L := by
  simp only [marginalProductK, marginalProductL, twoFactorCES, cesInner]
  set I := α * K ^ ρ + (1 - α) * L ^ ρ with hI_def
  -- Combine x^{ρ-1} · x = x^ρ
  have hK_combine : K ^ (ρ - 1) * K = K ^ ρ := by
    have h := rpow_add hK (ρ - 1) 1
    rw [rpow_one, show ρ - 1 + 1 = ρ from by ring] at h; exact h.symm
  have hL_combine : L ^ (ρ - 1) * L = L ^ ρ := by
    have h := rpow_add hL (ρ - 1) 1
    rw [rpow_one, show ρ - 1 + 1 = ρ from by ring] at h; exact h.symm
  -- Rearrange LHS
  have step1 : A * α * K ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * K +
      A * (1 - α) * L ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * L =
      A * I ^ ((1 - ρ) / ρ) * (α * K ^ ρ + (1 - α) * L ^ ρ) := by
    have lhs_rw1 : A * α * K ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * K =
        A * (α * (K ^ (ρ - 1) * K)) * I ^ ((1 - ρ) / ρ) := by ring
    have lhs_rw2 : A * (1 - α) * L ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * L =
        A * ((1 - α) * (L ^ (ρ - 1) * L)) * I ^ ((1 - ρ) / ρ) := by ring
    rw [lhs_rw1, lhs_rw2, hK_combine, hL_combine]; ring
  rw [step1, ← hI_def]
  -- I^{(1-ρ)/ρ} · I = I^{1/ρ}
  have hI_pos : 0 < I := by rw [hI_def]; exact cesInner_pos hα hα1 hK hL
  rw [show A * I ^ ((1 - ρ) / ρ) * I = A * (I ^ ((1 - ρ) / ρ) * I) from by ring]
  congr 1
  -- I^{(1-ρ)/ρ} * I = I^{1/ρ}
  have h1 : I ^ ((1 - ρ) / ρ + 1) = I ^ ((1 - ρ) / ρ) * I ^ (1 : ℝ) :=
    rpow_add hI_pos _ _
  rw [rpow_one] at h1
  rw [← h1]
  congr 1; field_simp; ring

theorem dtcPremium_threshold_sigma_2 {α K L : ℝ}
    (_hK : 0 < K) (_hL : 0 < L) :
    (α / (1 - α)) * (K / L) ^ ((2 : ℝ) - 2) = α / (1 - α) := by
  rw [show (2 : ℝ) - 2 = 0 from by ring]
  simp [rpow_zero]

theorem dtc_bias_invariant_cobbDouglas {K L : ℝ} (_hK : 0 < K) (_hL : 0 < L) :
    dtcEquilibriumBias 1 (K / L) = 1 := by
  simp only [dtcEquilibriumBias]
  rw [show (1 : ℝ) - 1 = 0 from by ring]
  exact rpow_zero _

theorem crossing_at_Qstar {p₀ p_d τ β : ℝ}
    (hp₀ : 0 < p₀) (hpdτ : 0 < p_d + τ) (hβ : β ≠ 0) :
    cleanEnergyCost p₀ β (crossingProduction p₀ p_d τ β) =
    effectiveDirtyCost p_d τ := by
  simp only [cleanEnergyCost, crossingProduction, effectiveDirtyCost]
  -- Goal: p₀ * ((p₀ / (p_d + τ)) ^ (1 / β)) ^ (-β) = p_d + τ
  have hbase : (0 : ℝ) ≤ p₀ / (p_d + τ) := le_of_lt (div_pos hp₀ hpdτ)
  -- Combine exponents: (x^{1/β})^{-β} = x^{(1/β)·(-β)} = x^{-1}
  rw [← rpow_mul hbase]
  have hexp : (1 / β * (-β) : ℝ) = -1 := by field_simp
  rw [hexp, rpow_neg_one (p₀ / (p_d + τ)), inv_div]
  -- p₀ * ((p_d + τ) / p₀) = p_d + τ
  field_simp

theorem planar_learns_faster {α₀ : ℝ} (hα₀ : 0 < α₀) :
    geometricLearningRate 1 α₀ < geometricLearningRate 2 α₀ :=
  learning_rate_monotone_in_dimension hα₀ (by norm_num)

theorem goldenRule_savings_eq_capitalShare {A α ρ s δ : ℝ} (hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0) (_hs : 0 < s) (_hδ : 0 < δ)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L)
    (hss : capitalAccumulation s δ (twoFactorCES A α ρ K L) K = 0)
    (hgr : marginalProductK A α ρ K L = δ) :
    s = capitalShare α ρ K L := by
  -- From mpk = s_K * Y/K and mpk = δ and s*Y = δ*K (SS):
  -- s_K * Y/K = δ → s_K * Y = δ*K = s*Y → s_K = s
  have hY := twoFactorCES_pos hA hα hα1 hρ hK hL
  have hY_ne := ne_of_gt hY
  have hK_ne := ne_of_gt hK
  have hmk := mpk_eq_capitalShare_times_ypk (show 0 < A from hA) hα hα1 hρ hK hL
  have h_eq := capitalAccumulation_eq_zero_iff.mp hss
  -- hmk: MPK = s_K * (Y / K)
  -- hgr: MPK = δ
  -- h_eq: s * Y = δ * K
  -- So s_K * (Y/K) = δ → s_K * Y = δ * K = s * Y → s_K = s
  rw [hgr] at hmk
  -- hmk: δ = s_K * (Y / K) → s_K * Y = δ * K
  have h1 : capitalShare α ρ K L * twoFactorCES A α ρ K L = δ * K := by
    have := hmk; field_simp at this; linarith
  -- s * Y = δ * K = s_K * Y, so s = s_K
  have h2 : s * twoFactorCES A α ρ K L =
      capitalShare α ρ K L * twoFactorCES A α ρ K L := by linarith
  exact mul_right_cancel₀ hY_ne h2

theorem ramsey_above_goldenRule {τ_K ρ_time δ : ℝ}
    (hρ : 0 < ρ_time) (hτ : τ_K < 1) :
    δ < eulerSteadyStateMPK τ_K ρ_time δ := by
  simp only [eulerSteadyStateMPK]
  have h := eulerSteadyStateReturn_pos hρ hτ
  simp only [eulerSteadyStateReturn] at h
  linarith

theorem growthRate_decreasing {g₀ β τ₁ τ₂ : ℝ}
    (hg : 0 < g₀) (hβ : 0 < β) (hτ : τ₁ < τ₂) :
    growthRate g₀ β τ₂ < growthRate g₀ β τ₁ := by
  simp only [growthRate]
  have h1 : β * τ₁ < β * τ₂ := mul_lt_mul_of_pos_left hτ hβ
  have h2 : 1 - β * τ₂ < 1 - β * τ₁ := by linarith
  exact mul_lt_mul_of_pos_left h2 hg

theorem ramsey_inverse_elasticity {a e₁ e₂ : ℝ}
    (ha : 0 < a) (he₁ : 0 < e₁) (he₂ : 0 < e₂) (he : e₁ < e₂) :
    saezTopRate a e₂ < saezTopRate a e₁ :=
  saezTopRate_decreasing_in_e ha he₁ he₂ he