Documentation

Lean 4 Proof

theorem productivity_dispersion_amplification {K σ_T : ℝ} (hK : 0 < K) (hσ : 0 < σ_T) :
    -- The systematic component K²·σ_T² is positive and increasing in K
    0 < K ^ 2 * σ_T ^ 2 := by positivity

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:103

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file