Documentation

Lean 4 Proof

theorem rho_diversity_selection (J : ℕ) (hJ : 2 ≤ J) :
    -- E[K_eff(rho)] >= K_eff(E[rho]) by Jensen's inequality
    -- Strict inequality when Var(rho) > 0 and K_eff concave in rho
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Closure.lean:36

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file