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

Geometric Learning Rate

defprovedMacroeconomics

Documentation

Lean 4 Proof

def geometricLearningRate (d α₀ : ℝ) : ℝ := d * α₀

Dependency Graph

Used by

planar_crosses_sooner geometric_learning_rate_linear intermediate_dimension_intermediate_rate geometric_learning_rate_planar planar_learns_faster learning_rate_monotone_in_dimension

Location

thesis/CESProofs/Macro/GreenTransition.lean:64

Module Section

Green Energy Transition Extension

In the same file

energyCESInner energyCES cleanEnergyShare dirtyEnergyShare cleanEnergyCost effectiveDirtyCost crossingProduction 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