Mathlib.Analysis.Normed.Group.Bounded

comap_norm_atTop' theorem

: comap norm atTop = cobounded E

Full source

@[to_additive (attr := simp) comap_norm_atTop]
lemma comap_norm_atTop' : comap norm atTop = cobounded E := by
  simpa only [dist_one_right] using comap_dist_right_atTop (1 : E)

Preimage of Norm under `atTop` Equals Cobounded Filter

Informal description

The preimage of the norm function on a normed group $E$ under the filter `atTop` (which consists of all sets containing an interval $[a, \infty)$ for some $a \in \mathbb{R}$) is equal to the cobounded filter on $E$ (the filter of sets whose complements are bounded in the norm).

Filter.HasBasis.cobounded_of_norm' theorem

 {ι : Sort*} {p : ι → Prop} {s : ι → Set ℝ} (h : HasBasis atTop p s) : HasBasis (cobounded E) p fun i ↦ norm ⁻¹' s i

Full source

@[to_additive Filter.HasBasis.cobounded_of_norm]
lemma Filter.HasBasis.cobounded_of_norm' {ι : Sort*} {p : ι → Prop} {s : ι → Set ℝ}
    (h : HasBasis atTop p s) : HasBasis (cobounded E) p fun i ↦ normnorm ⁻¹' s i :=
  comap_norm_atTop' (E := E) ▸ h.comap _

Basis of Cobounded Filter via Norm Preimages

Informal description

Let $E$ be a normed group, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\mathbb{R}$ indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. If the filter `atTop` on $\mathbb{R}$ has a basis consisting of the sets $s_i$ satisfying $p(i)$, then the cobounded filter on $E$ has a basis consisting of the preimages $\text{norm}^{-1}(s_i)$ for those $i$ satisfying $p(i)$.

Filter.hasBasis_cobounded_norm' theorem

: HasBasis (cobounded E) (fun _ ↦ True) ({x | · ≤ ‖x‖})

Full source

@[to_additive Filter.hasBasis_cobounded_norm]
lemma Filter.hasBasis_cobounded_norm' : HasBasis (cobounded E) (fun _ ↦ True) ({x | · ≤ ‖x‖}) :=
  atTop_basis.cobounded_of_norm'

Basis of Cobounded Filter via Norm Thresholds

Informal description

The cobounded filter on a normed group $E$ has a basis consisting of all sets of the form $\{x \in E \mid r \leq \|x\|\}$ for some real number $r$.

tendsto_norm_atTop_iff_cobounded' theorem

{f : α → E} {l : Filter α} : Tendsto (‖f ·‖) l atTop ↔ Tendsto f l (cobounded E)

Full source

