Documentation

Lean 4 Proof

theorem escortDistribution_hod_zero {x : Fin J → ℝ} (hx : ∀ j, 0 < x j)
    {c : ℝ} (hc : 0 < c) (q : ℝ) (j : Fin J) :
    escortDistribution J q (fun k => c * x k) j = escortDistribution J q x j := by
  simp only [escortDistribution]
  have hrw : ∀ k : Fin J, (c * x k) ^ q = c ^ q * (x k) ^ q :=
    fun k => mul_rpow (le_of_lt hc) (le_of_lt (hx k))
  simp_rw [hrw, ← Finset.mul_sum]
  rw [mul_div_mul_left _ _ (ne_of_gt (rpow_pos_of_pos hc q))]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:873

Module Section

Economics extensions for CES formalization:

In the same file