Documentation

Lean 4 Proof

theorem cleanShare_rises_with_relative_input_substitute {α ρ E_c₁ E_c₂ E_d : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hρ : 0 < ρ)
    (hEc₁ : 0 < E_c₁) (_hEc₂ : 0 < E_c₂) (hEd : 0 < E_d)
    (hEc : E_c₁ < E_c₂) :
    cleanEnergyShare α ρ E_c₁ E_d < cleanEnergyShare α ρ E_c₂ E_d := by
  simp only [cleanEnergyShare, capitalShare, cesInner]
  set C := (1 - α) * E_d ^ ρ
  have hC : 0 < C := mul_pos (by linarith) (rpow_pos_of_pos hEd ρ)
  set x₁ := α * E_c₁ ^ ρ
  set x₂ := α * E_c₂ ^ ρ
  have hx₁ : 0 < x₁ := mul_pos hα (rpow_pos_of_pos hEc₁ ρ)
  have hx_lt : x₁ < x₂ :=
    mul_lt_mul_of_pos_left (rpow_lt_rpow (le_of_lt hEc₁) hEc hρ) hα
  rw [div_lt_div_iff₀ (by linarith : 0 < x₁ + C) (by linarith : 0 < x₂ + C)]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:185

Module Section

Green Energy Transition Extension

In the same file