Documentation

Lean 4 Proof

theorem learning_rate_monotone_in_dimension {d₁ d₂ α₀ : ℝ}
    (hα₀ : 0 < α₀) (hd : d₁ < d₂) :
    geometricLearningRate d₁ α₀ < geometricLearningRate d₂ α₀ := by
  simp only [geometricLearningRate]; nlinarith

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GreenTransition.lean:229

Module Section

Green Energy Transition Extension

In the same file