Mathlib.Analysis.Normed.Group.Continuity

tendsto_iff_norm_div_tendsto_zero theorem

{f : α → E} {a : Filter α} {b : E} : Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0)

Full source

@[to_additive]
theorem tendsto_iff_norm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E} :
    TendstoTendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0) := by
  simp only [← dist_eq_norm_div, ← tendsto_iff_dist_tendsto_zero]

Convergence Criterion via Norm of Quotient

Informal description

For a function $f \colon \alpha \to E$ and a filter $a$ on $\alpha$, the function $f$ tends to $b \in E$ with respect to the filter $a$ if and only if the norm of the quotient $\|f(e) / b\|$ tends to $0$ with respect to the filter $a$.

tendsto_one_iff_norm_tendsto_zero theorem

{f : α → E} {a : Filter α} : Tendsto f a (𝓝 1) ↔ Tendsto (‖f ·‖) a (𝓝 0)

Full source

@[to_additive]
theorem tendsto_one_iff_norm_tendsto_zero {f : α → E} {a : Filter α} :
    TendstoTendsto f a (𝓝 1) ↔ Tendsto (‖f ·‖) a (𝓝 0) :=
  tendsto_iff_norm_div_tendsto_zero.trans <| by simp only [div_one]

Convergence to Identity via Norm: $f \to 1$ iff $\|f\| \to 0$

Informal description

For a function $f \colon \alpha \to E$ and a filter $a$ on $\alpha$, the function $f$ tends to the identity element $1 \in E$ with respect to the filter $a$ if and only if the norm $\|f(\cdot)\|$ tends to $0$ with respect to the filter $a$.

comap_norm_nhds_one theorem

: comap norm (𝓝 0) = 𝓝 (1 : E)

Full source

@[to_additive (attr := simp 1100)]
theorem comap_norm_nhds_one : comap norm (𝓝 0) = 𝓝 (1 : E) := by
  simpa only [dist_one_right] using nhds_comap_dist (1 : E)

Norm Preimage of Zero Neighborhood Equals Identity Neighborhood

Informal description

The preimage of the neighborhood filter of $0$ under the norm function is equal to the neighborhood filter of the identity element $1$ in the group $E$, i.e., $\text{comap}(\|\cdot\|, \mathcal{N}(0)) = \mathcal{N}(1)$.

squeeze_one_norm' theorem

 {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ᶠ n in t₀, ‖f n‖ ≤ a n) (h' : Tendsto a t₀ (𝓝 0)) : Tendsto f t₀ (𝓝 1)

Full source

/-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real
function `a` which tends to `0`, then `f` tends to `1` (neutral element of `SeminormedGroup`).
In this pair of lemmas (`squeeze_one_norm'` and `squeeze_one_norm`), following a convention of
similar lemmas in `Topology.MetricSpace.Basic` and `Topology.Algebra.Order`, the `'` version is
phrased using "eventually" and the non-`'` version is phrased absolutely. -/
@[to_additive "Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a
real function `a` which tends to `0`, then `f` tends to `0`. In this pair of lemmas
(`squeeze_zero_norm'` and `squeeze_zero_norm`), following a convention of similar lemmas in
`Topology.MetricSpace.Pseudo.Defs` and `Topology.Algebra.Order`, the `'` version is phrased using
\"eventually\" and the non-`'` version is phrased absolutely."]
theorem squeeze_one_norm' {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ᶠ n in t₀, ‖f n‖ ≤ a n)
    (h' : Tendsto a t₀ (𝓝 0)) : Tendsto f t₀ (𝓝 1) :=
  tendsto_one_iff_norm_tendsto_zero.2 <|
    squeeze_zero' (Eventually.of_forall fun _n => norm_nonneg' _) h h'

Sandwich Theorem for Norm Convergence: $\|f\| \leq a \to 0$ implies $f \to 1$

Informal description

Let $f \colon \alpha \to E$ be a function and $a \colon \alpha \to \mathbb{R}$ be a real-valued function. If there exists a filter $t_0$ on $\alpha$ such that eventually for all $n$ in $t_0$, the norm $\|f(n)\|$ is bounded above by $a(n)$, and if $a$ tends to $0$ with respect to $t_0$, then $f$ tends to the identity element $1 \in E$ with respect to $t_0$.

squeeze_one_norm theorem

 {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ n, ‖f n‖ ≤ a n) : Tendsto a t₀ (𝓝 0) → Tendsto f t₀ (𝓝 1)

Full source

/-- Special case of the sandwich theorem: if the norm of `f` is bounded by a real function `a` which
tends to `0`, then `f` tends to `1`. -/
@[to_additive "Special case of the sandwich theorem: if the norm of `f` is bounded by a real
function `a` which tends to `0`, then `f` tends to `0`."]
theorem squeeze_one_norm {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ n, ‖f n‖ ≤ a n) :
    Tendsto a t₀ (𝓝 0) → Tendsto f t₀ (𝓝 1) :=
  squeeze_one_norm' <| Eventually.of_forall h

Sandwich Theorem for Norm Convergence: $\|f\| \leq a \to 0$ implies $f \to 1$

Informal description

Let $f \colon \alpha \to E$ be a function and $a \colon \alpha \to \mathbb{R}$ be a real-valued function. If for all $n \in \alpha$, the norm $\|f(n)\|$ is bounded above by $a(n)$, and if $a$ tends to $0$ with respect to a filter $t_0$ on $\alpha$, then $f$ tends to the identity element $1 \in E$ with respect to $t_0$.

tendsto_norm_div_self theorem

(x : E) : Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0)

Full source

@[to_additive]
theorem tendsto_norm_div_self (x : E) : Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0) := by
  simpa [dist_eq_norm_div] using
    tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)

