Documentation

Lean 4 Proof

def lpNorm (J : ℕ) (p : ℝ) (x : Fin J → ℝ) : ℝ :=
  (∑ j : Fin J, |x j| ^ p) ^ (1 / p)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:401

Module Section

Economics extensions for CES formalization:

In the same file