Documentation

Lean 4 Proof

theorem crossingProduction_decreasing_in_tax {p₀ p_d τ₁ τ₂ β : ℝ}
    (hp₀ : 0 < p₀) (hpdτ₁ : 0 < p_d + τ₁)
    (hβ : 0 < β) (hτ : τ₁ < τ₂) :
    crossingProduction p₀ p_d τ₂ β < crossingProduction p₀ p_d τ₁ β := by
  simp only [crossingProduction]
  have hpdτ₂ : 0 < p_d + τ₂ := by linarith
  apply rpow_lt_rpow (le_of_lt (div_pos hp₀ hpdτ₂))
  · exact div_lt_div_of_pos_left hp₀ hpdτ₁ (by linarith)
  · exact div_pos one_pos hβ

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:144

Module Section

Green Energy Transition Extension

In the same file