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

Effective Multiplier

defprovedMacroeconomics

Documentation

Lean 4 Proof

def effectiveMultiplier (J : ℕ) (ρ T Tstar d_sq : ℝ) : ℝ :=
  effectiveCurvatureKeff J ρ T Tstar * d_sq

Dependency Graph

Used by

fiscal_multiplier_heterogeneity effectiveMultiplier_zero_at_critical stagflation effectiveMultiplier_nonneg effectiveMultiplier_decreasing_in_T

Location

thesis/CESProofs/Potential/MacroApplications.lean:68

Module Section

Macroeconomic Applications of the CES Potential

In the same file

cesMultiplier cesMultiplier_pos cesMultiplier_decreasing_in_rho 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