Sections / Section 14: Macro -- Two-Factor CES, Growth, Tax / energyCES_eq_twoFactorCES

Energy CES Eq Two Factor CES

theoremprovedMacroeconomics

Documentation

Lean 4 Proof

theorem energyCES_eq_twoFactorCES {α ρ E_c E_d : ℝ} :
    energyCES α ρ E_c E_d = twoFactorCES 1 α ρ E_c E_d := rfl

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:75

Module Section

Green Energy Transition Extension

In the same file

energyCESInner energyCES cleanEnergyShare dirtyEnergyShare cleanEnergyCost effectiveDirtyCost crossingProduction geometricLearningRate energyCESInner_eq_cesInner energyCESInner_pos energy_shares_sum_one cleanEnergyCost_eq_wright cleanEnergyCost_pos cleanEnergyCost_decreasing crossing_at_Qstar crossingProduction_pos crossingProduction_decreasing_in_tax crossingProduction_decreasing_in_beta energy_share_identity cleanShare_rises_with_relative_input_substitute