Auerbach's Lemma

Every n-dimensional normed space over ℝ admits a basis {eᵢ} with ‖eᵢ‖ = 1 whose dual coordinate functionals also satisfy ‖eⁱ‖ = 1.

The proof maximizes |det| on the product of unit balls, then reads off the basis and dual functionals from the maximizer.

structure IsAuerbachBasis (V : Type u_2) [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ι : Type u_3} [Fintype ι] (b : Module.Basis ι ℝ V) : Prop

An Auerbach basis: all basis vectors and dual coordinate functionals have norm 1.

• norm_basis (i : ι) : ‖b i‖ = 1
• norm_coord (i : ι) : ‖LinearMap.toContinuousLinearMap (b.coord i)‖ = 1

noncomputable def coordFunOfDet {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} (b₀ : Module.Basis (Fin n) ℝ V) (e : Fin n → V) (_h_det : b₀.det e ≠ 0) (i : Fin n) : V →L[ℝ] ℝ

The i-th coordinate functional: v ↦ det(e₁,…,v,…,eₙ) / det(e).

Linearity is Mathlib's: fixing all but the i-th argument of the multilinear b₀.det gives a linear map (MultilinearMap.toLinearMap), which is then scaled by (det e)⁻¹ and continuous because V is finite-dimensional.

Equations

• coordFunOfDet b₀ e _h_det i = LinearMap.toContinuousLinearMap ((b₀.det e)⁻¹ • (↑b₀.det).toLinearMap e i)

theorem coordFunOfDet_apply_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} (b₀ : Module.Basis (Fin n) ℝ V) (e : Fin n → V) (h_det : b₀.det e ≠ 0) (i : Fin n) (v : V) : (coordFunOfDet b₀ e h_det i) v = b₀.det (Function.update e i v) / b₀.det e

The defining value of coordFunOfDet, in the div form of the definition.

theorem coordFunOfDet_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} (b₀ : Module.Basis (Fin n) ℝ V) (e : Fin n → V) (h_det : b₀.det e ≠ 0) (i j : Fin n) : (coordFunOfDet b₀ e h_det i) (e j) = if i = j then 1 else 0

theorem exists_isAuerbachBasis (V : Type u_2) [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] : ∃ (b : Module.Basis (Fin (Module.finrank ℝ V)) ℝ V), IsAuerbachBasis V b

Auerbach's Lemma. Every finite-dimensional normed space over ℝ admits an Auerbach basis. (For the zero space this is the empty basis, for which the norm conditions hold vacuously.)