Documentation

Lean 4 Proof

theorem cleanEnergyCost_decreasing {p₀ β Q₁ Q₂ : ℝ}
    (hp₀ : 0 < p₀) (hβ : 0 < β) (hQ₁ : 0 < Q₁) (_hQ₂ : 0 < Q₂)
    (hQ : Q₁ < Q₂) :
    cleanEnergyCost p₀ β Q₂ < cleanEnergyCost p₀ β Q₁ :=
  wright_law_decreasing hp₀ hβ hQ₁ _hQ₂ hQ

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:106

Module Section

Green Energy Transition Extension

In the same file