Complemented subspacesPaper & formalisation
The mathematical vocabulary

Definitions, made explicit

The project’s definitions are shown with their exact source, mathematical meaning, and context. Standard Mathlib notions are identified separately below.

20 of 20 project definitions

Project-defined

basisMultiplier

Mb,θ ⁣(∑i=0n−1xibi)=∑i=0n−1θixibi,θ∈Rn.M_{b,\theta}\!\left(\sum_{i=0}^{n-1}x_i b_i\right)=\sum_{i=0}^{n-1}\theta_i x_i b_i,\qquad \theta\in\mathbb R^n.

The bounded linear operator that multiplies the coordinates of a finite real algebraic basis by the chosen real scalars. The basis makes the space finite-dimensional, so constrL also ensures continuity.

The definition of the operator allows arbitrary θ; the bound |θ_i| ≤ 1 enters the unconditional constant.

Exact Lean source excerpt
def basisMultiplier {n : ℕ} (b : Module.Basis (Fin n) ℝ E)
    (θ : Fin n → ℝ) : E →L[ℝ] E :=
  b.constrL (fun i => θ i • b i)

View sourceLocalUnconditional.lean · lines 49–51

Project-defined

unconditionalBasisConstant

u(b)=max⁡{1,sup⁡θ∈[−1,1]n∥Mb,θ∥}.u(b)=\max\left\{1,\sup_{\theta\in[-1,1]^n}\|M_{b,\theta}\|\right\}.

The unconditional constant of one finite real basis, measured in the existing norm of E. Every real scalar multiplier of modulus at most one is included. The maximum with one fixes the zero-dimensional convention.

The codomain is ℝ≥0∞, the extended nonnegative reals; ‖T‖ₑ is the operator norm embedded there.

Exact Lean source excerpt
def unconditionalBasisConstant {n : ℕ} (b : Module.Basis (Fin n) ℝ E) : ℝ≥0∞ :=
  max 1 (⨆ (θ : Fin n → ℝ) (_ : ∀ i, ‖θ i‖ ≤ 1), ‖basisMultiplier b θ‖ₑ)

View sourceLocalUnconditional.lean · lines 62–63

Related: basisMultiplier

Project-defined

unconditionalConstant

u(E)=inf⁡n∈N inf⁡b a basis of E indexed by {0,…,n−1}u(b).u(E)=\inf_{n\in\mathbb N}\ \inf_{b\text{ a basis of }E\text{ indexed by }\{0,\ldots,n-1\}}u(b).

The best finite-basis unconditional constant in the given norm. This is an infimum over all finite bases, with no claim that an optimal basis exists.

If E has no finite basis this infimum is ∞; the empty basis gives u({0}) = 1.

Exact Lean source excerpt
def unconditionalConstant (E : Type*) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : ℝ≥0∞ :=
  ⨅ (n : ℕ) (b : Module.Basis (Fin n) ℝ E), unconditionalBasisConstant b

View sourceLocalUnconditional.lean · lines 109–111

Related: unconditionalBasisConstant

Project-defined

lambdaDPR

λDPR(Z,V)=inf⁡{u(F):V⊆F⊆Z, dim⁡F<∞}.\lambda_{\mathrm{DPR}}(Z,V)=\inf\{u(F):V\subseteq F\subseteq Z,\ \dim F<\infty\}.

One starts with a real linear subspace V of Z and enlarges it to a finite-dimensional subspace F of the same Z. Both subspaces carry their inherited norms.

The definition accepts arbitrary V; finite dimensionality is imposed when taking the outer supremum.

Exact Lean source excerpt
def lambdaDPR (V : Submodule ℝ Z) : ℝ≥0∞ :=
  ⨅ (F : Submodule ℝ Z) (_ : V ≤ F) (_ : FiniteDimensional ℝ ↥F),
    unconditionalConstant ↥F

View sourceLocalUnconditional.lean · lines 125–127

Related: unconditionalConstant

Project-defined

chiDPR

χDPR(Z)=sup⁡V⊆Z0<dim⁡V<∞λDPR(Z,V).\chi_{\mathrm{DPR}}(Z)=\sup_{\substack{V\subseteq Z\\0<\dim V<\infty}}\lambda_{\mathrm{DPR}}(Z,V).

