Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Auerbach's lemma

Lax606786.AuerbachLemma · concepts/Lax606786/AuerbachLemma.lean · lax-606786

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let EE be a real normed space of finite dimension kk. Then there are unit vectors e1,…,ek∈Ee_1, \ldots, e_k \in E such that

    max⁡i∣ai∣≤∥∑iaiei∥for every a∈Rk.\max_i |a_i| \le \Bigl\| \sum_i a_i e_i \Bigr\| \quad \text{for every } a \in \mathbb{R}^k.

    Consequently, for every real normed space XX and every subspace W≤XW \le X of finite dimension mm, there is a bounded projection P:X→XP : X \to X onto WW with ∥P∥≤m\|P\| \le m. The first statement is Auerbach's lemma (see Wojtaszczyk 1991, II.E.11).

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 exists_auerbach_basis proven

    2 exists_proj_norm_le proven

    Lean source view on GitLab

    1import Mathlib.Analysis.Normed.Module.FiniteDimension
    2
    3/-!
    4---
    5title: Auerbach's lemma
    6type: theorem
    7---
    8Let EE be a real normed space of finite dimension kk. Then there are unit vectors
    9e1,…,ek∈Ee_1, \ldots, e_k \in E such that
    10max⁡i∣ai∣≤∥∑iaiei∥for every a∈Rk.\max_i |a_i| \le \Bigl\| \sum_i a_i e_i \Bigr\| \quad \text{for every } a \in \mathbb{R}^k.
    11Consequently, for every real normed space XX and every subspace W≤XW \le X of finite dimension
    12mm, there is a bounded projection P:X→XP : X \to X onto WW with ∥P∥≤m\|P\| \le m. The first statement
    13is Auerbach's lemma (see Wojtaszczyk 1991, II.E.11).
    14-/
    15
    16namespace Lax606786.AuerbachLemma
    17
    18/-- An Auerbach basis: unit vectors whose coefficients are controlled by the norm of the sum
    19(`‖a‖` is the supremum norm on `Fin k → ℝ`). -/
    20axiom exists_auerbach_basis {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    21 [FiniteDimensional ℝ E] {k : ℕ} (hk : Module.finrank ℝ E = k) :
    22 ∃ e : Fin k → E, (∀ i, ‖e i‖ = 1) ∧ ∀ a : Fin k → ℝ, ‖a‖ ≤ ‖∑ i, a i • e i‖
    23
    24/-- A projection of norm at most `m` onto an `m`-dimensional subspace. -/
    25axiom exists_proj_norm_le {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    26 (W : Submodule ℝ X) [FiniteDimensional ℝ W] {m : ℕ} (hm : Module.finrank ℝ W = m) :
    27 ∃ P : X →L[ℝ] X, (∀ x, P x ∈ W) ∧ (∀ w ∈ W, P w = w) ∧ ‖P‖ ≤ m
    28
    29end Lax606786.AuerbachLemma
    30
    Show ProofShow Proof
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…