Norm of Division Tends to Zero at Identity

Informal description

For any element $x$ in a normed group $E$, the function $a \mapsto \|a / x\|$ tends to $0$ as $a$ tends to $x$ in the neighborhood filter of $x$.

tendsto_norm_div_self_nhdsGE theorem

(x : E) : Tendsto (fun a ↦ ‖a / x‖) (𝓝 x) (𝓝[≥] 0)

Full source

@[to_additive]
theorem tendsto_norm_div_self_nhdsGE (x : E) : Tendsto (fun a ↦ ‖a / x‖) (𝓝 x) (𝓝[≥] 0) :=
  tendsto_nhdsWithin_iff.mpr ⟨tendsto_norm_div_self x, by simp⟩

Norm of Division Tends to Zero from Above at Identity

Informal description

For any element $x$ in a normed group $E$, the function $a \mapsto \|a / x\|$ tends to $0$ from above as $a$ tends to $x$ in the neighborhood filter of $x$. That is, the limit of $\|a / x\|$ as $a \to x$ is $0$, and all values of $\|a / x\|$ are non-negative.

tendsto_norm' theorem

{x : E} : Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖)

Full source

@[to_additive tendsto_norm]
theorem tendsto_norm' {x : E} : Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖) := by
  simpa using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (1 : E)) _ _)

Limit of Norm at a Point in Seminormed Groups

Informal description

For any element $x$ in a seminormed group $E$, the function $a \mapsto \|a\|$ tends to $\|x\|$ in the neighborhood filter of $x$.

tendsto_norm_one theorem

: Tendsto (fun a : E => ‖a‖) (𝓝 1) (𝓝 0)

Full source

/-- See `tendsto_norm_one` for a version with pointed neighborhoods. -/
@[to_additive "See `tendsto_norm_zero` for a version with pointed neighborhoods."]
theorem tendsto_norm_one : Tendsto (fun a : E => ‖a‖) (𝓝 1) (𝓝 0) := by
  simpa using tendsto_norm_div_self (1 : E)

Norm Tends to Zero at Identity in Seminormed Groups

Informal description

The norm function $\|\cdot\|$ tends to $0$ as its argument tends to the identity element $1$ in a seminormed group $E$.

continuous_norm' theorem

: Continuous fun a : E => ‖a‖

Full source

@[to_additive (attr := continuity, fun_prop) continuous_norm]
theorem continuous_norm' : Continuous fun a : E => ‖a‖ := by
  simpa using continuous_id.dist (continuous_const : Continuous fun _a => (1 : E))

Continuity of the Norm in Seminormed Groups

Informal description

The norm function $\|\cdot\|$ on a seminormed group $E$ is continuous.

continuous_nnnorm' theorem

: Continuous fun a : E => ‖a‖₊

Full source

