Tendsto f atTop (nhds L)

Stream: new members

[Hbz]

Is there a theorem in Lean4 regarding ∃ L : ℝ , Tendsto f atTop (nhds L) ↔ ∃ L, ∀ ε > 0, ∃ N, ∀ x > N, |f x - L| < ε, or a similar theorem? Or do I have to prove it manually?

[Kenny Lau]

@Hbz @loogle Filter.Tendsto _ Filter.atTop (nhds _) ↔ _

[loogle]

:search: tendsto_atTop_nhds, tendsto_const_mul_pow_nhds_iff, and 23 more

[Kenny Lau]

@loogle Filter.Tendsto _ Filter.atTop (nhds _) ↔ _, Norm.norm

[loogle]

:search: NormedAddCommGroup.tendsto_atTop, NormedAddCommGroup.tendsto_atTop', and 1 more

[Matt Diamond]

docs#Metric.tendsto_atTop / docs#Metric.tendsto_atTop' is close

[Matt Diamond]

actually I think that's exactly it

[Jireh Loreaux]

But to be honest, the right answer here is just to use filter bases and docs#Filter.HasBasis.tendsto_iff as the proof of the result Matt linked to does. That allows you to easily get lots of minor variations on the precise statement (e.g. if you wanted \le \eps instead at the end).

[Wuyang]

Looks like Metric.tendsto_atTop or its variants should match your need, and Filter.HasBasis.tendsto_iff gives flexibility for tweaks.

You can also try LeanFinder (www.leanfinder.org) to explore related limit theorems quickly.

[Wuyang]

@leanfinder limit theorem equivalence tendsto atTop nhds L epsilon N characterization in Lean4

[leanfinder]

Here’s what I found:

• theorem tendsto_atTop' : Tendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s := by simp only [tendsto_def, mem_atTop_sets, mem_preimage] "A function $f : \alpha \to \beta$ tends to the filter $l$ at infinity (i.e., as $x \to \infty$) if and only if for every set $s$ in the filter $l$, there exists a threshold $a \in \alpha$ such that for all $b \geq a$, the value $f(b)$ belongs to $s$." (score: 0.744)

• theorem Filter.tendsto_atTop' : Tendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s := by simp only [tendsto_def, mem_atTop_sets, mem_preimage] "A function $f : \alpha \to \beta$ tends to the filter $l$ at infinity (i.e., as $x \to \infty$) if and only if for every set $s$ in the filter $l$, there exists a threshold $a \in \alpha$ such that for all $b \geq a$, the value $f(b)$ belongs to $s$." (score: 0.744)

• theorem Metric.tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := (atTop_basis.tendsto_iff nhds_basis_ball).trans <| by simp only [true_and, mem_ball, mem_Ici] "Let $\alpha$ be a pseudo-metric space and $\beta$ be a nonempty join-semilattice. For a function $u : \beta \to \alpha$ and a point $a \in \alpha$, the function $u$ tends to $a$ as the argument tends to infinity (with respect to the order on $\beta$) if and only if for every $\varepsilon > 0$, there exists an index $N \in \beta$ such that for all $n \geq N$, the distance $\text{dist}(u(n), a) < \varepsilon$." (score: 0.736)

• theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε := (atTop_basis.tendsto_iff nhds_basis_eball).trans <| by simp only [exists_prop, true_and_iff, mem_Ici, mem_ball] "Let $\alpha$ be an extended pseudo-metric space and $\beta$ be a nonempty join-semilattice. For a function $u : \beta \to \alpha$ and a point $a \in \alpha$, the function $u$ tends to $a$ as $n$ approaches infinity if and only if for every $\varepsilon > 0$, there exists $N \in \beta$ such that for all $n \geq N$, the extended distance $\text{edist}(u(n), a) < \varepsilon$. This means that $u(n)$ gets arbitrarily close to $a$ as $n$ becomes large." (score: 0.734)