The supremum of the local DPR constants over nonzero finite-dimensional real subspaces. Equality to ∞ means that there is no finite uniform bound.

The zero subspace is excluded. An empty supremum is zero, so χDPR({0}) = 0.

Exact Lean source excerpt
def chiDPR : ℝ≥0∞ :=
  ⨆ (V : Submodule ℝ Z) (_ : FiniteDimensional ℝ ↥V) (_ : V ≠ ⊥),
    lambdaDPR Z V

View sourceLocalUnconditional.lean · lines 130–132

Related: lambdaDPR

Project-defined

GLFactorization

U=(Rn,ν),ν(θ⋅x)≤ν(x)(∣θi∣≤1),a:V→U,b:U→Z,ba=ιV,A,B≥0,ν(ax)≤A∥x∥,∥by∥≤Bν(y).\begin{gathered}U=(\mathbb R^n,\nu),\quad \nu(\theta\cdot x)\leq\nu(x)\quad(|\theta_i|\leq1),\\a:V\to U,\quad b:U\to Z,\quad ba=\iota_V,\\A,B\geq0,\quad \nu(ax)\leq A\|x\|,\quad\|by\|\leq B\nu(y).\end{gathered}

A finite factorisation of the inclusion V → Z. The auxiliary norm ν is defined by a positive-definite real seminorm, and coordinate multipliers are required to be contractions. The linear maps carry explicit finite nonnegative bounds A and B, which make them bounded for that auxiliary norm.

The auxiliary norm is arbitrary subject to these conditions; it is not restricted to a particular ℓp norm.

No injectivity condition is imposed on b. Injectivity of a follows from ba = inclusion.

The coordinate carrier Fin n → ℝ does not mean that the auxiliary norm is the default supremum norm.

The conversions between finite-dimensional representations are in LocalUnconditional.lean: ofUnconditionalBasis 220–254, ofUnconditionalBasis_cost 257–264, Aux and its norm/complete-space instances 272–298, auxBasis_unconditional 314–324, auxA/auxB and aux_factorizes 327–336, aux_cost_le 347–351.

Exact Lean source excerpt
structure GLFactorization (V : Submodule ℝ Z) where
  dimension : ℕ
  auxNorm : Seminorm ℝ (Fin dimension → ℝ)
  positive_definite : ∀ x, auxNorm x = 0 → x = 0
  unconditional : ∀ (θ x : Fin dimension → ℝ),
    (∀ i, ‖θ i‖ ≤ 1) → auxNorm (fun i => θ i * x i) ≤ auxNorm x
  a : ↥V →ₗ[ℝ] (Fin dimension → ℝ)
  b : (Fin dimension → ℝ) →ₗ[ℝ] Z
  factorizes : b.comp a = V.subtype
  aBound : ℝ≥0
  bBound : ℝ≥0
  bound_a : ∀ x : ↥V, auxNorm (a x) ≤ (aBound : ℝ) * ‖x‖
  bound_b : ∀ x : Fin dimension → ℝ, ‖b x‖ ≤ (bBound : ℝ) * auxNorm x

View sourceLocalUnconditional.lean · lines 159–171

Project-defined

GLFactorization.cost

cost⁡(F)=AFBF∈[0,∞].\operatorname{cost}(F)=A_F B_F\in[0,\infty].

The product of the two certified bounds in a factorisation. These bounds need not be the smallest possible bounds; all admissible choices are included in the subsequent infimum.

Exact Lean source excerpt
def GLFactorization.cost {V : Submodule ℝ Z} (F : GLFactorization V) : ℝ≥0∞ :=
  (F.aBound : ℝ≥0∞) * (F.bBound : ℝ≥0∞)

View sourceLocalUnconditional.lean · lines 174–175

Related: GLFactorization

Project-defined

lambdaGL

λGL(Z,V)=inf⁡F∈GLFactorization⁡(V)cost⁡(F).\lambda_{\mathrm{GL}}(Z,V)=\inf_{F\in\operatorname{GLFactorization}(V)}\operatorname{cost}(F).

The infimum over every finite coordinate factorisation of the inclusion, including every admissible auxiliary unconditional norm and every certified pair of operator bounds.

The source converts bounded-operator factorisations into these witnesses using their exact operator norms, and converts witnesses back without increasing cost.

