The norm as a seminorm

In this file, we define the norm of a normed space as a bundled seminorm.

def normSeminorm (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Seminorm 𝕜 E

The norm of a seminormed space as a seminorm.

Equations

• normSeminorm 𝕜 E = { toAddGroupSeminorm := normAddGroupSeminorm E, smul' := ⋯ }

@[simp]

theorem coe_normSeminorm (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : ⇑(normSeminorm 𝕜 E) = norm

@[simp]

theorem ball_normSeminorm (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : (normSeminorm 𝕜 E).ball = Metric.ball

@[simp]

theorem closedBall_normSeminorm (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : (normSeminorm 𝕜 E).closedBall = Metric.closedBall

theorem absorbent_ball_zero {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : Absorbent 𝕜 (Metric.ball 0 r)

Balls at the origin are absorbent.

theorem absorbent_ball {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} {x : E} (hx : ‖x‖ < r) : Absorbent 𝕜 (Metric.ball x r)

Balls containing the origin are absorbent.

theorem balanced_ball_zero {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : Balanced 𝕜 (Metric.ball 0 r)

Balls at the origin are balanced.

theorem balanced_closedBall_zero {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : Balanced 𝕜 (Metric.closedBall 0 r)

Closed balls at the origin are balanced.

theorem rescale_to_shell_semi_normed_zpow {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {c : 𝕜} {ε : ℝ} (hc : 1 < ‖c‖) (εpos : 0 < ε) (hx : ‖x‖ ≠ 0) : ∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

If there is a scalar c with ‖c‖ > 1, then any element with nonzero norm can be moved by scalar multiplication to any shell of width ‖c‖. Also recap information on the norm of the rescaling element that shows up in applications.

theorem rescale_to_shell_semi_normed {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {c : 𝕜} {ε : ℝ} (hc : 1 < ‖c‖) (εpos : 0 < ε) (hx : ‖x‖ ≠ 0) : ∃ (d : 𝕜), d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

If there is a scalar c with ‖c‖ > 1, then any element with nonzero norm can be moved by scalar multiplication to any shell of width ‖c‖. Also recap information on the norm of the rescaling element that shows up in applications.

theorem rescale_to_shell_zpow {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {c : 𝕜} {ε : ℝ} (hc : 1 < ‖c‖) (εpos : 0 < ε) (hx : x ≠ 0) : ∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

theorem rescale_to_shell {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {c : 𝕜} {ε : ℝ} (hc : 1 < ‖c‖) (εpos : 0 < ε) (hx : x ≠ 0) : ∃ (d : 𝕜), d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

If there is a scalar c with ‖c‖ > 1, then any element can be moved by scalar multiplication to any shell of width ‖c‖. Also recap information on the norm of the rescaling element that shows up in applications.