Mathlib.Analysis.NormedSpace.Real

Real.punctured_nhds_module_neBot instance

 {E : Type*} [AddCommGroup E] [TopologicalSpace E] [ContinuousAdd E] [Nontrivial E] [Module ℝ E] [ContinuousSMul ℝ E]
  (x : E) : NeBot (𝓝[≠] x)

Full source

/-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points.
This is a particular case of `Module.punctured_nhds_neBot`. -/
instance Real.punctured_nhds_module_neBot {E : Type*} [AddCommGroup E] [TopologicalSpace E]
    [ContinuousAdd E] [Nontrivial E] [Module ℝ E] [ContinuousSMul ℝ E] (x : E) : NeBot (𝓝[≠] x) :=
  Module.punctured_nhds_neBot ℝ E x

Nontrivial Real Topological Vector Spaces Have No Isolated Points

Informal description

For any nontrivial topological vector space $E$ over $\mathbb{R}$ with continuous scalar multiplication, the punctured neighborhood of any point $x \in E$ is nonempty. In other words, $E$ has no isolated points.

inv_norm_smul_mem_unitClosedBall theorem

(x : E) : ‖x‖⁻¹ • x ∈ closedBall (0 : E) 1

Full source

theorem inv_norm_smul_mem_unitClosedBall (x : E) :
    ‖x‖‖x‖⁻¹‖x‖⁻¹ • x ∈ closedBall (0 : E) 1 := by
  simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul,
    div_self_le_one]

Normalized Vector Lies in Unit Closed Ball

Informal description

For any vector $x$ in a real seminormed space $E$, the vector $\|x\|^{-1} \cdot x$ lies in the closed unit ball centered at the origin, i.e., $\|x\|^{-1} \cdot x \in \overline{B}(0, 1)$.

norm_smul_of_nonneg theorem

{t : ℝ} (ht : 0 ≤ t) (x : E) : ‖t • x‖ = t * ‖x‖

Full source

theorem norm_smul_of_nonneg {t : ℝ} (ht : 0 ≤ t) (x : E) : ‖t • x‖ = t * ‖x‖ := by
  rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]

Norm Scaling Identity for Nonnegative Scalars

Informal description

For any nonnegative real number $t \geq 0$ and any vector $x$ in a real seminormed space $E$, the norm of the scalar multiple $t \cdot x$ satisfies $\|t \cdot x\| = t \cdot \|x\|$.

dist_smul_add_one_sub_smul_le theorem

{r : ℝ} {x y : E} (h : r ∈ Icc 0 1) : dist (r • x + (1 - r) • y) x ≤ dist y x

Full source

theorem dist_smul_add_one_sub_smul_le {r : ℝ} {x y : E} (h : r ∈ Icc 0 1) :
    dist (r • x + (1 - r) • y) x ≤ dist y x :=
  calc
    dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖ := by
      simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
    _ = (1 - r) * dist y x := by
      rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']
    _ ≤ (1 - 0) * dist y x := by gcongr; exact h.1
    _ = dist y x := by rw [sub_zero, one_mul]

Distance Bound for Convex Combination in Seminormed Space

Informal description

For any real number $r \in [0, 1]$ and any vectors $x, y$ in a real seminormed space $E$, the distance between the convex combination $r \cdot x + (1 - r) \cdot y$ and $x$ is bounded by the distance between $y$ and $x$, i.e., \[ \text{dist}(r x + (1 - r) y, x) \leq \text{dist}(y, x). \]

closure_ball theorem

(x : E) {r : ℝ} (hr : r ≠ 0) : closure (ball x r) = closedBall x r

Full source

theorem closure_ball (x : E) {r : ℝ} (hr : r ≠ 0) : closure (ball x r) = closedBall x r := by
  refine Subset.antisymm closure_ball_subset_closedBall fun y hy => ?_
  have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 :=
    ((continuous_id.smul continuous_const).add continuous_const).continuousWithinAt
  convert this.mem_closure _ _
  · rw [one_smul, sub_add_cancel]
  · simp [closure_Ico zero_ne_one, zero_le_one]
  · rintro c ⟨hc0, hc1⟩
    rw [mem_ball, dist_eq_norm, add_sub_cancel_right, norm_smul, Real.norm_eq_abs,
      abs_of_nonneg hc0, mul_comm, ← mul_one r]
    rw [mem_closedBall, dist_eq_norm] at hy
    replace hr : 0 < r := ((norm_nonneg _).trans hy).lt_of_ne hr.symm
    apply mul_lt_mul' <;> assumption

