Documentation

Lean 4 Proof

theorem crossingProduction_decreasing_in_beta {p₀ p_d τ β₁ β₂ : ℝ}
    (_hp₀ : 0 < p₀) (hpdτ : 0 < p_d + τ)
    (hβ₁ : 0 < β₁) (_hβ₂ : 0 < β₂) (hβ : β₁ < β₂)
    (hexpensive : p_d + τ < p₀) :
    crossingProduction p₀ p_d τ β₂ < crossingProduction p₀ p_d τ β₁ := by
  simp only [crossingProduction]
  have hbase : 1 < p₀ / (p_d + τ) := by rwa [one_lt_div hpdτ]
  exact rpow_lt_rpow_of_exponent_lt hbase (div_lt_div_of_pos_left one_pos hβ₁ hβ)

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GreenTransition.lean:157

Module Section

Green Energy Transition Extension

In the same file