Diagonal indices and floor cutoffs along atTop

If for every k a property P k n holds for all large n, then an index κ n tending to infinity can be chosen so slowly that P (κ n) n holds for all large n (TauCeti.exists_tendsto_atTop_of_forall_eventually). This is the diagonal step of constructions that must meet countably many eventual requirements at once with a single sequence, such as a recovery sequence built from a countable neighbourhood basis. It complements Mathlib's Filter.extraction_forall_of_eventually, which meets the requirements along a subsequence instead.

The second statement is the diagonal extraction of a subsequence along which countably many sequences converge at once (TauCeti.extraction_forall_exists_tendsto): if every subsequence of each of the sequences x j has a convergent further subsequence, a single subsequence makes all of them converge. It is the compactness step of the Arzelà–Ascoli theorem.

Finally, a sequence converges along atTop exactly when it does so along real (or other floor semiring) cutoffs x ↦ u ⌊x⌋₊ (TauCeti.tendsto_comp_natFloor_iff). This compares limits of partial sums ∑ n ≤ x taken over real and over natural cutoffs. More generally, a reindexing g : ℕ → ℕ that tends to infinity and eventually never increases by more than one at a time takes every large value, so map g atTop = atTop (TauCeti.map_atTop_eq_of_le_add_one) and u ∘ g converges exactly when u does (TauCeti.tendsto_comp_iff_of_le_add_one). For instance, a partial product over the primes p ≤ n is a function of the prime count π n, which moves in steps of at most one.

In a ring of characteristic zero without zero divisors, a + k * b vanishes for all large natural numbers k exactly when a = b = 0, and otherwise it is nonzero for all large k (TauCeti.eventually_add_mul_eq_zero_iff): it vanishes for at most one k unless b = 0.

theorem TauCeti.exists_tendsto_atTop_of_forall_eventually {P : ℕ → ℕ → Prop} (h : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, P k n) : ∃ (κ : ℕ → ℕ), Filter.Tendsto κ Filter.atTop Filter.atTop ∧ ∀ᶠ (n : ℕ) in Filter.atTop, P (κ n) n

If for every k the property P k n holds for all large n, then there is an index κ n tending to infinity with P (κ n) n for all large n.

theorem TauCeti.extraction_forall_exists_tendsto {X : Type u_1} {l : X → Filter X} {x : ℕ → ℕ → X} (h : ∀ (j : ℕ) (ψ : ℕ → ℕ), StrictMono ψ → ∃ (y : X) (ψ' : ℕ → ℕ), StrictMono ψ' ∧ Filter.Tendsto (fun (n : ℕ) => x j (ψ (ψ' n))) Filter.atTop (l y)) : ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∀ (j : ℕ), ∃ (y : X), Filter.Tendsto (fun (n : ℕ) => x j (ψ n)) Filter.atTop (l y)

Diagonal extraction. Let x j : ℕ → X be countably many sequences and l y the filter of a convergence to y on X. If every subsequence of every x j has a further subsequence converging to some point, then one subsequence makes every x j converge.

theorem TauCeti.tendsto_comp_natFloor_iff {R : Type u_1} {X : Type u_2} [Semiring R] [LinearOrder R] [FloorSemiring R] {u : ℕ → X} {l : Filter X} : Filter.Tendsto (fun (x : R) => u ⌊x⌋₊) Filter.atTop l ↔ Filter.Tendsto u Filter.atTop l

A sequence u converges along atTop if and only if its values u ⌊x⌋₊ at the natural floors of x converge as x → ∞ in a floor semiring such as ℝ.

theorem TauCeti.map_atTop_eq_of_le_add_one {g : ℕ → ℕ} (hg : Filter.Tendsto g Filter.atTop Filter.atTop) (hle : ∀ᶠ (n : ℕ) in Filter.atTop, g (n + 1) ≤ g n + 1) : Filter.map g Filter.atTop = Filter.atTop

A map g : ℕ → ℕ that tends to infinity and eventually increases by at most one at each step takes every large value, so it pushes atTop forward to atTop.

theorem TauCeti.tendsto_comp_iff_of_le_add_one {X : Type u_1} {g : ℕ → ℕ} (hg : Filter.Tendsto g Filter.atTop Filter.atTop) (hle : ∀ᶠ (n : ℕ) in Filter.atTop, g (n + 1) ≤ g n + 1) {u : ℕ → X} {l : Filter X} : Filter.Tendsto (u ∘ g) Filter.atTop l ↔ Filter.Tendsto u Filter.atTop l

If g : ℕ → ℕ tends to infinity and eventually increases by at most one at each step, then u ∘ g converges along atTop exactly when u does.

theorem TauCeti.eventually_add_mul_eq_zero_iff {R : Type u_1} [Ring R] [NoZeroDivisors R] [CharZero R] (a b : R) : ∀ᶠ (k : ℕ) in Filter.atTop, a + ↑k * b = 0 ↔ a = 0 ∧ b = 0

In a ring of characteristic zero without zero divisors, a + k * b vanishes for all large natural numbers k exactly when a = b = 0, and otherwise it is nonzero for all large k.