Closure of Open Ball Equals Closed Ball in Seminormed Space

Informal description

For any point $x$ in a real seminormed space $E$ and any nonzero radius $r \neq 0$, the closure of the open ball $\text{ball}(x, r)$ is equal to the closed ball $\text{closedBall}(x, r)$.

frontier_ball theorem

(x : E) {r : ℝ} (hr : r ≠ 0) : frontier (ball x r) = sphere x r

Full source

theorem frontier_ball (x : E) {r : ℝ} (hr : r ≠ 0) :
    frontier (ball x r) = sphere x r := by
  rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]

Frontier of Open Ball Equals Sphere in Seminormed Space

Informal description

For any point $x$ in a real seminormed space $E$ and any nonzero radius $r \neq 0$, the frontier of the open ball $\text{ball}(x, r)$ is equal to the sphere $\text{sphere}(x, r)$.

interior_closedBall theorem

(x : E) {r : ℝ} (hr : r ≠ 0) : interior (closedBall x r) = ball x r

Full source

theorem interior_closedBall (x : E) {r : ℝ} (hr : r ≠ 0) :
    interior (closedBall x r) = ball x r := by
  rcases hr.lt_or_lt with hr | hr
  · rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]
  refine Subset.antisymm ?_ ball_subset_interior_closedBall
  intro y hy
  rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)
  · exact hr
  set f : ℝ → E := fun c : ℝ => c • (y - x) + x
  suffices f ⁻¹' closedBall x (dist y x)f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1 by
    have hfc : Continuous f := (continuous_id.smul continuous_const).add continuous_const
    have hf1 : (1 : ℝ) ∈ f ⁻¹' interior (closedBall x <| dist y x) := by simpa [f]
    have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage hfc hf1)
    simp at h1
  intro c hc
  rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_right hr]
  simpa [f, dist_eq_norm, norm_smul] using hc

Interior of Closed Ball Equals Open Ball in Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any nonzero radius $r \in \mathbb{R}$ ($r \neq 0$), the interior of the closed ball $\overline{B}(x, r)$ is equal to the open ball $B(x, r)$.

frontier_closedBall theorem

(x : E) {r : ℝ} (hr : r ≠ 0) : frontier (closedBall x r) = sphere x r

Full source

theorem frontier_closedBall (x : E) {r : ℝ} (hr : r ≠ 0) :
    frontier (closedBall x r) = sphere x r := by
  rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]

Frontier of Closed Ball Equals Sphere in Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any nonzero radius $r \in \mathbb{R}$ ($r \neq 0$), the frontier of the closed ball $\overline{B}(x, r)$ is equal to the sphere $S(x, r)$.

interior_sphere theorem

(x : E) {r : ℝ} (hr : r ≠ 0) : interior (sphere x r) = ∅

Full source

theorem interior_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : interior (sphere x r) = ∅ := by
  rw [← frontier_closedBall x hr, interior_frontier isClosed_closedBall]

Interior of Sphere is Empty in Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any nonzero radius $r \in \mathbb{R}$ ($r \neq 0$), the interior of the sphere $S(x, r)$ is the empty set, i.e., $\text{interior}(S(x, r)) = \emptyset$.

frontier_sphere theorem

(x : E) {r : ℝ} (hr : r ≠ 0) : frontier (sphere x r) = sphere x r

Full source

theorem frontier_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (sphere x r) = sphere x r := by
  rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]

Frontier of Sphere Equals Itself in Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any nonzero radius $r \in \mathbb{R}$ ($r \neq 0$), the frontier of the sphere $S(x, r)$ is equal to the sphere itself, i.e., $\text{frontier}(S(x, r)) = S(x, r)$.

exists_norm_eq theorem

{c : ℝ} (hc : 0 ≤ c) : ∃ x : E, ‖x‖ = c

Full source

theorem exists_norm_eq {c : ℝ} (hc : 0 ≤ c) : ∃ x : E, ‖x‖ = c := by
  rcases exists_ne (0 : E) with ⟨x, hx⟩
  rw [← norm_ne_zero_iff] at hx
  use c • ‖x‖⁻¹ • x
  simp [norm_smul, Real.norm_of_nonneg hc, abs_of_nonneg hc, inv_mul_cancel₀ hx]