Exact Lean source excerpt
def lambdaGL (V : Submodule ℝ Z) : ℝ≥0∞ :=
  ⨅ F : GLFactorization V, F.cost

View sourceLocalUnconditional.lean · lines 359–360

Related: GLFactorizationGLFactorization.cost

Project-defined

chiGL

χGL(Z)=sup⁡V⊆Z0<dim⁡V<∞λGL(Z,V).\chi_{\mathrm{GL}}(Z)=\sup_{\substack{V\subseteq Z\\0<\dim V<\infty}}\lambda_{\mathrm{GL}}(Z,V).

The project’s real GL local unconditional structure constant: take the local factorisation infimum for each nonzero finite-dimensional real subspace, then take the supremum.

This name refers to the definition above. The project does not identify it with a separately defined operator-ideal constant.

Exact Lean source excerpt
def chiGL : ℝ≥0∞ :=
  ⨆ (V : Submodule ℝ Z) (_ : FiniteDimensional ℝ ↥V) (_ : V ≠ ⊥),
    lambdaGL Z V

View sourceLocalUnconditional.lean · lines 364–366

Related: lambdaGL

Project-defined

BlockParameters

Nj∈N>0,2<pj≤3,pj+1≤pj,lim⁡j→∞pj=2.N_j\in\mathbb N_{>0},\qquad 2<p_j\leq3,\qquad p_{j+1}\leq p_j,\qquad\lim_{j\to\infty}p_j=2.

The positive finite dimensions and real exponents of the countable block sum. Antitone means nonincreasing, not strictly decreasing. Lean indexes the sequence starting at zero.

Exact Lean source excerpt
structure BlockParameters where
  dimension : ℕ → ℕ+
  exponent : ℕ → ℝ
  two_lt_exponent : ∀ j, 2 < exponent j
  exponent_le_three : ∀ j, exponent j ≤ 3
  exponent_antitone : Antitone exponent
  exponent_tendsto : Filter.Tendsto exponent Filter.atTop (𝓝 2)

View sourceAmbient.lean · lines 23–29

Project-defined

Block

Block⁡(a,j)=ℓpjNj(R),∥x∥=(∑i=0Nj−1∣xi∣pj)1/pj.\operatorname{Block}(a,j)=\ell_{p_j}^{N_j}(\mathbb R),\qquad\|x\|=\left(\sum_{i=0}^{N_j-1}|x_i|^{p_j}\right)^{1/p_j}.

A finite PiLp space over ℝ at the exponent specified by a. The sum in the norm uses counting measure; it is not divided by the dimension.

The local Fact (1 ≤ ENNReal.ofReal (a.exponent j)) instance in Ambient.lean 31–36 specifies the normed-space side condition.

Exact Lean source excerpt
abbrev Block (a : BlockParameters) (j : ℕ) :=
  PiLp (ENNReal.ofReal (a.exponent j)) (fun _ : Fin (a.dimension j) => ℝ)

View sourceAmbient.lean · lines 39–40

Related: BlockParameters

Project-defined

Ambient

Xa=(⨁j∈NℓpjNj(R))2,∥x∥=(∑j=0∞∥xj∥pj2)1/2.X_a=\left(\bigoplus_{j\in\mathbb N}\ell_{p_j}^{N_j}(\mathbb R)\right)_2,\qquad\|x\|=\left(\sum_{j=0}^{\infty}\|x_j\|_{p_j}^{2}\right)^{1/2}.

The dependent ℓ² sum of the finite blocks: vectors are block sequences with square-summable block norms. The abbreviation selects Mathlib’s lp construction, whose type is an additive subgroup coerced to its carrier.

Exact Lean source excerpt
abbrev Ambient (a : BlockParameters) := lp (Block a) 2

View sourceAmbient.lean · lines 43–43

Related: Block

Project-defined

HasRealBanachLatticeOrder

∃ a lattice order on X:x≤y⇒x+z≤y+z,t≥0, x≤y⇒tx≤ty,∣x∣≤∣y∣⇒∥x∥≤∥y∥.\exists\ \text{a lattice order on }X:\quad x\leq y\Rightarrow x+z\leq y+z,\quad t\geq0,\ x\leq y\Rightarrow tx\leq ty,\quad |x|\leq|y|\Rightarrow\|x\|\leq\|y\|.

