Allocation Distortion At Critical

theorem proved Macroeconomics

Documentation

Lean 4 Proof

theorem allocationDistortion_at_critical {Tstar : ℝ} (hTs : 0 < Tstar) :
    allocationDistortion Tstar Tstar = 1 := by
  simp [allocationDistortion, div_self (ne_of_gt hTs)]

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:174

Module Section

Macroeconomic Applications of the CES Potential

In the same file

cesMultiplier cesMultiplier_pos cesMultiplier_decreasing_in_rho 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_monotone stagflation recession_dual_degradation