@[to_additive (attr := continuity, fun_prop) continuous_nnnorm]
theorem continuous_nnnorm' : Continuous fun a : E => ‖a‖₊ :=
  continuous_norm'.subtype_mk _

Continuity of the Nonnegative Norm in Seminormed Groups

Informal description

The nonnegative norm function $\|\cdot\|₊$ on a seminormed group $E$ is continuous.

SeminormedGroup.toContinuousENorm instance

[SeminormedGroup E] : ContinuousENorm E

Full source

@[to_additive]
instance SeminormedGroup.toContinuousENorm [SeminormedGroup E] : ContinuousENorm E where
  continuous_enorm := ENNReal.isOpenEmbedding_coe.continuous.comp continuous_nnnorm'

Continuity of the Norm in Seminormed Groups

Informal description

For any seminormed group $E$, the norm function $\| \cdot \|$ on $E$ is continuous.

NormedGroup.toENormedMonoid instance

{F : Type*} [NormedGroup F] : ENormedMonoid F

Full source

@[to_additive]
instance NormedGroup.toENormedMonoid {F : Type*} [NormedGroup F] : ENormedMonoid F where
  enorm_eq_zero := by simp [enorm_eq_nnnorm]
  enorm_mul_le := by simp [enorm_eq_nnnorm, ← coe_add, nnnorm_mul_le']

Normed Groups as Enriched Normed Monoids

Informal description

Every normed group $F$ is also an enriched normed monoid.

NormedCommGroup.toENormedCommMonoid instance

[NormedCommGroup E] : ENormedCommMonoid E

Full source

@[to_additive]
instance NormedCommGroup.toENormedCommMonoid [NormedCommGroup E] : ENormedCommMonoid E where
  mul_comm := by simp [mul_comm]

Normed Commutative Groups as Enriched Normed Commutative Monoids

Informal description

Every normed commutative group $E$ is also an enriched normed commutative monoid.

Inseparable.norm_eq_norm' theorem

{u v : E} (h : Inseparable u v) : ‖u‖ = ‖v‖

Full source

@[to_additive Inseparable.norm_eq_norm]
theorem Inseparable.norm_eq_norm' {u v : E} (h : Inseparable u v) : ‖u‖ = ‖v‖ :=
  h.map continuous_norm' |>.eq

Norm Equality for Topologically Inseparable Points

Informal description

For any two points $u$ and $v$ in a seminormed group $E$, if $u$ and $v$ are topologically inseparable (i.e., $u \sim_i v$), then their norms are equal, i.e., $\|u\| = \|v\|$.

Inseparable.nnnorm_eq_nnnorm' theorem

{u v : E} (h : Inseparable u v) : ‖u‖₊ = ‖v‖₊

Full source

@[to_additive Inseparable.nnnorm_eq_nnnorm]
theorem Inseparable.nnnorm_eq_nnnorm' {u v : E} (h : Inseparable u v) : ‖u‖₊ = ‖v‖₊ :=
  h.map continuous_nnnorm' |>.eq

Equality of Nonnegative Norms for Inseparable Points in Seminormed Groups

Informal description

For any two points $u$ and $v$ in a seminormed group $E$, if $u$ and $v$ are topologically inseparable (i.e., $u \sim_i v$), then their nonnegative norms are equal, i.e., $\|u\|₊ = \|v\|₊$.

Inseparable.enorm_eq_enorm' theorem

{E : Type*} [TopologicalSpace E] [ContinuousENorm E] {u v : E} (h : Inseparable u v) : ‖u‖ₑ = ‖v‖ₑ

Full source

@[to_additive Inseparable.enorm_eq_enorm]
theorem Inseparable.enorm_eq_enorm' {E : Type*} [TopologicalSpace E] [ContinuousENorm E]
    {u v : E} (h : Inseparable u v) : ‖u‖ₑ = ‖v‖ₑ :=
  h.map continuous_enorm |>.eq

Equality of Extended Norms for Topologically Inseparable Points

Informal description

Let $E$ be a topological space equipped with a continuous extended norm $\|\cdot\|_e$. For any two points $u, v \in E$ that are topologically inseparable, their extended norms are equal, i.e., $\|u\|_e = \|v\|_e$.

mem_closure_one_iff_norm theorem

{x : E} : x ∈ closure ({ 1 } : Set E) ↔ ‖x‖ = 0

Full source

@[to_additive]
theorem mem_closure_one_iff_norm {x : E} : x ∈ closure ({1} : Set E)x ∈ closure ({1} : Set E) ↔ ‖x‖ = 0 := by
  rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).le_iff_eq]

