Documentation

Lean 4 Proof

theorem generalKeff_le_standardKeff
    {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {a : Fin J → ℝ} (ha_pos : ∀ j, 0 < a j) (ha_sum : ∑ j, a j = 1)
    (T Tstar : ℝ) :
    generalEffectiveCurvatureKeff J ρ a T Tstar
    ≤ effectiveCurvatureKeff J ρ T Tstar := by
  unfold generalEffectiveCurvatureKeff effectiveCurvatureKeff
  apply mul_le_mul_of_nonneg_right
  · exact equalWeights_maximize_K hJ hρ ha_pos ha_sum
  · exact le_max_left 0 _

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:331

Module Section

## General-Weight Effective Curvature Theorems

In the same file