On a complete normed real vector space with its existing norm, there is a compatible lattice order. The order must respect addition and nonnegative scalar multiplication, and the norm must be solid.

The predicate assumes that X is complete. Only the order is existentially chosen; the existing norm is retained.

Exact Lean source excerpt
def HasRealBanachLatticeOrder (X : Type*) [NormedAddCommGroup X]
    [NormedSpace ℝ X] [CompleteSpace X] : Prop :=
  ∃ latticeOrder : Lattice X,
    letI : Lattice X := latticeOrder
    IsOrderedAddMonoid X ∧ PosSMulMono ℝ X ∧ HasSolidNorm X

View sourceTheoremStatement.lean · lines 34–38

Project-defined

HasSeparatedRange

Z=ran⁡P,χGL(Z)≤∥P∥,χDPR(Z)=∞,χGL(Z∗)≤∥P∥,χDPR(Z∗)=∞.Z=\operatorname{ran}P,\quad\chi_{\mathrm{GL}}(Z)\leq\|P\|,\quad\chi_{\mathrm{DPR}}(Z)=\infty,\quad\chi_{\mathrm{GL}}(Z^*)\leq\|P\|,\quad\chi_{\mathrm{DPR}}(Z^*)=\infty.

Combines the four local-structure conditions for the range and its continuous real dual. The range has the inherited subspace norm, and its dual has the operator norm.

The predicate itself does not require P² = P; idempotence is a separate clause of the main theorem.

Applied to I − P, its bound is ‖I − P‖, because the predicate uses the norm of its own argument.

