Documentation

Lean 4 Proof

theorem generalKeff_nonneg
    {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {a : Fin J → ℝ} (ha_pos : ∀ j, 0 < a j) (ha_sum : ∑ j, a j = 1)
    (hH : herfindahlIndex J a < 1)
    (T Tstar : ℝ) :
    0 ≤ generalEffectiveCurvatureKeff J ρ a T Tstar := by
  unfold generalEffectiveCurvatureKeff
  apply mul_nonneg
  · exact le_of_lt (gen_quadruple_K_pos hJ hρ ha_pos ha_sum hH)
  · exact le_max_left 0 _

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:318

Module Section

## General-Weight Effective Curvature Theorems

In the same file