Characterization of Closure of Identity via Norm: $\overline{\{1\}} = \{x \mid \|x\| = 0\}$

Informal description

For any element $x$ in a topological group $E$ with a norm, $x$ belongs to the closure of the singleton set $\{1\}$ if and only if the norm of $x$ is zero, i.e., $x \in \overline{\{1\}} \leftrightarrow \|x\| = 0$.

closure_one_eq theorem

: closure ({ 1 } : Set E) = {x | ‖x‖ = 0}

Full source

@[to_additive]
theorem closure_one_eq : closure ({1} : Set E) = { x | ‖x‖ = 0 } :=
  Set.ext fun _x => mem_closure_one_iff_norm

Closure of Identity Equals Zero Norm Set

Informal description

The closure of the singleton set $\{1\}$ in a topological group $E$ with a norm is equal to the set of all elements $x \in E$ with zero norm, i.e., $\overline{\{1\}} = \{x \mid \|x\| = 0\}$.

Filter.Tendsto.norm' theorem

(h : Tendsto f l (𝓝 a)) : Tendsto (fun x => ‖f x‖) l (𝓝 ‖a‖)

Full source

@[to_additive Filter.Tendsto.norm]
theorem Filter.Tendsto.norm' (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => ‖f x‖) l (𝓝 ‖a‖) :=
  tendsto_norm'.comp h

Convergence of Norm Along a Filter

Informal description

Let $f$ be a function from a topological space to a seminormed group $E$, and let $l$ be a filter. If $f$ tends to $a$ along $l$, then the norm $\|f(x)\|$ tends to $\|a\|$ along $l$.

Filter.Tendsto.nnnorm' theorem

(h : Tendsto f l (𝓝 a)) : Tendsto (fun x => ‖f x‖₊) l (𝓝 ‖a‖₊)

Full source

@[to_additive Filter.Tendsto.nnnorm]
theorem Filter.Tendsto.nnnorm' (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => ‖f x‖₊) l (𝓝 ‖a‖₊) :=
  Tendsto.comp continuous_nnnorm'.continuousAt h

Convergence of Nonnegative Norm Along a Filter

Informal description

Let $f$ be a function from a topological space to a seminormed group $E$, and let $l$ be a filter. If $f$ tends to $a$ along $l$, then the nonnegative norm $\|f(x)\|₊$ tends to $\|a\|₊$ along $l$.

Filter.Tendsto.enorm' theorem

(h : Tendsto f l (𝓝 a)) : Tendsto (‖f ·‖ₑ) l (𝓝 ‖a‖ₑ)

Full source

@[to_additive Filter.Tendsto.enorm]
lemma Filter.Tendsto.enorm' (h : Tendsto f l (𝓝 a)) : Tendsto (‖f ·‖ₑ) l (𝓝 ‖a‖ₑ) :=
  .comp continuous_enorm.continuousAt h

Convergence of Extended Norm Along a Filter

Informal description

Let $f$ be a function such that $f$ tends to $a$ along a filter $l$. Then the extended norm $\|f(\cdot)\|_e$ tends to $\|a\|_e$ along the same filter $l$.

Continuous.norm' theorem

: Continuous f → Continuous fun x => ‖f x‖

Full source

@[to_additive (attr := fun_prop) Continuous.norm]
theorem Continuous.norm' : Continuous f → Continuous fun x => ‖f x‖ :=
  continuous_norm'.comp

Continuity of the Norm under Continuous Functions

Informal description

If $f$ is a continuous function, then the function $x \mapsto \|f(x)\|$ is also continuous.

Continuous.nnnorm' theorem

: Continuous f → Continuous fun x => ‖f x‖₊

Full source

@[to_additive (attr := fun_prop) Continuous.nnnorm]
theorem Continuous.nnnorm' : Continuous f → Continuous fun x => ‖f x‖₊ :=
  continuous_nnnorm'.comp

Continuity of the Nonnegative Norm under Continuous Functions

Informal description

If $f$ is a continuous function, then the function $x \mapsto \|f(x)\|₊$ is also continuous, where $\|\cdot\|₊$ denotes the nonnegative norm.

