Documentation

Lean 4 Proof

theorem factorShare_sum_eq_one {a : Fin J → ℝ} {ρ : ℝ} {x : Fin J → ℝ}
    (hden : 0 < ∑ i : Fin J, a i * (x i) ^ ρ) :
    ∑ j : Fin J, factorShare J a ρ x j = 1 := by
  simp only [factorShare]
  simp_rw [div_eq_mul_inv]
  rw [← Finset.sum_mul]
  exact mul_inv_cancel₀ (ne_of_gt hden)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:127

Module Section

Economics extensions for CES formalization:

In the same file