Documentation

Lean 4 Proof

theorem intermediate_dimension_intermediate_rate {d α₀ : ℝ}
    (hα₀ : 0 < α₀) (hd_lo : 1 < d) (hd_hi : d < 2) :
    geometricLearningRate 1 α₀ < geometricLearningRate d α₀ ∧
    geometricLearningRate d α₀ < geometricLearningRate 2 α₀ :=
  ⟨learning_rate_monotone_in_dimension hα₀ hd_lo,
   learning_rate_monotone_in_dimension hα₀ hd_hi⟩

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:246

Module Section

Green Energy Transition Extension

In the same file