Sections / Section 9: CES Potential and Information Friction / allocationDistortion_monotone

Allocation Distortion Monotone

theoremprovedMacroeconomics

Documentation

Lean 4 Proof

theorem allocationDistortion_monotone {T1 T2 Tstar : ℝ} (hTs : 0 < Tstar)
    (h : T1 ≤ T2) :
    allocationDistortion T1 Tstar ≤ allocationDistortion T2 Tstar := by
  simp only [allocationDistortion]
  linarith [degradation_monotone hTs h]

Dependency Graph

Used by

multisector_stagflation stagflation

Location

thesis/CESProofs/Potential/MacroApplications.lean:180

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_at_critical stagflation recession_dual_degradation