Unit vectors far from a subspace of smaller dimension

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

proven

Loading review…

Let $X$ be a real normed space and $A, W \le X$ finite-dimensional subspaces with $\dim W < \dim A$ . Then there is a unit vector $u \in A$ with

d(u, W) \ge \frac{1}{1 + \dim W}.

Concept map

1 concept

100%

Proven claimThis concept

Evidence

Each proof establishes this claim relative to its assumptions.

Show types on hover

1	import Mathlib.Analysis.Normed.Module.FiniteDimension
2
3	/-!
4	---
5	title: Unit vectors far from a subspace of smaller dimension
6	type: theorem
7	---
8	Let $X$ be a real normed space and $A, W \le X$ finite-dimensional subspaces with
9	$\dim W < \dim A$ . Then there is a unit vector $u \in A$ with
10	$d(u, W) \ge \frac{1}{1 + \dim W}.$
11	-/
12
13	namespace Lax606786.FarUnitVectors
14
15	/-- A unit vector of `A` at distance at least `1 / (1 + dim W)` from `W`. -/
16	axiom exists_unit_far_of_finrank_lt {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
17	{A W : Submodule ℝ X} [FiniteDimensional ℝ A] [FiniteDimensional ℝ W]
18	(h : Module.finrank ℝ W < Module.finrank ℝ A) :
19	∃ u ∈ A, ‖u‖ = 1 ∧ (1 : ℝ) / (1 + Module.finrank ℝ W) ≤ Metric.infDist u (W : Set X)
20
21	end Lax606786.FarUnitVectors
22

Builds on

none

Used by

none

From Mathlib

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

Loading discussion…

Lax Lean Archive