@[to_additive (attr := simp) tendsto_norm_atTop_iff_cobounded]
lemma tendsto_norm_atTop_iff_cobounded' {f : α → E} {l : Filter α} :
    TendstoTendsto (‖f ·‖) l atTop ↔ Tendsto f l (cobounded E) := by
  rw [← comap_norm_atTop', tendsto_comap_iff]; rfl

Equivalence of Norm Tending to Infinity and Function Tending to Cobounded Filter

Informal description

For a function $f \colon \alpha \to E$ and a filter $l$ on $\alpha$, the function $\|f(\cdot)\|$ tends to infinity along $l$ if and only if $f$ tends to the cobounded filter along $l$. In other words, $\lim_{l} \|f\| = \infty$ is equivalent to $\lim_{l} f$ being in the cobounded filter of $E$.

tendsto_norm_cobounded_atTop' theorem

: Tendsto norm (cobounded E) atTop

Full source

@[to_additive tendsto_norm_cobounded_atTop]
lemma tendsto_norm_cobounded_atTop' : Tendsto norm (cobounded E) atTop :=
  tendsto_norm_atTop_iff_cobounded'.2 tendsto_id

Norm Tends to Infinity Along Cobounded Filter

Informal description

The norm function $\|\cdot\|$ tends to infinity along the cobounded filter of $E$, i.e., $\lim_{\text{cobounded } E} \|\cdot\| = \infty$.

eventually_cobounded_le_norm' theorem

(a : ℝ) : ∀ᶠ x in cobounded E, a ≤ ‖x‖

Full source

@[to_additive eventually_cobounded_le_norm]
lemma eventually_cobounded_le_norm' (a : ℝ) : ∀ᶠ x in cobounded E, a ≤ ‖x‖ :=
  tendsto_norm_cobounded_atTop'.eventually_ge_atTop a

Lower Bound on Norm in Cobounded Subset of Normed Group

Informal description

For any real number $a$, there exists a cobounded subset of $E$ such that for all $x$ in this subset, $a \leq \|x\|$.

tendsto_norm_cocompact_atTop' theorem

[ProperSpace E] : Tendsto norm (cocompact E) atTop

Full source

@[to_additive tendsto_norm_cocompact_atTop]
lemma tendsto_norm_cocompact_atTop' [ProperSpace E] : Tendsto norm (cocompact E) atTop :=
  cobounded_eq_cocompact (α := E) ▸ tendsto_norm_cobounded_atTop'

Norm tends to infinity at infinity in proper normed groups

Informal description

For a proper normed group $E$, the norm function $\|\cdot\|$ tends to infinity along the cocompact filter of $E$, i.e., $\lim_{\text{cocompact } E} \|\cdot\| = \infty$.

Filter.inv_cobounded theorem

: (cobounded E)⁻¹ = cobounded E

Full source

@[to_additive (attr := simp)]
lemma Filter.inv_cobounded : (cobounded E)⁻¹ = cobounded E := by
  simp only [← comap_norm_atTop', ← Filter.comap_inv, comap_comap, Function.comp_def, norm_inv']

Inverse of Cobounded Filter Equals Cobounded Filter in Normed Groups

Informal description

For a normed group $E$, the inverse of the cobounded filter on $E$ is equal to the cobounded filter itself, i.e., $(\text{cobounded } E)^{-1} = \text{cobounded } E$.

Filter.tendsto_inv_cobounded theorem

: Tendsto Inv.inv (cobounded E) (cobounded E)

Full source

/-- In a (semi)normed group, inversion `x ↦ x⁻¹` tends to infinity at infinity. -/
@[to_additive "In a (semi)normed group, negation `x ↦ -x` tends to infinity at infinity."]
theorem Filter.tendsto_inv_cobounded : Tendsto Inv.inv (cobounded E) (cobounded E) :=
  inv_cobounded.le

Inversion Tends to Infinity at Infinity in Normed Groups

Informal description

In a normed group $E$, the inversion operation $x \mapsto x^{-1}$ tends to infinity at infinity, meaning that the inverse of any unbounded set is also unbounded. Formally, the inversion function maps the cobounded filter on $E$ to itself, i.e., $\text{Inv.inv} \colon \text{cobounded } E \to \text{cobounded } E$.

isBounded_iff_forall_norm_le' theorem

: Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C

Full source

@[to_additive isBounded_iff_forall_norm_le]
lemma isBounded_iff_forall_norm_le' : Bornology.IsBoundedBornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C := by
  simpa only [Set.subset_def, mem_closedBall_one_iff] using isBounded_iff_subset_closedBall (1 : E)

Boundedness Criterion via Norm in Normed Groups

Informal description

A subset $s$ of a normed group is bounded if and only if there exists a constant $C$ such that for every element $x \in s$, the norm of $x$ satisfies $\|x\| \leq C$.

Bornology.IsBounded.exists_pos_norm_le' theorem

(hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R

Full source

@[to_additive exists_pos_norm_le]
lemma Bornology.IsBounded.exists_pos_norm_le' (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R :=
  let ⟨R₀, hR₀⟩ := hs.exists_norm_le'
  ⟨max R₀ 1, by positivity, fun x hx => (hR₀ x hx).trans <| le_max_left _ _⟩

Existence of Uniform Norm Bound for Bounded Sets in Normed Groups

Informal description

For any bounded subset $s$ of a normed group, there exists a positive real number $R > 0$ such that for every element $x \in s$, the norm of $x$ satisfies $\|x\| \leq R$.

Bornology.IsBounded.exists_pos_norm_lt' theorem

(hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R

Full source

@[to_additive Bornology.IsBounded.exists_pos_norm_lt]
lemma Bornology.IsBounded.exists_pos_norm_lt' (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R :=
  let ⟨R, hR₀, hR⟩ := hs.exists_pos_norm_le'
  ⟨R + 1, by positivity, fun x hx ↦ (hR x hx).trans_lt (lt_add_one _)⟩

Existence of Strict Uniform Norm Bound for Bounded Sets in Normed Groups

Informal description

For any bounded subset $s$ of a normed group, there exists a positive real number $R > 0$ such that for every element $x \in s$, the norm of $x$ satisfies $\|x\| < R$.

NormedCommGroup.cauchySeq_iff theorem

 [Nonempty α] [SemilatticeSup α] {u : α → E} : CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → ‖u m / u n‖ < ε

Full source

@[to_additive]
lemma NormedCommGroup.cauchySeq_iff [Nonempty α] [SemilatticeSup α] {u : α → E} :
    CauchySeqCauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → ‖u m / u n‖ < ε := by
  simp [Metric.cauchySeq_iff, dist_eq_norm_div]

Cauchy Sequence Criterion in Normed Commutative Groups

Informal description

Let $E$ be a normed commutative group, and let $\alpha$ be a nonempty directed set (specifically, a nonempty join-semilattice). A sequence $u : \alpha \to E$ is a Cauchy sequence if and only if for every $\varepsilon > 0$, there exists an index $N \in \alpha$ such that for all $m, n \geq N$, the norm of the quotient $\|u(m) / u(n)\|$ is less than $\varepsilon$.

IsCompact.exists_bound_of_continuousOn' theorem

 [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : α → E} (hf : ContinuousOn f s) : ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C

Full source

@[to_additive IsCompact.exists_bound_of_continuousOn]
lemma IsCompact.exists_bound_of_continuousOn' [TopologicalSpace α] {s : Set α} (hs : IsCompact s)
    {f : α → E} (hf : ContinuousOn f s) : ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C :=
  (isBounded_iff_forall_norm_le'.1 (hs.image_of_continuousOn hf).isBounded).imp fun _C hC _x hx =>
    hC _ <| Set.mem_image_of_mem _ hx

Norm Bound for Continuous Functions on Compact Sets

Informal description

Let $X$ be a topological space, $E$ a normed group, $s \subseteq X$ a compact subset, and $f : X \to E$ a function that is continuous on $s$. Then there exists a constant $C$ such that for every $x \in s$, the norm of $f(x)$ satisfies $\|f(x)\| \leq C$.

HasCompactMulSupport.exists_bound_of_continuous theorem

[TopologicalSpace α] {f : α → E} (hf : HasCompactMulSupport f) (h'f : Continuous f) : ∃ C, ∀ x, ‖f x‖ ≤ C

Full source

@[to_additive]
lemma HasCompactMulSupport.exists_bound_of_continuous [TopologicalSpace α]
    {f : α → E} (hf : HasCompactMulSupport f) (h'f : Continuous f) : ∃ C, ∀ x, ‖f x‖ ≤ C := by
  simpa using (hf.isCompact_range h'f).isBounded.exists_norm_le'

Boundedness of Continuous Functions with Compact Multiplicative Support

Informal description

Let $f : \alpha \to E$ be a continuous function between topological spaces with compact multiplicative support. Then there exists a constant $C$ such that for all $x \in \alpha$, the norm of $f(x)$ satisfies $\|f(x)\| \leq C$.

Filter.Tendsto.op_one_isBoundedUnder_le' theorem

 {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (𝓝 1)) (hg : IsBoundedUnder (· ≤ ·) l (Norm.norm ∘ g))
  (op : E → F → G) (h_op : ∃ A, ∀ x y, ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) : Tendsto (fun x => op (f x) (g x)) l (𝓝 1)

Full source

/-- 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 (•)`. -/
@[to_additive "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 (•)`."]
lemma Filter.Tendsto.op_one_isBoundedUnder_le' {f : α → E} {g : α → F} {l : Filter α}
    (hf : Tendsto f l (𝓝 1)) (hg : IsBoundedUnder (· ≤ ·) l (Norm.normNorm.norm ∘ g)) (op : E → F → G)
    (h_op : ∃ A, ∀ x y, ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) : Tendsto (fun x => op (f x) (g x)) l (𝓝 1) := by
  obtain ⟨A, h_op⟩ := h_op
  rcases hg with ⟨C, hC⟩; rw [eventually_map] at hC
  rw [NormedCommGroup.tendsto_nhds_one] at hf ⊢
  intro ε ε₀
  rcases exists_pos_mul_lt ε₀ (A * C) with ⟨δ, δ₀, hδ⟩
  filter_upwards [hf δ δ₀, hC] with i hf hg
  refine (h_op _ _).trans_lt ?_
  rcases le_total A 0 with hA | hA
  · exact (mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <|
      norm_nonneg' _).trans_lt ε₀
  calc
    A * ‖f i‖ * ‖g i‖ ≤ A * δ * C := by gcongr; exact hg
    _ = A * C * δ := mul_right_comm _ _ _
    _ < ε := hδ

Limit of Bounded Operation with Function Tending to One

Informal description

Let $E$, $F$, and $G$ be normed groups, and let $f : \alpha \to E$ and $g : \alpha \to F$ be functions defined on some type $\alpha$. Consider a filter $l$ on $\alpha$ such that $f$ tends to $1$ along $l$ and the norm of $g$ is bounded above along $l$. For any binary operation $\mathrm{op} : E \to F \to G$ satisfying $\|\mathrm{op}(x, y)\| \leq A \cdot \|x\| \cdot \|y\|$ for some constant $A > 0$, the function $\lambda x \mapsto \mathrm{op}(f(x), g(x))$ tends to $1$ along $l$.

Filter.Tendsto.op_one_isBoundedUnder_le theorem

 {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (𝓝 1)) (hg : IsBoundedUnder (· ≤ ·) l (Norm.norm ∘ g))
  (op : E → F → G) (h_op : ∀ x y, ‖op x y‖ ≤ ‖x‖ * ‖y‖) : Tendsto (fun x => op (f x) (g x)) l (𝓝 1)

Full source

/-- 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 (•)`. -/
@[to_additive "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 {f : α → E} {g : α → F} {l : Filter α}
    (hf : Tendsto f l (𝓝 1)) (hg : IsBoundedUnder (· ≤ ·) l (Norm.normNorm.norm ∘ g)) (op : E → F → G)
    (h_op : ∀ x y, ‖op x y‖ ≤ ‖x‖ * ‖y‖) : Tendsto (fun x => op (f x) (g x)) l (𝓝 1) :=
  hf.op_one_isBoundedUnder_le' hg op ⟨1, fun x y => (one_mul ‖x‖).symm ▸ h_op x y⟩

Limit of Bounded Operation with Function Tending to One (Submultiplicative Case)

Informal description

Let $E$, $F$, and $G$ be normed groups, and let $f : \alpha \to E$ and $g : \alpha \to F$ be functions defined on some type $\alpha$. Consider a filter $l$ on $\alpha$ such that $f$ tends to $1$ along $l$ and the norm of $g$ is bounded above along $l$. For any binary operation $\mathrm{op} : E \to F \to G$ satisfying $\|\mathrm{op}(x, y)\| \leq \|x\| \cdot \|y\|$ for all $x \in E$ and $y \in F$, the function $\lambda x \mapsto \mathrm{op}(f(x), g(x))$ tends to $1$ along $l$.

Continuous.bounded_above_of_compact_support theorem

(hf : Continuous f) (h : HasCompactSupport f) : ∃ C, ∀ x, ‖f x‖ ≤ C

Full source

lemma Continuous.bounded_above_of_compact_support (hf : Continuous f) (h : HasCompactSupport f) :
    ∃ C, ∀ x, ‖f x‖ ≤ C := by
  simpa [bddAbove_def] using hf.norm.bddAbove_range_of_hasCompactSupport h.norm

Boundedness of Continuous Functions with Compact Support

Informal description

Let $f : \alpha \to E$ be a continuous function with compact support. Then there exists a constant $C \in \mathbb{R}$ such that for all $x \in \alpha$, the norm of $f(x)$ is bounded above by $C$, i.e., $\|f(x)\| \leq C$.

HasCompactMulSupport.exists_pos_le_norm theorem

[One E] (hf : HasCompactMulSupport f) : ∃ R : ℝ, 0 < R ∧ ∀ x : α, R ≤ ‖x‖ → f x = 1

Full source

@[to_additive]
lemma HasCompactMulSupport.exists_pos_le_norm [One E] (hf : HasCompactMulSupport f) :
    ∃ R : ℝ, 0 < R ∧ ∀ x : α, R ≤ ‖x‖ → f x = 1 := by
  obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf
  obtain ⟨S, hS, hS'⟩ := hK1.isBounded.exists_pos_norm_le
  refine ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) ?_)⟩
  contrapose! hx
  exact lt_add_of_le_of_pos hx zero_lt_one

Existence of Radius Beyond Which a Function with Compact Multiplicative Support is Constant One

Informal description

Let $E$ be a type with a multiplicative identity element, and let $f : \alpha \to E$ be a function with compact multiplicative support. Then there exists a positive real number $R > 0$ such that for all $x \in \alpha$ with $\|x\| \geq R$, we have $f(x) = 1$.

Tags