Boundedness in normed groups

This file rephrases metric boundedness in terms of norms.

Tags

normed group

@[simp]

theorem comap_norm_atTop' {E : Type u_2} [SeminormedGroup E] : Filter.comap norm Filter.atTop = Bornology.cobounded E

@[simp]

theorem comap_norm_atTop {E : Type u_2} [SeminormedAddGroup E] : Filter.comap norm Filter.atTop = Bornology.cobounded E

theorem Filter.HasBasis.cobounded_of_norm' {E : Type u_2} [SeminormedGroup E] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set ℝ} (h : atTop.HasBasis p s) : (Bornology.cobounded E).HasBasis p fun (i : ι) => norm ⁻¹' s i

theorem Filter.HasBasis.cobounded_of_norm {E : Type u_2} [SeminormedAddGroup E] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set ℝ} (h : atTop.HasBasis p s) : (Bornology.cobounded E).HasBasis p fun (i : ι) => norm ⁻¹' s i

theorem Filter.hasBasis_cobounded_norm' {E : Type u_2} [SeminormedGroup E] : (Bornology.cobounded E).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => {x_1 : E | x ≤ ‖x_1‖}

theorem Filter.hasBasis_cobounded_norm {E : Type u_2} [SeminormedAddGroup E] : (Bornology.cobounded E).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => {x_1 : E | x ≤ ‖x_1‖}

@[simp]

theorem tendsto_norm_atTop_iff_cobounded' {α : Type u_1} {E : Type u_2} [SeminormedGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto (fun (x : α) => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)

@[simp]

