Documentation

Lean 4 Proof

theorem gen_hessian_equal_marginals (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ)
    (hρ : ρ < 1) (hρne : ρ ≠ 0)
    (ha_pos : ∀ j, 0 < a j) (ha_sum : ∑ j : Fin J, a j = 1) :
    -- At the cost-minimizing point, all marginal products are equal.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralWeights.lean:50

Module Section

General-weight CES results (Paper 1, Section 10):

In the same file