CES Multiplier Decreasing In Rho

theorem proved Macroeconomics

Documentation

Lean 4 Proof

theorem cesMultiplier_decreasing_in_rho {J : ℕ} (hJ : 2 ≤ J)
    {ρ1 ρ2 d_sq : ℝ} (hρ : ρ1 < ρ2) (hd : 0 < d_sq) :
    cesMultiplier J ρ2 d_sq < cesMultiplier J ρ1 d_sq := by
  simp only [cesMultiplier]
  exact mul_lt_mul_of_pos_right (curvatureK_decreasing_in_rho hJ hρ) hd

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:52

Module Section

Macroeconomic Applications of the CES Potential

In the same file

cesMultiplier cesMultiplier_pos effectiveMultiplier effectiveMultiplier_nonneg effectiveMultiplier_decreasing_in_T effectiveMultiplier_zero_at_critical fiscal_multiplier_heterogeneity recession_depth_proportional_to_K sectoral_recession_ordering allocationDistortion allocationDistortion_nonneg allocationDistortion_at_zero allocationDistortion_at_critical allocationDistortion_monotone stagflation recession_dual_degradation