Documentation

Lean 4 Proof

theorem dispersion_increases_with_K {K₁ K₂ σ_T : ℝ}
    (hK1 : 0 < K₁) (_hK2 : 0 < K₂) (hK12 : K₁ < K₂) (hσ : 0 < σ_T) :
    K₁ ^ 2 * σ_T ^ 2 < K₂ ^ 2 * σ_T ^ 2 := by
  apply mul_lt_mul_of_pos_right _ (by positivity)
  exact sq_lt_sq' (by linarith) hK12

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:108

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file