ContinuousAt.norm' theorem

{a : α} (h : ContinuousAt f a) : ContinuousAt (fun x => ‖f x‖) a

Full source

@[to_additive (attr := fun_prop) ContinuousAt.norm]
theorem ContinuousAt.norm' {a : α} (h : ContinuousAt f a) : ContinuousAt (fun x => ‖f x‖) a :=
  Tendsto.norm' h

Continuity of Norm at a Point

Informal description

Let $f$ be a function from a topological space $\alpha$ to a seminormed group $E$, and let $a \in \alpha$. If $f$ is continuous at $a$, then the function $x \mapsto \|f(x)\|$ is also continuous at $a$.

ContinuousAt.nnnorm' theorem

{a : α} (h : ContinuousAt f a) : ContinuousAt (fun x => ‖f x‖₊) a

Full source

@[to_additive (attr := fun_prop) ContinuousAt.nnnorm]
theorem ContinuousAt.nnnorm' {a : α} (h : ContinuousAt f a) : ContinuousAt (fun x => ‖f x‖₊) a :=
  Tendsto.nnnorm' h

Continuity of Nonnegative Norm at a Point

Informal description

Let $f$ be a function from a topological space $\alpha$ to a seminormed group $E$, and let $a \in \alpha$. If $f$ is continuous at $a$, then the function $x \mapsto \|f(x)\|₊$ is also continuous at $a$, where $\|\cdot\|₊$ denotes the nonnegative norm.

ContinuousWithinAt.norm' theorem

{s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x => ‖f x‖) s a

Full source

@[to_additive ContinuousWithinAt.norm]
theorem ContinuousWithinAt.norm' {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
    ContinuousWithinAt (fun x => ‖f x‖) s a :=
  Tendsto.norm' h

Continuity of Norm Within a Subset at a Point

Informal description

Let $f : \alpha \to E$ be a function from a topological space $\alpha$ to a seminormed group $E$, and let $s \subseteq \alpha$ and $a \in \alpha$. If $f$ is continuous within $s$ at $a$, then the function $x \mapsto \|f(x)\|$ is also continuous within $s$ at $a$.

ContinuousWithinAt.nnnorm' theorem

{s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x => ‖f x‖₊) s a

Full source

@[to_additive ContinuousWithinAt.nnnorm]
theorem ContinuousWithinAt.nnnorm' {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
    ContinuousWithinAt (fun x => ‖f x‖₊) s a :=
  Tendsto.nnnorm' h

Continuity of Nonnegative Norm Within a Subset at a Point

Informal description

Let $f$ be a function from a topological space $\alpha$ to a seminormed group $E$, and let $s$ be a subset of $\alpha$ and $a$ a point in $\alpha$. If $f$ is continuous within $s$ at $a$, then the nonnegative norm function $x \mapsto \|f(x)\|₊$ is also continuous within $s$ at $a$.

ContinuousOn.norm' theorem

{s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun x => ‖f x‖) s

Full source

@[to_additive (attr := fun_prop) ContinuousOn.norm]
theorem ContinuousOn.norm' {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun x => ‖f x‖) s :=
  fun x hx => (h x hx).norm'

Continuity of Norm on a Subset

Informal description

Let $f : \alpha \to E$ be a function from a topological space $\alpha$ to a seminormed group $E$, and let $s \subseteq \alpha$. If $f$ is continuous on $s$, then the function $x \mapsto \|f(x)\|$ is also continuous on $s$.

ContinuousOn.nnnorm' theorem

{s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun x => ‖f x‖₊) s

Full source

@[to_additive (attr := fun_prop) ContinuousOn.nnnorm]
theorem ContinuousOn.nnnorm' {s : Set α} (h : ContinuousOn f s) :
    ContinuousOn (fun x => ‖f x‖₊) s := fun x hx => (h x hx).nnnorm'

Continuity of Nonnegative Norm on a Subset

Informal description

Let $f$ be a function from a topological space $\alpha$ to a seminormed group $E$, and let $s$ be a subset of $\alpha$. If $f$ is continuous on $s$, then the nonnegative norm function $x \mapsto \|f(x)\|₊$ is also continuous on $s$.

eventually_ne_of_tendsto_norm_atTop' theorem

