Strict half-spaces of a real normed space are unbounded

A strict half-space {y | φ y < u} cut out by a nonzero linear functional holds points of arbitrarily large norm, and is therefore unbounded. Linearity alone suffices: φ need not be continuous, so the results apply to a discontinuous functional on an infinite-dimensional space. For such a φ the set need not be topologically open, which is why it is called strict rather than open here.

Main results

• TauCeti.exists_apply_lt_and_lt_norm and TauCeti.exists_lt_apply_and_lt_norm — either side of a nonzero linear functional holds points of arbitrarily large norm.
• TauCeti.not_isBounded_halfSpace_lt and TauCeti.not_isBounded_halfSpace_gt — either strict half-space is unbounded.

theorem TauCeti.exists_apply_lt_and_lt_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : E →ₗ[ℝ] ℝ} (hφ : φ ≠ 0) (u R : ℝ) : ∃ (y : E), φ y < u ∧ R < ‖y‖

A strict half-space contains points of arbitrarily large norm. For a nonzero linear functional φ, every bound u and every radius R admit a y with φ y < u and R < ‖y‖. Linearity suffices; φ need not be continuous.

theorem TauCeti.exists_lt_apply_and_lt_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : E →ₗ[ℝ] ℝ} (hφ : φ ≠ 0) (u R : ℝ) : ∃ (y : E), u < φ y ∧ R < ‖y‖

The other side of a nonzero linear functional also contains points of arbitrarily large norm: every bound u and radius R admit a y with u < φ y and R < ‖y‖.

theorem TauCeti.not_isBounded_halfSpace_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : E →ₗ[ℝ] ℝ} (hφ : φ ≠ 0) (u : ℝ) : ¬Bornology.IsBounded {y : E | φ y < u}

A strict half-space cut out by a nonzero linear functional is unbounded. No radius bounds {y | φ y < u}. Linearity suffices; φ need not be continuous.

theorem TauCeti.not_isBounded_halfSpace_gt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : E →ₗ[ℝ] ℝ} (hφ : φ ≠ 0) (u : ℝ) : ¬Bornology.IsBounded {y : E | u < φ y}

The half-space on the other side of a nonzero linear functional is unbounded. No radius bounds {y | u < φ y} either. Linearity suffices; φ need not be continuous.