Documentation

Lean 4 Proof

theorem factorShare_le_one {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) :
    factorShare J a ρ x j ≤ 1 := by
  have hsum := factorShare_sum_eq_one hden
  have hnneg : ∀ k, 0 ≤ factorShare J a ρ x k :=
    factorShare_nonneg ha hx (le_of_lt hden)
  calc factorShare J a ρ x j
      ≤ ∑ k : Fin J, factorShare J a ρ x k :=
        Finset.single_le_sum (fun k _ => hnneg k) (Finset.mem_univ j)
    _ = 1 := hsum

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:147

Module Section

Economics extensions for CES formalization:

In the same file