Documentation

Lean 4 Proof

theorem weight_dependent_rho_optimization
    (J : ℕ) (a : Fin J → ℝ) :
    -- ∂ρ*/∂H > 0: more concentrated weights → optimal ρ is higher
    -- At equal weights (H = 1/J): ρ* is minimized (maximum complementarity)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:501

Module Section

## Proposition 3b.7: Weight-Dependent ρ Optimization

In the same file