The finite coordinate power functional and its norm range
DefinitionHlawkaSchatten_DiagonalConstruction_BasicFor a finite index set , a normed abelian group (NormedAddCommGroup), a real exponent , and a family with each , lpNorm defines
The formula is defined for every real exponent , using Lean's totalized real power and division. For , it is a norm and satisfies the triangle inequality. The formula also has uses outside this norm range; no converse about a particular index set or space is asserted here.
This is the coordinate-explicit stand-in used throughout the diagonal construction for the exponent-indexed PiLp norm: writing the finite power sum directly, rather than through the PiLp type, keeps later constructions independent of that type's exponent index while still inheriting the same norm laws once .
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.Normed.Lp.PiLp
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
/-
Copyright (c) 2026 Ezzeri Esa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ezzeri Esa
-/
/-!
# Coordinate norms for the diagonal construction
The explicit finite power sum keeps coordinate arguments independent of
the exponent-indexed `PiLp` type. Its norm laws are inherited from `PiLp`.
-/
namespace HlawkaSchatten.DiagonalConstruction
variable {ι E : Type*} [Fintype ι] [NormedAddCommGroup E]
/-- The finite coordinate `p`-norm, with a real exponent. -/
noncomputable def lpNorm (p : ℝ) (x : ι → E) : ℝ :=
(∑ i, ‖x i‖ ^ p) ^ (1 / p)
end HlawkaSchatten.DiagonalConstruction
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.