Documentation

Lean 4 Proof

theorem energy_shares_sum_one {α ρ E_c E_d : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hEc : 0 < E_c) (hEd : 0 < E_d) :
    cleanEnergyShare α ρ E_c E_d + dirtyEnergyShare α ρ E_c E_d = 1 :=
  capitalShare_plus_laborShare (ρ := ρ) hα hα1 hEc hEd

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:85

Module Section

Green Energy Transition Extension

In the same file