Existence of Element with Given Norm in Seminormed Space

Informal description

For any real number $c \geq 0$, there exists an element $x$ in a real seminormed space $E$ such that its norm equals $c$, i.e., $\|x\| = c$.

range_norm theorem

: range (norm : E → ℝ) = Ici 0

Full source

@[simp]
theorem range_norm : range (norm : E → ℝ) = Ici 0 :=
  Subset.antisymm (range_subset_iff.2 norm_nonneg) fun _ => exists_norm_eq E

Range of Norm Function Equals Non-Negative Reals

Informal description

The range of the norm function $\|\cdot\| : E \to \mathbb{R}$ on a real seminormed space $E$ is equal to the set of non-negative real numbers $[0, \infty)$. That is, $\text{range}(\|\cdot\|) = [0, \infty)$.

nnnorm_surjective theorem

: Surjective (nnnorm : E → ℝ≥0)

Full source

theorem nnnorm_surjective : Surjective (nnnorm : E → ℝ≥0) := fun c =>
  (exists_norm_eq E c.coe_nonneg).imp fun _ h => NNReal.eq h

Surjectivity of Nonnegative Norm Function on Seminormed Spaces

Informal description

The nonnegative real norm function $\|\cdot\| : E \to \mathbb{R}_{\geq 0}$ on a real seminormed space $E$ is surjective. That is, for every nonnegative real number $y \in \mathbb{R}_{\geq 0}$, there exists an element $x \in E$ such that $\|x\| = y$.

range_nnnorm theorem

: range (nnnorm : E → ℝ≥0) = univ

Full source

@[simp]
theorem range_nnnorm : range (nnnorm : E → ℝ≥0) = univ :=
  (nnnorm_surjective E).range_eq

Surjectivity of Nonnegative Norm Function onto Nonnegative Reals

Informal description

The range of the nonnegative norm function $\|\cdot\| : E \to \mathbb{R}_{\geq 0}$ on a real seminormed space $E$ is equal to the entire set of nonnegative real numbers $\mathbb{R}_{\geq 0}$. That is, for every $y \in \mathbb{R}_{\geq 0}$, there exists an $x \in E$ such that $\|x\| = y$.

interior_closedBall' theorem

(x : E) (r : ℝ) : interior (closedBall x r) = ball x r

Full source

theorem interior_closedBall' (x : E) (r : ℝ) : interior (closedBall x r) = ball x r := by
  rcases eq_or_ne r 0 with (rfl | hr)
  · rw [closedBall_zero, ball_zero, interior_singleton]
  · exact interior_closedBall x hr

Interior of Closed Ball Equals Open Ball in Real Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any radius $r \in \mathbb{R}$, the interior of the closed ball $\overline{B}(x, r)$ is equal to the open ball $B(x, r)$.

frontier_closedBall' theorem

(x : E) (r : ℝ) : frontier (closedBall x r) = sphere x r

Full source

theorem frontier_closedBall' (x : E) (r : ℝ) : frontier (closedBall x r) = sphere x r := by
  rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]

Frontier of Closed Ball Equals Sphere in Real Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any radius $r \in \mathbb{R}$, the frontier of the closed ball $\overline{B}(x, r)$ is equal to the sphere $S(x, r)$.

interior_sphere' theorem

(x : E) (r : ℝ) : interior (sphere x r) = ∅

Full source

@[simp]
theorem interior_sphere' (x : E) (r : ℝ) : interior (sphere x r) = ∅ := by
  rw [← frontier_closedBall' x, interior_frontier isClosed_closedBall]

Empty Interior of Sphere in Real Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any radius $r \in \mathbb{R}$, the interior of the sphere $S(x, r)$ is empty, i.e., $\text{interior}(S(x, r)) = \emptyset$.

frontier_sphere' theorem

(x : E) (r : ℝ) : frontier (sphere x r) = sphere x r

Full source

@[simp]
theorem frontier_sphere' (x : E) (r : ℝ) : frontier (sphere x r) = sphere x r := by
  rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]

Frontier of Sphere Equals Itself in Real Seminormed Spaces

Informal description

For any point $x$ in a real seminormed space $E$ and any radius $r \in \mathbb{R}$, the frontier of the sphere $S(x, r)$ is equal to the sphere itself, i.e., $\text{frontier}(S(x, r)) = S(x, r)$.

Main results