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

Crossing Production

defprovedMacroeconomics

Documentation

Lean 4 Proof

def crossingProduction (p₀ p_d τ β : ℝ) : ℝ := (p₀ / (p_d + τ)) ^ (1 / β)

Dependency Graph

Used by

crossingProduction_decreasing_in_tax planar_crosses_sooner crossing_at_Qstar crossingProduction_decreasing_in_beta crossingProduction_pos

Location

thesis/CESProofs/Macro/GreenTransition.lean:59

Module Section

Green Energy Transition Extension

In the same file

energyCESInner energyCES cleanEnergyShare dirtyEnergyShare cleanEnergyCost effectiveDirtyCost geometricLearningRate energyCESInner_eq_cesInner energyCES_eq_twoFactorCES 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