Exact Lean source excerpt
def HasSeparatedRange {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (P : X →L[ℝ] X) : Prop :=
  chiGL ↥P.range ≤ ‖P‖ₑ ∧
  chiDPR ↥P.range = ⊤ ∧
  chiGL (↥P.range →L[ℝ] ℝ) ≤ ‖P‖ₑ ∧
  chiDPR (↥P.range →L[ℝ] ℝ) = ⊤

View sourceTheoremStatement.lean · lines 42–47

Related: chiGLchiDPR

Project-defined

BanachModel

BK=(X,∥⋅∥,K-vector structure,completeness).\mathcal B_{\mathbb K}=(X,\|\cdot\|,\mathbb K\text{-vector structure},\text{completeness}).

A bundled Banach-space witness: an underlying type, a normed additive group, a compatible normed vector-space structure over the field, and completeness. This lets existential statements choose the space and its norm together.

The selected corollaries quantify over BanachModel.{0}; the renormability and nonlattice predicates use a model in the same universe as E.

Exact Lean source excerpt
structure BanachModel (𝕜 : Type*) [NontriviallyNormedField 𝕜] where
  Carrier : Type u
  normedGroup : NormedAddCommGroup Carrier
  normedSpace : letI := normedGroup; NormedSpace 𝕜 Carrier
  completeSpace : letI := normedGroup; CompleteSpace Carrier

View sourceCorollaryStatement.lean · lines 25–29

Project-defined

HasUnconditionalSchauderBasis

(∃n∈N, (bi)i<n is an unconditional Schauder basis of E) ∨ (∃(bi)i∈N an unconditional Schauder basis of E).\bigl(\exists n\in\mathbb N,\ (b_i)_{i<n}\text{ is an unconditional Schauder basis of }E\bigr)\ \lor\ \bigl(\exists(b_i)_{i\in\mathbb N}\text{ an unconditional Schauder basis of }E\bigr).

There is either a finite unconditional Schauder basis or one indexed by ℕ, using Mathlib’s continuous coordinate functionals and unconditional norm convergence of finite partial sums.

Finite bases include the empty basis of the zero space. Nonempty packages existence of a basis object.

Exact Lean source excerpt
def HasUnconditionalSchauderBasis (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=
  (∃ n : ℕ, Nonempty (UnconditionalSchauderBasis (Fin n) 𝕜 E)) ∨
    Nonempty (UnconditionalSchauderBasis ℕ 𝕜 E)

View sourceCorollaryStatement.lean · lines 40–43

Project-defined

IsOneUnconditional

∀s⊂N finite, ∀θ∈KN (∣θi∣≤1), ∀x∈E:∥∑i∈sθibi∗(x)bi∥≤∥x∥.\forall s\subset\mathbb N\text{ finite},\ \forall\theta\in\mathbb K^{\mathbb N}\ (|\theta_i|\leq1),\ \forall x\in E:\quad\left\|\sum_{i\in s}\theta_i b_i^*(x)b_i\right\|\leq\|x\|.

Every finite coordinate multiplier of an ℕ-indexed unconditional Schauder basis is contractive. The condition uses all scalars of modulus at most one; over ℂ it includes all complex phases.

Exact Lean source excerpt
def IsOneUnconditional (b : UnconditionalSchauderBasis ℕ 𝕜 E) : Prop :=
  ∀ (s : Finset ℕ) (θ : ℕ → 𝕜), (∀ i, ‖θ i‖ ≤ 1) →
    ∀ x : E, ‖∑ i ∈ s, (θ i * b.coord i x) • b i‖ ≤ ‖x‖

View sourceCorollaryStatement.lean · lines 47–49

Project-defined

HasOneUnconditionalSchauderBasis

∃(bi)i∈N an unconditional Schauder basis of E: IsOneUnconditional⁡(b).\exists(b_i)_{i\in\mathbb N}\text{ an unconditional Schauder basis of }E:\ \operatorname{IsOneUnconditional}(b).

Existence of an ℕ-indexed unconditional Schauder basis satisfying the finite multiplier contraction condition. This is the positive ambient-space witness in the corollaries.

This positive predicate uses ℕ; the negative range predicate HasUnconditionalSchauderBasis also counts finite bases.

Exact Lean source excerpt
def HasOneUnconditionalSchauderBasis (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=
  ∃ b : UnconditionalSchauderBasis ℕ 𝕜 E, IsOneUnconditional b

View sourceCorollaryStatement.lean · lines 55–57

Related: IsOneUnconditional

Project-defined

IsSuperreflexiveByRenorming

∃H a complete uniformly convex normed K-space:E≃H by a bounded linear isomorphism.\exists H\text{ a complete uniformly convex normed }\mathbb K\text{-space}:\quad E\simeq H\text{ by a bounded linear isomorphism}.

The convention used for superreflexivity in the separable nonprimarity statement: E is boundedly linearly isomorphic to a complete uniformly convex normed space.

The project does not prove equivalence here with a separately formalised finite-representability definition of superreflexivity. The real main theorem directly asks for uniform convexity of the displayed ambient norm.

Exact Lean source excerpt
def IsSuperreflexiveByRenorming (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=
  ∃ H : BanachModel.{u} 𝕜,
    UniformConvexSpace H.Carrier ∧ Nonempty (E ≃L[𝕜] H.Carrier)

View sourceCorollaryStatement.lean · lines 60–63

Related: BanachModel

Project-defined

IsIsomorphicToRealBanachLattice

∃L a real Banach space:L has a compatible Banach lattice order,E≃L by a bounded real-linear isomorphism.\exists L\text{ a real Banach space}:\quad L\text{ has a compatible Banach lattice order},\quad E\simeq L\text{ by a bounded real-linear isomorphism}.

There exists some Banach-space model L carrying a compatible lattice order and a continuous real-linear equivalence from E to L. Thus its negation excludes all such Banach lattice models, including models with a different norm.

The chosen model lies in the same type universe as E. No order-preservation condition is imposed on the isomorphism.

Exact Lean source excerpt
def IsIsomorphicToRealBanachLattice (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] : Prop :=
  ∃ L : BanachModel.{u} ℝ,
    HasRealBanachLatticeOrder L.Carrier ∧ Nonempty (E ≃L[ℝ] L.Carrier)

View sourceCorollaryStatement.lean · lines 67–70

Related: BanachModelHasRealBanachLatticeOrder

Standard library

Definitions from Mathlib

These are established library notions used by the project. The local source excerpts record the pinned revision; online documentation may describe a newer revision.

Standard Mathlib notion

ContinuousLinearMap

E→LKF={T:E→F:T is linear and continuous}.E\to_L^{\mathbb K}F=\{T:E\to F:T\text{ is linear and continuous}\}.

In these normed spaces, →L[𝕜] means a bounded linear operator. Its operator norm is used for projection and dual norms. The underlying generic Mathlib structure also supports semilinear maps.

Pinned Mathlib source excerpt
structure ContinuousLinearMap {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
    (M : Type*) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type*) [TopologicalSpace M₂]
    [AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₛₗ[σ] M₂ where
  cont : Continuous toFun := by
    first | fun_prop | eta_expand; dsimp; fun_prop | skip
Pinned sourceMathlib documentation ↗
Standard Mathlib notion

UniformConvexSpace

∀ε>0 ∃δ>0:∥x∥=∥y∥=1, ∥x−y∥≥ε⇒∥x+y∥≤2−δ.\forall\varepsilon>0\ \exists\delta>0:\quad\|x\|=\|y\|=1,\ \|x-y\|\geq\varepsilon\Rightarrow\|x+y\|\leq2-\delta.

Uniform convexity is a property of the given norm. The local Mathlib class uses this sphere formulation.

Pinned Mathlib source excerpt
class UniformConvexSpace (E : Type*) [SeminormedAddCommGroup E] : Prop where
  uniform_convex : ∀ ⦃ε : ℝ⦄,
    0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
Pinned sourceMathlib documentation ↗
Standard Mathlib notion

TopologicalSpace.SeparableSpace

∃D⊆X:D is countable and D‾=X.\exists D\subseteq X:\quad D\text{ is countable and }\overline D=X.

Existence of a countable dense subset in the given topology.

Pinned Mathlib source excerpt
@[mk_iff] class SeparableSpace : Prop where
  /-- There exists a countable dense set. -/
  exists_countable_dense : ∃ s : Set α, s.Countable ∧ Dense s
Pinned sourceMathlib documentation ↗
Standard Mathlib notion

Submodule

V⊆Z,0∈V,V+V⊆V,KV⊆V.V\subseteq Z,\qquad0\in V,\quad V+V\subseteq V,\quad\mathbb K V\subseteq V.

A bundled linear subspace. It is not required to be topologically closed by this definition. The notation ↥V denotes its carrier as a type, inheriting the subspace norm in the statements.

Pinned Mathlib source excerpt
structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
    extends AddSubmonoid M, SubMulAction R M
Pinned sourceMathlib documentation ↗
Standard Mathlib notion

lp

ℓ2(Ej)={(xj):∑j∥xj∥2<∞}.\ell^2(E_j)=\{(x_j):\sum_j\|x_j\|^2<\infty\}.

The dependent ℓp construction; the displayed formula is its p = 2 specialisation used by Ambient. The general definition uses the Memℓp predicate.

Pinned Mathlib source excerpt
def lp (E : α → Type*) [∀ i, NormedAddCommGroup (E i)] (p : ℝ≥0∞) : AddSubgroup (PreLp E) where
  carrier := { f | Memℓp f p }
  zero_mem' := zero_memℓp
  add_mem' := Memℓp.add
  neg_mem' := Memℓp.neg
Pinned sourceMathlib documentation ↗
Standard Mathlib notion

PiLp

∥(xi)i<n∥p=(∑i<n∥xi∥p)1/p(1≤p<∞).\left\|(x_i)_{i<n}\right\|_p=\left(\sum_{i<n}\|x_i\|^p\right)^{1/p}\quad(1\leq p<\infty).

A type synonym for a product carrying the indicated ℓp norm. The displayed finite-p formula is the case used in Block.

Pinned Mathlib source excerpt
abbrev PiLp (p : ℝ≥0∞) {ι : Type*} (α : ι → Type*) : Type _ :=
  WithLp p (∀ i : ι, α i)
Pinned sourceMathlib documentation ↗
Standard Mathlib notion

UnconditionalSchauderBasis

bi∗(bj)=δij,x=∑ibi∗(x)bi unconditionally in norm.b_i^*(b_j)=\delta_{ij},\qquad x=\sum_i b_i^*(x)b_i\text{ unconditionally in norm}.

An abbreviation for GeneralSchauderBasis with the unconditional summation filter. GeneralSchauderBasis 105–115 stores the vectors, continuous coordinate functionals, biorthogonality and expansion.

Pinned Mathlib source excerpt
abbrev UnconditionalSchauderBasis (β : Type*)
    (𝕜 : Type*) (X : Type*) [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] :=
  GeneralSchauderBasis β 𝕜 X (SummationFilter.unconditional β)
Pinned sourceMathlib documentation ↗