Documentation

Mathlib.Analysis.Normed.Group.Bounded

Boundedness in normed groups #

This file rephrases metric boundedness in terms of norms.

Tags #

normed group

@[simp]
theorem comap_norm_atTop {E : Type u_3} [SeminormedAddGroup E] :
Filter.comap norm Filter.atTop = Bornology.cobounded E
@[simp]
theorem comap_norm_atTop' {E : Type u_3} [SeminormedGroup E] :
Filter.comap norm Filter.atTop = Bornology.cobounded E
theorem Filter.HasBasis.cobounded_of_norm {E : Type u_3} [SeminormedAddGroup E] {ι : Sort u_6} {p : ιProp} {s : ιSet } (h : Filter.atTop.HasBasis p s) :
(Bornology.cobounded E).HasBasis p fun (i : ι) => norm ⁻¹' s i
theorem Filter.HasBasis.cobounded_of_norm' {E : Type u_3} [SeminormedGroup E] {ι : Sort u_6} {p : ιProp} {s : ιSet } (h : Filter.atTop.HasBasis p s) :
(Bornology.cobounded E).HasBasis p fun (i : ι) => norm ⁻¹' s i
theorem Filter.hasBasis_cobounded_norm {E : Type u_3} [SeminormedAddGroup E] :
(Bornology.cobounded E).HasBasis (fun (x : ) => True) fun (x : ) => {x_1 : E | x x_1}
theorem Filter.hasBasis_cobounded_norm' {E : Type u_3} [SeminormedGroup 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_3} [SeminormedAddGroup 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_3} [SeminormedGroup E] {f : αE} {l : Filter α} :
Filter.Tendsto (fun (x : α) => f x) l Filter.atTop Filter.Tendsto f l (Bornology.cobounded E)
theorem eventually_cobounded_le_norm {E : Type u_3} [SeminormedAddGroup E] (a : ) :
∀ᶠ (x : E) in Bornology.cobounded E, a x
theorem eventually_cobounded_le_norm' {E : Type u_3} [SeminormedGroup E] (a : ) :
∀ᶠ (x : E) in Bornology.cobounded E, a x

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

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

theorem isBounded_iff_forall_norm_le {E : Type u_3} [SeminormedAddGroup E] {s : Set E} :
Bornology.IsBounded s ∃ (C : ), xs, x C
theorem isBounded_iff_forall_norm_le' {E : Type u_3} [SeminormedGroup E] {s : Set E} :
Bornology.IsBounded s ∃ (C : ), xs, x C
theorem Bornology.IsBounded.exists_norm_le' {E : Type u_3} [SeminormedGroup E] {s : Set E} :
Bornology.IsBounded s∃ (C : ), xs, x C

Alias of the forward direction of isBounded_iff_forall_norm_le'.

theorem Bornology.IsBounded.exists_norm_le {E : Type u_3} [SeminormedAddGroup E] {s : Set E} :
Bornology.IsBounded s∃ (C : ), xs, x C

Alias of the forward direction of isBounded_iff_forall_norm_le.

theorem Bornology.IsBounded.exists_pos_norm_le {E : Type u_3} [SeminormedAddGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
R > 0, xs, x R
theorem Bornology.IsBounded.exists_pos_norm_le' {E : Type u_3} [SeminormedGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
R > 0, xs, x R
theorem Bornology.IsBounded.exists_pos_norm_lt {E : Type u_3} [SeminormedAddGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
R > 0, xs, x < R
theorem Bornology.IsBounded.exists_pos_norm_lt' {E : Type u_3} [SeminormedGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
R > 0, xs, x < R
theorem NormedAddCommGroup.cauchySeq_iff {α : Type u_1} {E : Type u_3} [SeminormedAddGroup E] [Nonempty α] [SemilatticeSup α] {u : αE} :
CauchySeq u ε > 0, ∃ (N : α), ∀ (m : α), N m∀ (n : α), N nu m - u n < ε
theorem NormedCommGroup.cauchySeq_iff {α : Type u_1} {E : Type u_3} [SeminormedGroup E] [Nonempty α] [SemilatticeSup α] {u : αE} :
CauchySeq u ε > 0, ∃ (N : α), ∀ (m : α), N m∀ (n : α), N nu m / u n < ε
theorem IsCompact.exists_bound_of_continuousOn {α : Type u_1} {E : Type u_3} [SeminormedAddGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : αE} (hf : ContinuousOn f s) :
∃ (C : ), xs, f x C
theorem IsCompact.exists_bound_of_continuousOn' {α : Type u_1} {E : Type u_3} [SeminormedGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : αE} (hf : ContinuousOn f s) :
∃ (C : ), xs, f x C
theorem HasCompactSupport.exists_bound_of_continuous {α : Type u_1} {E : Type u_3} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} (hf : HasCompactSupport f) (h'f : Continuous f) :
∃ (C : ), ∀ (x : α), f x C
theorem HasCompactMulSupport.exists_bound_of_continuous {α : Type u_1} {E : Type u_3} [SeminormedGroup E] [TopologicalSpace α] {f : αE} (hf : HasCompactMulSupport f) (h'f : Continuous f) :
∃ (C : ), ∀ (x : α), f x C
theorem Filter.Tendsto.op_zero_isBoundedUnder_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) l (norm g)) (op : EFG) (h_op : ∃ (A : ), ∀ (x : E) (y : F), op x y A * x * y) :
Filter.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_3} {F : Type u_4} {G : Type u_5} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) l (norm g)) (op : EFG) (h_op : ∃ (A : ), ∀ (x : E) (y : F), op x y A * x * y) :
Filter.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_3} {F : Type u_4} {G : Type u_5} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) l (norm g)) (op : EFG) (h_op : ∀ (x : E) (y : F), op x y x * y) :
Filter.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 Filter.Tendsto.op_one_isBoundedUnder_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) l (norm g)) (op : EFG) (h_op : ∀ (x : E) (y : F), op x y x * y) :
Filter.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 Continuous.bounded_above_of_compact_support {α : Type u_1} {E : Type u_3} [NormedAddGroup E] [TopologicalSpace α] {f : αE} (hf : Continuous f) (h : HasCompactSupport f) :
∃ (C : ), ∀ (x : α), f x C
theorem HasCompactSupport.exists_pos_le_norm {α : Type u_1} {E : Type u_3} [NormedAddGroup α] {f : αE} [Zero E] (hf : HasCompactSupport f) :
∃ (R : ), 0 < R ∀ (x : α), R xf x = 0
theorem HasCompactMulSupport.exists_pos_le_norm {α : Type u_1} {E : Type u_3} [NormedAddGroup α] {f : αE} [One E] (hf : HasCompactMulSupport f) :
∃ (R : ), 0 < R ∀ (x : α), R xf x = 1