Birkhoff–James orthogonality

12 fully proved

Birkhoff–James orthogonality

DefinitionBirkhoff–James orthogonality#✓fully proved

x is Birkhoff–James orthogonal to y if x is a shortest vector on the affine line x + 𝕜 • y.

def BirkhoffJamesOrthogonal (𝕜 : Type*) [RCLike 𝕜] {E : Type*} [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] (x y : E) : Prop :=
  ∀ c : 𝕜, ‖x‖ ≤ ‖x + c • y‖

Used by 9

Used byDuality-mapping characterization of Birkhoff–James orthogonality · Norming-functional characterization of Birkhoff–James orthogonality · Birkhoff–James orthogonality in inner product spaces · Annihilating norming functional implies Birkhoff–James orthogonality · Only zero is Birkhoff–James orthogonal to itself · Homogeneity of Birkhoff–James orthogonality · Zero is Birkhoff–James orthogonal to every vector · Every vector is Birkhoff–James orthogonal to zero · Birkhoff–James orthogonality gives an annihilating norming functional

TheoremZero is Birkhoff–James orthogonal to every vector#✓fully proved

0 is Birkhoff–James orthogonal to every vector.

theorem birkhoffJamesOrthogonal_zero_left (y : E) :
    BirkhoffJamesOrthogonal 𝕜 (0 : E) y

Uses 1 · Used by 1

Statement usesBirkhoff–James orthogonality

Used byOnly zero is Birkhoff–James orthogonal to itself

TheoremEvery vector is Birkhoff–James orthogonal to zero#✓fully proved

Every vector is Birkhoff–James orthogonal to 0.

theorem birkhoffJamesOrthogonal_zero_right (x : E) :
    BirkhoffJamesOrthogonal 𝕜 x 0

Uses 1

Statement usesBirkhoff–James orthogonality

TheoremOnly zero is Birkhoff–James orthogonal to itself#✓fully proved

A vector is Birkhoff–James orthogonal to itself if and only if it is 0.

theorem birkhoffJamesOrthogonal_self_iff {x : E} :
    BirkhoffJamesOrthogonal 𝕜 x x ↔ x = 0

Uses 2

Statement usesBirkhoff–James orthogonality

Proof usesZero is Birkhoff–James orthogonal to every vector

TheoremHomogeneity of Birkhoff–James orthogonality#✓fully proved

Birkhoff–James orthogonality is homogeneous in both arguments.

theorem birkhoffJamesOrthogonal_smul_left_right {x y : E} {a b : 𝕜}
    (h : BirkhoffJamesOrthogonal 𝕜 x y) :
    BirkhoffJamesOrthogonal 𝕜 (a • x) (b • y)

Uses 1 · Used by 1

Statement usesBirkhoff–James orthogonality

Used byBirkhoff–James orthogonality in inner product spaces

TheoremAnnihilating norming functional implies Birkhoff–James orthogonality#✓fully proved

If a norming functional of x vanishes at y, then x is Birkhoff–James orthogonal to y.

theorem birkhoffJamesOrthogonal_of_exists_norming {x y : E} {f : E →L[𝕜] 𝕜}
    (hf : ‖f‖ = 1) (hfx : f x = ‖x‖) (hfy : f y = 0) :
    BirkhoffJamesOrthogonal 𝕜 x y

Uses 1 · Used by 1

Statement usesBirkhoff–James orthogonality

Used byNorming-functional characterization of Birkhoff–James orthogonality

TheoremBirkhoff–James orthogonality gives an annihilating norming functional#✓fully proved

The converse: if x ≠ 0 is Birkhoff–James orthogonal to y, there is a norming functional of x vanishing at y. Birkhoff–James orthogonality makes the distance from x to 𝕜 ∙ y equal to ‖x‖, so the dual distance formula supplies an annihilating norming functional.

theorem exists_norming_of_birkhoffJamesOrthogonal {x y : E} (hx : x ≠ 0)
    (h : BirkhoffJamesOrthogonal 𝕜 x y) :
    ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ ∧ f y = 0

Uses 2 · Used by 2

Statement usesBirkhoff–James orthogonality

Proof usesNorm-one annihilating functional at positive distance

Used byDuality-mapping characterization of Birkhoff–James orthogonality · Norming-functional characterization of Birkhoff–James orthogonality

TheoremNorming-functional characterization of Birkhoff–James orthogonality#✓fully proved

For x ≠ 0, Birkhoff–James orthogonality to y is equivalent to the existence of a norming functional of x vanishing at y.

theorem birkhoffJamesOrthogonal_iff_exists_norming {x y : E} (hx : x ≠ 0) :
    BirkhoffJamesOrthogonal 𝕜 x y ↔
      ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ ∧ f y = 0

Uses 3

Statement usesBirkhoff–James orthogonality

Proof usesAnnihilating norming functional implies Birkhoff–James orthogonality · Birkhoff–James orthogonality gives an annihilating norming functional

DefinitionDuality mapping of a normed space#✓fully proved

The duality mapping (duality set) at x: the functionals f with f x = ‖x‖ ^ 2 and ‖f‖ = ‖x‖. At x = 0 this is the singleton {0}.

def dualityMapping (𝕜 : Type*) [RCLike 𝕜] {E : Type*} [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] (x : E) : Set (E →L[𝕜] 𝕜) :=
  {f | f x = ((‖x‖ ^ 2 : ℝ) : 𝕜) ∧ ‖f‖ = ‖x‖}

Used by 2

Used byDuality-mapping characterization of Birkhoff–James orthogonality · Duality mapping is nonempty

TheoremDuality mapping is nonempty#✓fully proved

The duality mapping is nonempty at every point: take a Hahn–Banach norming functional and scale it by ‖x‖.

theorem dualityMapping_nonempty (x : E) : (dualityMapping 𝕜 x).Nonempty

Uses 1

Statement usesDuality mapping of a normed space

TheoremDuality-mapping characterization of Birkhoff–James orthogonality#✓fully proved

Birkhoff–James orthogonality to y is equivalent to the existence of a functional in the duality mapping at x that vanishes at y.

theorem birkhoffJamesOrthogonal_iff_exists_dualityMapping {x y : E} :
    BirkhoffJamesOrthogonal 𝕜 x y ↔ ∃ f ∈ dualityMapping 𝕜 x, f y = 0

Uses 3

Statement usesBirkhoff–James orthogonality · Duality mapping of a normed space

Proof usesBirkhoff–James orthogonality gives an annihilating norming functional

Inner Product

TheoremBirkhoff–James orthogonality in inner product spaces#✓fully proved

In an inner product space, Birkhoff–James orthogonality is ordinary inner-product orthogonality.

theorem birkhoffJamesOrthogonal_iff_inner_eq_zero {x y : E} :
    BirkhoffJamesOrthogonal 𝕜 x y ↔ ⟪x, y⟫ = 0

Uses 2

Statement usesBirkhoff–James orthogonality

Proof usesHomogeneity of Birkhoff–James orthogonality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.