theorem tendsto_norm_atTop_iff_cobounded {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto (fun (x : α) => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)

theorem tendsto_norm_cobounded_atTop' {E : Type u_2} [SeminormedGroup E] : Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop

theorem tendsto_norm_cobounded_atTop {E : Type u_2} [SeminormedAddGroup E] : Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop

theorem eventually_cobounded_le_norm' {E : Type u_2} [SeminormedGroup E] (a : ℝ) : ∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖

theorem eventually_cobounded_le_norm {E : Type u_2} [SeminormedAddGroup E] (a : ℝ) : ∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖

theorem tendsto_norm_cocompact_atTop' {E : Type u_2} [SeminormedGroup E] [ProperSpace E] : Filter.Tendsto norm (Filter.cocompact E) Filter.atTop

theorem tendsto_norm_cocompact_atTop {E : Type u_2} [SeminormedAddGroup E] [ProperSpace E] : Filter.Tendsto norm (Filter.cocompact E) Filter.atTop

@[simp]

theorem Filter.inv_cobounded {E : Type u_2} [SeminormedGroup E] : (Bornology.cobounded E)⁻¹ = Bornology.cobounded E

@[simp]

theorem Filter.neg_cobounded {E : Type u_2} [SeminormedAddGroup E] : -Bornology.cobounded E = Bornology.cobounded E

theorem Filter.tendsto_inv_cobounded {E : Type u_2} [SeminormedGroup E] : Tendsto Inv.inv (Bornology.cobounded E) (Bornology.cobounded E)

In a (semi)normed group, inversion x ↦ x⁻¹ tends to infinity at infinity.

theorem Filter.tendsto_neg_cobounded {E : Type u_2} [SeminormedAddGroup E] : Tendsto Neg.neg (Bornology.cobounded E) (Bornology.cobounded E)

In a (semi)normed group, negation x ↦ -x tends to infinity at infinity.

theorem isBounded_iff_forall_norm_le' {E : Type u_2} [SeminormedGroup E] {s : Set E} : Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

theorem isBounded_iff_forall_norm_le {E : Type u_2} [SeminormedAddGroup E] {s : Set E} : Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

theorem Bornology.IsBounded.exists_norm_le' {E : Type u_2} [SeminormedGroup E] {s : Set E} : IsBounded s → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

Alias of the forward direction of isBounded_iff_forall_norm_le'.

theorem Bornology.IsBounded.exists_norm_le {E : Type u_2} [SeminormedAddGroup E] {s : Set E} : IsBounded s → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

Alias of the forward direction of isBounded_iff_forall_norm_le.

theorem Bornology.IsBounded.exists_pos_norm_le' {E : Type u_2} [SeminormedGroup E] {s : Set E} (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R

theorem Bornology.IsBounded.exists_pos_norm_le {E : Type u_2} [SeminormedAddGroup E] {s : Set E} (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R

theorem Bornology.IsBounded.exists_pos_norm_lt' {E : Type u_2} [SeminormedGroup E] {s : Set E} (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R

theorem Bornology.IsBounded.exists_pos_norm_lt {E : Type u_2} [SeminormedAddGroup E] {s : Set E} (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R

theorem NormedCommGroup.cauchySeq_iff {α : Type u_1} {E : Type u_2} [SeminormedGroup E] [Nonempty α] [SemilatticeSup α] {u : α → E} : CauchySeq u ↔ ∀ ε > 0, ∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m / u n‖ < ε

theorem NormedAddCommGroup.cauchySeq_iff {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] [Nonempty α] [SemilatticeSup α] {u : α → E} : CauchySeq u ↔ ∀ ε > 0, ∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m - u n‖ < ε

theorem IsCompact.exists_bound_of_continuousOn' {α : Type u_1} {E : Type u_2} [SeminormedGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : α → E} (hf : ContinuousOn f s) : ∃ (C : ℝ), ∀ x ∈ s, ‖f x‖ ≤ C

theorem IsCompact.exists_bound_of_continuousOn {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : α → E} (hf : ContinuousOn f s) : ∃ (C : ℝ), ∀ x ∈ s, ‖f x‖ ≤ C

theorem HasCompactMulSupport.exists_bound_of_continuous {α : Type u_1} {E : Type u_2} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} (hf : HasCompactMulSupport f) (h'f : Continuous f) : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem HasCompactSupport.exists_bound_of_continuous {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} (hf : HasCompactSupport f) (h'f : Continuous f) : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem Filter.Tendsto.op_one_isBoundedUnder_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (nhds 1)) (hg : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (Norm.norm ∘ g)) (op : E → F → G) (h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) : Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_zero_isBoundedUnder_le' {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (nhds 0)) (hg : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (Norm.norm ∘ g)) (op : E → F → G) (h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) : Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_one_isBoundedUnder_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (nhds 1)) (hg : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (Norm.norm ∘ g)) (op : E → F → G) (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) : Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_zero_isBoundedUnder_le {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (nhds 0)) (hg : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (Norm.norm ∘ g)) (op : E → F → G) (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) : Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding' {E : Type u_2} [SeminormedGroup E] {X : Type u_5} [TopologicalSpace X] [DiscreteTopology X] [ProperSpace E] {e : X → E} (he : Topology.IsClosedEmbedding e) : Filter.Tendsto (norm ∘ e) Filter.cofinite Filter.atTop

theorem tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding {E : Type u_2} [SeminormedAddGroup E] {X : Type u_5} [TopologicalSpace X] [DiscreteTopology X] [ProperSpace E] {e : X → E} (he : Topology.IsClosedEmbedding e) : Filter.Tendsto (norm ∘ e) Filter.cofinite Filter.atTop

theorem Continuous.bounded_above_of_compact_support {α : Type u_1} {E : Type u_2} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} (hf : Continuous f) (h : HasCompactSupport f) : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem HasCompactMulSupport.exists_pos_le_norm {α : Type u_1} {E : Type u_2} [NormedAddGroup α] {f : α → E} [One E] (hf : HasCompactMulSupport f) : ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

theorem HasCompactSupport.exists_pos_le_norm {α : Type u_1} {E : Type u_2} [NormedAddGroup α] {f : α → E} [Zero E] (hf : HasCompactSupport f) : ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 0