Documentation

Lean 4 Proof

theorem planar_crosses_sooner {p₀ p_d τ α₀ : ℝ}
    (hp₀ : 0 < p₀) (hpdτ : 0 < p_d + τ)
    (hα₀ : 0 < α₀) (hexpensive : p_d + τ < p₀) :
    crossingProduction p₀ p_d τ (geometricLearningRate 2 α₀) <
    crossingProduction p₀ p_d τ (geometricLearningRate 1 α₀) :=
  crossingProduction_decreasing_in_beta hp₀ hpdτ
    (by simp [geometricLearningRate]; linarith)
    (by simp [geometricLearningRate]; linarith)
    (planar_learns_faster hα₀) hexpensive

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:257

Module Section

Green Energy Transition Extension

In the same file