Documentation

Lean 4 Proof

theorem unnormCES_eq_lpNorm {ρ : ℝ} {x : Fin J → ℝ}
    (hx : ∀ j, 0 ≤ x j) :
    unnormCES J ρ x = lpNorm J ρ x := by
  simp only [unnormCES, lpNorm]
  congr 1
  apply Finset.sum_congr rfl
  intro j _
  rw [abs_of_nonneg (hx j)]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:405

Module Section

Economics extensions for CES formalization:

In the same file