Basic facts about seminormed groups

In a seminormed additive group, the squared distance between two points is at most twice the sum of their squared distances to any third point: the triangle inequality through c, squared with (x + y) ^ 2 ≤ 2 (x ^ 2 + y ^ 2). The reciprocal transform (1 + ‖x - a‖²)⁻¹ of a squared distance is at most 1.

An unbounded set stays unbounded after removing a closed ball, since a closed ball is bounded.

A bound on the norms of a set with two distinct points is positive, since one of the points is nonzero.

A continuous function on ℝ with limits at ±∞ is bounded.

A map bounded by M on a set sends it into the closed ball of radius 2 * M around any of its values there.

Near 0, the product ‖x‖ * R is eventually less than any positive bound.

A sum z + a with ‖a‖ < ‖z‖ is nonzero.

A constant bound on ‖f x‖ over a ball of positive radius is nonnegative, since the ball contains 0.

Main declarations

• TauCeti.norm_sub_sq_le_two_mul -- the squared triangle inequality through an intermediate point.
• TauCeti.inv_one_add_norm_sub_sq_le_one -- the reciprocal transform of a squared distance is at most 1.
• TauCeti.not_isBounded_inter_lt_norm_sub -- the part of an unbounded set outside a closed ball is unbounded.
• Set.Nontrivial.pos_of_forall_norm_le -- a bound on the norms of a nontrivial set is positive.
• TauCeti.exists_forall_norm_le_of_tendsto -- a continuous function ℝ → F with limits at ±∞ is bounded.
• TauCeti.exists_enorm_sub_le_mul_of_reflTransGen -- constants joined by a chain of related indices are uniformly close if constants at related indices are.
• TauCeti.mapsTo_closedBall_of_forall_norm_le -- a map bounded by M on s sends s into the closed ball of radius 2 * M around any of its values on s.
• TauCeti.eventually_norm_mul_lt -- eventually near 0, ‖x‖ * R < ρ for any ρ > 0.
• TauCeti.add_ne_zero_of_norm_lt -- z + a ≠ 0 when ‖a‖ < ‖z‖.
• TauCeti.nonneg_of_forall_norm_lt -- a constant bound on ‖f x‖ over a ball of positive radius is nonnegative.

theorem TauCeti.norm_sub_sq_le_two_mul {E : Type u_1} [SeminormedAddCommGroup E] (a b c : E) : ‖a - b‖ ^ 2 ≤ 2 * (‖a - c‖ ^ 2 + ‖b - c‖ ^ 2)

Squared triangle inequality. The squared distance from a to b is at most twice the sum of the squared distances from a and from b to an intermediate point c.

theorem TauCeti.inv_one_add_norm_sub_sq_le_one {E : Type u_1} [SeminormedAddCommGroup E] (x a : E) : (1 + ‖x - a‖ ^ 2)⁻¹ ≤ 1

The reciprocal transform (1 + ‖x - a‖²)⁻¹ of the squared distance is at most 1.

theorem TauCeti.not_isBounded_inter_lt_norm_sub {E : Type u_1} [SeminormedAddCommGroup E] {s : Set E} (hs : ¬Bornology.IsBounded s) (c : E) (ρ : ℝ) : ¬Bornology.IsBounded (s ∩ {w : E | ρ < ‖w - c‖})

An unbounded set stays unbounded after removing a closed ball: its far part s ∩ {w | ρ < ‖w - c‖} is unbounded.

theorem Set.Nontrivial.pos_of_forall_norm_le {E : Type u_1} [NormedAddGroup E] {s : Set E} (hs : s.Nontrivial) {r : ℝ} (hr : ∀ x ∈ s, ‖x‖ ≤ r) : 0 < r

In a normed group, a bound on the norms of a set with two distinct points is positive.

theorem TauCeti.mapsTo_closedBall_of_forall_norm_le {α : Type u_1} {F : Type u_2} [SeminormedAddCommGroup F] {f : α → F} {s : Set α} {c : α} {M : ℝ} (hM : ∀ y ∈ s, ‖f y‖ ≤ M) (hc : c ∈ s) : Set.MapsTo f s (Metric.closedBall (f c) (2 * M))

A map bounded by M on a set s sends s into the closed ball of radius 2 * M around its value at any point c ∈ s.

theorem TauCeti.eventually_norm_mul_lt {E : Type u_1} [SeminormedAddGroup E] (R : ℝ) {ρ : ℝ} (hρ : 0 < ρ) : ∀ᶠ (x : E) in nhds 0, ‖x‖ * R < ρ

Eventually near 0, the norm of x times a fixed real R is less than any ρ > 0.

theorem TauCeti.add_ne_zero_of_norm_lt {E : Type u_1} [SeminormedAddGroup E] {a z : E} (h : ‖a‖ < ‖z‖) : z + a ≠ 0

A sum z + a with ‖a‖ < ‖z‖ is nonzero.

theorem TauCeti.exists_forall_norm_le_of_tendsto {F : Type u_1} [SeminormedAddCommGroup F] {A : ℝ → F} {Aminus Aplus : F} (hA : Continuous A) (hbot : Filter.Tendsto A Filter.atBot (nhds Aminus)) (htop : Filter.Tendsto A Filter.atTop (nhds Aplus)) : ∃ (M : ℝ), ∀ (s : ℝ), ‖A s‖ ≤ M

A continuous function ℝ → F into a seminormed group with limits at ±∞ is bounded.

theorem TauCeti.exists_enorm_sub_le_mul_of_reflTransGen {κ : Type u_1} {F : Type u_2} {ι : Type u_3} [SeminormedAddGroup F] {R : ι → ι → Prop} {i₀ : ι} {a : κ → ι → F} {G : κ → ENNReal} (hadj : ∀ (i j : ι), R i j → ∃ (D : NNReal), ∀ (k : κ), ‖a k j - a k i‖ₑ ≤ ↑D * G k) {j : ι} (hj : Relation.ReflTransGen R i₀ j) : ∃ (D : NNReal), ∀ (k : κ), ‖a k j - a k i₀‖ₑ ≤ ↑D * G k

Families of vectors joined by a chain of related indices are uniformly close, if the vectors at related indices are: if ‖a k j - a k i‖ ≤ D * G k for related i j and all k, then the same holds, with a constant D' independent of k, for any j reachable from i₀.

theorem TauCeti.nonneg_of_forall_norm_lt {E : Type u_1} {F : Type u_2} {𝓕 : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] (f : 𝓕) {δ B : ℝ} (hδ : 0 < δ) (hf : ∀ (x : E), ‖x‖ < δ → ‖f x‖ ≤ B) : 0 ≤ B

A constant bound on ‖f x‖ over a ball of positive radius is nonnegative, since the ball contains 0.