Documentation

Lean 4 Proof

theorem T_dependent_selection (T Tstar : ℝ) :
    -- T < T* => Cov(rho, pi) < 0 (selection for complementarity)
    -- T > T* => Cov(rho, pi) > 0 (selection for substitutability)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:127

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file