Documentation

Lean 4 Proof

theorem planar_learns_faster {α₀ : ℝ} (hα₀ : 0 < α₀) :
    geometricLearningRate 1 α₀ < geometricLearningRate 2 α₀ :=
  learning_rate_monotone_in_dimension hα₀ (by norm_num)

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GreenTransition.lean:238

Module Section

Green Energy Transition Extension

In the same file