Auerbach bases

DefinitionCoordinate functional of a basis as a continuous linear map#✓fully proved

The i-th coordinate functional of a basis, as a continuous linear map. In finite dimensions every linear map is continuous, so this is just the coordinate functional bundled with its continuity.

noncomputable def coordCLM {ι : Type*} [FiniteDimensional 𝕜 E] (b : Module.Basis ι 𝕜 E) (i : ι) :
    E →L[𝕜] 𝕜 :=
  ⟨b.coord i, (b.coord i).continuous_of_finiteDimensional⟩

Used by 4

Used byAuerbach's theorem · Auerbach basis · Coordinate functional of a unit basis vector has operator norm 1 · Operator norm of a norm-bounded coordinate functional is at most 1

TheoremOperator norm of a norm-bounded coordinate functional is at most 1#✓fully proved

If the i-th coordinate functional is bounded by the norm, its operator norm is at most 1.

theorem norm_coordCLM_le_one {ι : Type*} [FiniteDimensional 𝕜 E] (b : Module.Basis ι 𝕜 E) (i : ι)
    (h : ∀ y : E, ‖b.coord i y‖ ≤ ‖y‖) : ‖coordCLM b i‖ ≤ 1

Uses 1 · Used by 1

Statement usesCoordinate functional of a basis as a continuous linear map

Used byCoordinate functional of a unit basis vector has operator norm 1

TheoremCoordinate functional of a unit basis vector has operator norm 1#✓fully proved

If the i-th basis vector has norm 1 and the i-th coordinate functional is bounded by the norm, its operator norm is exactly 1: it attains 1 at the i-th basis vector.

theorem norm_coordCLM_eq_one {ι : Type*} [FiniteDimensional 𝕜 E] (b : Module.Basis ι 𝕜 E) (i : ι)
    (hb : ‖b i‖ = 1) (h : ∀ y : E, ‖b.coord i y‖ ≤ ‖y‖) : ‖coordCLM b i‖ = 1

Uses 2 · Used by 1

Statement usesCoordinate functional of a basis as a continuous linear map

Proof usesOperator norm of a norm-bounded coordinate functional is at most 1

Used byAuerbach's theorem

DefinitionAuerbach basis#✓fully proved

An Auerbach basis is a basis of unit vectors whose coordinate functionals all have operator norm 1.

def IsAuerbachBasis {ι : Type*} [FiniteDimensional 𝕜 E] (b : Module.Basis ι 𝕜 E) : Prop :=
  (∀ i, ‖b i‖ = 1) ∧ ∀ i, ‖coordCLM b i‖ = 1

Uses 1 · Used by 1

Statement usesCoordinate functional of a basis as a continuous linear map

Used byAuerbach's theorem

TheoremAuerbach's theorem#✓fully proved

Every finite-dimensional normed space over 𝕜 has an Auerbach basis, indexed by Fin (Module.finrank 𝕜 E).

theorem exists_auerbach_basis [FiniteDimensional 𝕜 E] :
    ∃ b : Module.Basis (Fin (Module.finrank 𝕜 E)) 𝕜 E, IsAuerbachBasis b

Uses 3

Statement usesAuerbach basis

Proof usesCoordinate functional of a basis as a continuous linear map · Coordinate functional of a unit basis vector has operator norm 1

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.