Documentation

Lean 4 Proof

theorem crossing_at_Qstar {p₀ p_d τ β : ℝ}
    (hp₀ : 0 < p₀) (hpdτ : 0 < p_d + τ) (hβ : β ≠ 0) :
    cleanEnergyCost p₀ β (crossingProduction p₀ p_d τ β) =
    effectiveDirtyCost p_d τ := by
  simp only [cleanEnergyCost, crossingProduction, effectiveDirtyCost]
  -- Goal: p₀ * ((p₀ / (p_d + τ)) ^ (1 / β)) ^ (-β) = p_d + τ
  have hbase : (0 : ℝ) ≤ p₀ / (p_d + τ) := le_of_lt (div_pos hp₀ hpdτ)
  -- Combine exponents: (x^{1/β})^{-β} = x^{(1/β)·(-β)} = x^{-1}
  rw [← rpow_mul hbase]
  have hexp : (1 / β * (-β) : ℝ) = -1 := by field_simp
  rw [hexp, rpow_neg_one (p₀ / (p_d + τ)), inv_div]
  -- p₀ * ((p_d + τ) / p₀) = p_d + τ
  field_simp

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:121

Module Section

Green Energy Transition Extension

In the same file