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 tendsto_norm_cobounded_atTop {E : Type u_3} [SeminormedAddGroup E] : Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop

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

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‖

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

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

@[simp]

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

@[simp]

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

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

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

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

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 : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

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

theorem Bornology.IsBounded.exists_norm_le' {E : Type u_3} [SeminormedGroup E] {s : Set E} : Bornology.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_3} [SeminormedAddGroup E] {s : Set E} : Bornology.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_3} [SeminormedAddGroup E] {s : Set E} (hs : Bornology.IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R

abbrev Bornology.IsBounded.exists_pos_norm_le.match_1 {E : Type u_1} [SeminormedAddGroup E] {s : Set E} (motive : (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) → Prop) : ∀ (x : ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C), (∀ (R₀ : ℝ) (hR₀ : ∀ x ∈ s, ‖x‖ ≤ R₀), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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

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

abbrev Bornology.IsBounded.exists_pos_norm_lt.match_1 {E : Type u_1} [SeminormedAddGroup E] {s : Set E} (motive : (∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R) → Prop) : ∀ (x : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R), (∀ (R : ℝ) (hR₀ : R > 0) (hR : ∀ x ∈ s, ‖x‖ ≤ R), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Bornology.IsBounded.exists_pos_norm_lt' {E : Type u_3} [SeminormedGroup E] {s : Set E} (hs : Bornology.IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖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 ≤ n → ‖u 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 ≤ n → ‖u 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 : ℝ), ∀ x ∈ s, ‖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 : ℝ), ∀ x ∈ s, ‖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 (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (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 (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (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 (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (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 (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (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 ≤ ‖x‖ → f 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 ≤ ‖x‖ → f x = 1