Documentation

Lean 4 Proof

theorem energy_share_identity {α ρ E_c E_d : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hEc : 0 < E_c) (hEd : 0 < E_d) :
    Real.log (dirtyEnergyShare α ρ E_c E_d / cleanEnergyShare α ρ E_c E_d) =
    Real.log ((1 - α) / α) + ρ * Real.log (E_d / E_c) :=
  factorShare_identity hα hα1 hEc hEd

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:172

Module Section

Green Energy Transition Extension

In the same file