Documentation

Lean 4 Proof

theorem factorShare_nonneg {a : Fin J → ℝ} {ρ : ℝ} {x : Fin J → ℝ}
    (ha : ∀ j, 0 ≤ a j) (hx : ∀ j, 0 ≤ x j)
    (hden : 0 ≤ ∑ i : Fin J, a i * (x i) ^ ρ) (j : Fin J) :
    0 ≤ factorShare J a ρ x j := by
  simp only [factorShare]
  apply div_nonneg
  · exact mul_nonneg (ha j) (rpow_nonneg (hx j) ρ)
  · exact hden

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:115

Module Section

Economics extensions for CES formalization:

In the same file