• theorem Metric.tendsto_atTop' [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : β → α} {a : α} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε := (atTop_basis_Ioi.tendsto_iff nhds_basis_ball).trans <| by simp only [true_and, gt_iff_lt, mem_Ioi, mem_ball] "Let $\alpha$ be a pseudo-metric space and $\beta$ be a nonempty directed set (specifically, a join-semilattice) with no maximal elements. For a function $u : \beta \to \alpha$ and a point $a \in \alpha$, the function $u$ tends to $a$ as the index tends to infinity if and only if for every $\varepsilon > 0$, there exists an index $N \in \beta$ such that for all $n > N$, the distance $\text{dist}(u(n), a) < \varepsilon$." (score: 0.732)

• theorem tendsto_atTop_nhds [Nonempty α] [SemilatticeSup α] {f : α → X} : Tendsto f atTop (𝓝 x) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U := (atTop_basis.tendsto_iff (nhds_basis_opens x)).trans <| by simp only [and_imp, exists_prop, true_and, mem_Ici] "Let $\alpha$ be a nonempty join-semilattice and $X$ a topological space. For a function $f \colon \alpha \to X$, the following are equivalent:

1. The function $f$ tends to the neighborhood filter $\mathcal{N}(x)$ along the filter atTop (i.e., $\lim_{i \to \infty} f(i) = x$ in the order topology).
2. For every open neighborhood $U$ of $x$ in $X$, there exists an index $N \in \alpha$ such that for all $n \geq N$, we have $f(n) \in U$." (score: 0.726)

• theorem tendsto_atTop_nhds [Nonempty α] [SemilatticeSup α] {f : α → X} : Tendsto f atTop (𝓝 x) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U := (atTop_basis.tendsto_iff (nhds_basis_opens x)).trans <| by simp only [and_imp, exists_prop, true_and, mem_Ici] "Let $\alpha$ be a nonempty join-semilattice and $X$ a topological space. For a function $f \colon \alpha \to X$, the following are equivalent:

1. The function $f$ tends to the neighborhood filter $\mathcal{N}(x)$ along the filter atTop (i.e., $\lim_{i \to \infty} f(i) = x$ in the order topology).
2. For every open neighborhood $U$ of $x$ in $X$, there exists an index $N \in \alpha$ such that for all $n \geq N$, we have $f(n) \in U$." (score: 0.726)

• theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞) : Tendsto f atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε) := .trans (atTop_basis.tendsto_iff (hasBasis_nhds_of_ne_top ha)) (by simp only [true_and]; rfl) "Let $\beta$ be a nonempty join-semilattice and $f : \beta \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ be a function. For any finite extended non-negative real number $a \neq \infty$, the function $f$ tends to $a$ as $n$ approaches infinity if and only if for every $\varepsilon > 0$, there exists $N \in \beta$ such that for all $n \geq N$, the value $f(n)$ lies in the closed interval $[a - \varepsilon, a + \varepsilon]$." (score: 0.726)

• theorem EMetric.tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε := (atTop_basis.tendsto_iff nhds_basis_eball).trans <| by simp only [exists_prop, true_and, mem_Ici, mem_ball] "Let $\alpha$ be an extended pseudo-metric space and $\beta$ be a nonempty join-semilattice. For a function $u : \beta \to \alpha$ and a point $a \in \alpha$, the function $u$ tends to $a$ along the filter atTop if and only if for every $\varepsilon > 0$, there exists $N \in \beta$ such that for all $n \geq N$, the extended distance satisfies $\text{edist}(u(n), a) < \varepsilon$." (score: 0.724)

• theorem ENNReal.tendsto_atTop [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞) : Tendsto f atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε) := .trans (atTop_basis.tendsto_iff (hasBasis_nhds_of_ne_top ha)) (by simp only [true_and]; rfl) "Let $\beta$ be a nonempty join-semilattice and $f : \beta \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ be a function. For any finite extended non-negative real number $a \neq \infty$, the function $f$ tends to $a$ along the filter at infinity if and only if for every $\varepsilon > 0$, there exists $N \in \beta$ such that for all $n \geq N$, the value $f(n)$ lies in the closed interval $[a - \varepsilon, a + \varepsilon]$." (score: 0.723)