Documentation

Lean 4 Proof

theorem generalized_crisis_sequence
    (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) (T Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : T < Tstar) :
    -- Within "production", concentrated inputs (high a_j) fail last
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:426

Module Section

## General-Weight Effective Curvature Theorems

In the same file