Documentation

Lean 4 Proof

theorem secular_equation (J : ℕ) (w : Fin J → ℝ) (hw : StrictMono w) :
    -- The secular equation Σ 1/(wⱼ - μ) = 0 has exactly J-1 roots,
    -- one in each open interval (w_{(k)}, w_{(k+1)}).
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralWeights.lean:91

Module Section

General-weight CES results (Paper 1, Section 10):

In the same file