{l : Filter α} {f : α → E} (h : Tendsto (fun y => ‖f y‖) l atTop) (x : E) : ∀ᶠ y in l, f y ≠ x

Full source

/-- If `‖y‖ → ∞`, then we can assume `y ≠ x` for any fixed `x`. -/
@[to_additive eventually_ne_of_tendsto_norm_atTop "If `‖y‖→∞`, then we can assume `y≠x` for any
fixed `x`"]
theorem eventually_ne_of_tendsto_norm_atTop' {l : Filter α} {f : α → E}
    (h : Tendsto (fun y => ‖f y‖) l atTop) (x : E) : ∀ᶠ y in l, f y ≠ x :=
  (h.eventually_ne_atTop _).mono fun _x => ne_of_apply_ne norm

Eventual Distinctness from Fixed Point under Norm Divergence

Informal description

Let $f : \alpha \to E$ be a function and $l$ a filter on $\alpha$. If the norm $\|f(y)\|$ tends to infinity as $y$ tends along $l$, then for any fixed $x \in E$, the function value $f(y)$ is eventually different from $x$ as $y$ tends along $l$.

SeminormedCommGroup.mem_closure_iff theorem

: a ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

Full source

@[to_additive]
theorem SeminormedCommGroup.mem_closure_iff :
    a ∈ closure sa ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε := by
  simp [Metric.mem_closure_iff, dist_eq_norm_div]

Characterization of Closure in Seminormed Commutative Groups via Norm of Quotient

Informal description

An element $a$ belongs to the closure of a set $s$ in a seminormed commutative group if and only if for every positive real number $\varepsilon$, there exists an element $b \in s$ such that the norm of the quotient $a / b$ is less than $\varepsilon$.

SeminormedGroup.tendstoUniformlyOn_one theorem

 {f : ι → κ → G} {s : Set κ} {l : Filter ι} : TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ i in l, ∀ x ∈ s, ‖f i x‖ < ε

Full source

@[to_additive]
theorem SeminormedGroup.tendstoUniformlyOn_one {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
    TendstoUniformlyOnTendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ i in l, ∀ x ∈ s, ‖f i x‖ < ε := by
  simp only [tendstoUniformlyOn_iff, Pi.one_apply, dist_one_left]

Uniform Convergence to Identity in Seminormed Groups via Norm Condition

Informal description

A family of functions $f_i : \kappa \to G$ indexed by $i \in \iota$ converges uniformly to the identity element $1$ on a set $s \subseteq \kappa$ with respect to a filter $l$ on $\iota$ if and only if for every $\varepsilon > 0$, there exists an event in $l$ such that for all $i$ in this event and all $x \in s$, the norm of $f_i(x)$ is less than $\varepsilon$.

SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one theorem

 {f : ι → κ → G} {l : Filter ι} {l' : Filter κ} :
  UniformCauchySeqOnFilter f l l' ↔
    TendstoUniformlyOnFilter (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'

Full source

@[to_additive]
theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {f : ι → κ → G}
    {l : Filter ι} {l' : Filter κ} :
    UniformCauchySeqOnFilterUniformCauchySeqOnFilter f l l' ↔
      TendstoUniformlyOnFilter (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l' := by
  refine ⟨fun hf u hu => ?_, fun hf u hu => ?_⟩
  · obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
    refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H 1 (f x.fst.fst x.snd / f x.fst.snd x.snd) ?_
    simpa [dist_eq_norm_div, norm_div_rev] using hx
  · obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
    refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H (f x.fst.fst x.snd) (f x.fst.snd x.snd) ?_
    simpa [dist_eq_norm_div, norm_div_rev] using hx

Uniformly Cauchy Family of Functions Converges to Identity via Quotient

Informal description

A family of functions $ f_i : \kappa \to G $ indexed by $ i \in \iota $ is uniformly Cauchy on a filter $ l' $ over $ \kappa $ with respect to a filter $ l $ on $ \iota $ if and only if the family of functions $ (n, z) \mapsto f_{n_1}(z) / f_{n_2}(z) $, where $ n = (n_1, n_2) \in \iota \times \iota $, converges uniformly to the identity element $ 1 $ on the filter $ l' $ with respect to the product filter $ l \times l $.

SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one theorem

 {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
  UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) s

Full source

@[to_additive]
theorem SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one {f : ι → κ → G} {s : Set κ}
    {l : Filter ι} :
    UniformCauchySeqOnUniformCauchySeqOn f l s ↔
      TendstoUniformlyOn (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) s := by
  rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
    uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
    SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]

Uniformly Cauchy Family of Functions on a Set Converges to Identity via Quotient

Informal description

Let $G$ be a seminormed group, $\iota$ and $\kappa$ be index types, $f : \iota \to \kappa \to G$ be a family of functions, $s \subseteq \kappa$ be a subset, and $l$ be a filter on $\iota$. Then the following are equivalent: 1. The family $f$ is uniformly Cauchy on $s$ with respect to $l$. 2. The family of functions $(n, z) \mapsto f_{n_1}(z) / f_{n_2}(z)$ (where $n = (n_1, n_2) \in \iota \times \iota$) converges uniformly to the identity element $1$ on $s$ with respect to the product filter $l \times l$.

controlled_prod_of_mem_closure theorem

 {s : Subgroup E} (hg : a ∈ closure (s : Set E)) {b : ℕ → ℝ} (b_pos : ∀ n, 0 < b n) :
  ∃ v : ℕ → E,
    Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ n, v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ n, 0 < n → ‖v n‖ < b n

Full source

@[to_additive]
theorem controlled_prod_of_mem_closure {s : Subgroup E} (hg : a ∈ closure (s : Set E)) {b : ℕ → ℝ}
    (b_pos : ∀ n, 0 < b n) :
    ∃ v : ℕ → E,
      Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
        (∀ n, v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ n, 0 < n → ‖v n‖ < b n := by
  obtain ⟨u : ℕ → E, u_in : ∀ n, u n ∈ s, lim_u : Tendsto u atTop (𝓝 a)⟩ :=
    mem_closure_iff_seq_limit.mp hg
  obtain ⟨n₀, hn₀⟩ : ∃ n₀, ∀ n ≥ n₀, ‖u n / a‖ < b 0 :=
    haveI : { x | ‖x / a‖ < b 0 }{ x | ‖x / a‖ < b 0 } ∈ 𝓝 a := by
      simp_rw [← dist_eq_norm_div]
      exact Metric.ball_mem_nhds _ (b_pos _)
    Filter.tendsto_atTop'.mp lim_u _ this
  set z : ℕ → E := fun n => u (n + n₀)
  have lim_z : Tendsto z atTop (𝓝 a) := lim_u.comp (tendsto_add_atTop_nat n₀)
  have mem_𝓤 : ∀ n, { p : E × E | ‖p.1 / p.2‖ < b (n + 1) }{ p : E × E | ‖p.1 / p.2‖ < b (n + 1) } ∈ 𝓤 E := fun n => by
    simpa [← dist_eq_norm_div] using Metric.dist_mem_uniformity (b_pos <| n + 1)
  obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ‖z (φ <| n + 1) / z (φ n)‖ < b (n + 1)⟩ :=
    lim_z.cauchySeq.subseq_mem mem_𝓤
  set w : ℕ → E := z ∘ φ
  have hw : Tendsto w atTop (𝓝 a) := lim_z.comp φ_extr.tendsto_atTop
  set v : ℕ → E := fun i => if i = 0 then w 0 else w i / w (i - 1)
  refine ⟨v, Tendsto.congr (Finset.eq_prod_range_div' w) hw, ?_, hn₀ _ (n₀.le_add_left _), ?_⟩
  · rintro ⟨⟩
    · change w 0 ∈ s
      apply u_in
    · apply s.div_mem <;> apply u_in
  · intro l hl
    obtain ⟨k, rfl⟩ : ∃ k, l = k + 1 := Nat.exists_eq_succ_of_ne_zero hl.ne'
    apply hφ

Controlled Product Approximation in Group Closure

Informal description

Let $E$ be a seminormed group, $s$ a subgroup of $E$, and $a \in \overline{s}$ (the closure of $s$ in $E$). Given a sequence of positive real numbers $(b_n)_{n \in \mathbb{N}}$, there exists a sequence $(v_n)_{n \in \mathbb{N}}$ in $E$ such that: 1. The product $\prod_{i=0}^n v_i$ converges to $a$ as $n \to \infty$, 2. Each $v_n$ belongs to $s$, 3. The norm $\|v_0 / a\| < b_0$, and 4. For all $n > 0$, $\|v_n\| < b_n$.

controlled_prod_of_mem_closure_range theorem

 {j : E →* F} {b : F} (hb : b ∈ closure (j.range : Set F)) {f : ℕ → ℝ} (b_pos : ∀ n, 0 < f n) :
  ∃ a : ℕ → E,
    Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧ ‖j (a 0) / b‖ < f 0 ∧ ∀ n, 0 < n → ‖j (a n)‖ < f n

Full source

@[to_additive]
theorem controlled_prod_of_mem_closure_range {j : E →* F} {b : F}
    (hb : b ∈ closure (j.range : Set F)) {f : ℕ → ℝ} (b_pos : ∀ n, 0 < f n) :
    ∃ a : ℕ → E,
      Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
        ‖j (a 0) / b‖ < f 0 ∧ ∀ n, 0 < n → ‖j (a n)‖ < f n := by
  obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos
  choose g hg using v_in
  exact
    ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀,
      fun n hn => by simpa [hg] using hv_pos n hn⟩

Controlled Product Approximation in Closure of Homomorphism Range

Informal description

Let $E$ and $F$ be seminormed groups, $j \colon E \to F$ be a monoid homomorphism, and $b \in \overline{j(\text{range}(j))}$ (the closure of the range of $j$ in $F$). Given a sequence of positive real numbers $(f_n)_{n \in \mathbb{N}}$, there exists a sequence $(a_n)_{n \in \mathbb{N}}$ in $E$ such that: 1. The product $\prod_{i=0}^n j(a_i)$ converges to $b$ as $n \to \infty$, 2. The norm $\|j(a_0) / b\| < f_0$, and 3. For all $n > 0$, $\|j(a_n)\| < f_n$.

tendsto_norm_nhdsNE_one theorem

: Tendsto (norm : E → ℝ) (𝓝[≠] 1) (𝓝[>] 0)

Full source

/-- See `tendsto_norm_one` for a version with full neighborhoods. -/
@[to_additive "See `tendsto_norm_zero` for a version with full neighborhoods."]
lemma tendsto_norm_nhdsNE_one : Tendsto (norm : E → ℝ) (𝓝[≠] 1) (𝓝[>] 0) :=
  tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _ hx ↦ norm_pos_iff'.2 hx

Limit of Norm at Identity: $\lim_{x \to 1^\neq} \|x\| = 0^+$

Informal description

The norm function $\|\cdot\|$ tends to $0^+$ (approaches 0 from above) as its argument tends to the identity element $1$ in a seminormed group $E$ while remaining distinct from $1$.

tendsto_norm_div_self_nhdsNE theorem

(a : E) : Tendsto (fun x => ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0)

Full source

@[to_additive]
theorem tendsto_norm_div_self_nhdsNE (a : E) : Tendsto (fun x => ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0) :=
  (tendsto_norm_div_self a).inf <|
    tendsto_principal_principal.2 fun _x hx => norm_pos_iff'.2 <| div_ne_one.2 hx

Limit of Normed Division Near Non-Identity: $\lim_{x \to a^\neq} \|x/a\| = 0^+$

Informal description

For any element $a$ in a normed group $E$, the function $x \mapsto \|x / a\|$ tends to $0^+$ (approaches 0 from above) as $x$ approaches $a$ while remaining distinct from $a$.

comap_norm_nhdsGT_zero' theorem

: comap norm (𝓝[>] 0) = 𝓝[≠] (1 : E)

Full source

/-- A version of `comap_norm_nhdsGT_zero` for a multiplicative normed group. -/
@[to_additive comap_norm_nhdsGT_zero]
lemma comap_norm_nhdsGT_zero' : comap norm (𝓝[>] 0) = 𝓝[≠] (1 : E) := by
  simp [nhdsWithin, comap_norm_nhds_one, Set.preimage, Set.compl_def]

Norm Preimage of Positive Zero Neighborhood Equals Punctured Identity Neighborhood

Informal description

The preimage of the neighborhood filter of positive real numbers under the norm function is equal to the punctured neighborhood filter of the identity element $1$ in the group $E$, i.e., $\text{comap}(\|\cdot\|, \mathcal{N}_{>0}(0)) = \mathcal{N}_{\neq}(1)$.

Tags