Double Sequences and Iterated Limits in Regular Space

First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space. Endou, Okazaki and Shidama formalized in [14] the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence converges in “Pringsheim’s sense” but not in Frechet filter on ℕ × ℕ sense. In the next section, we generalize some definitions: “is convergent in the first coordinate”, “is convergent in the second coordinate”, “the lim in the first coordinate of”, “the lim in the second coordinate of” according to [14], in Hausdorff space. Finally, we generalize two theorems: (3) and (4) from [14] in the case of double sequences and we formalize the “iterated limit” theorem (“Double limit” [7], p. 81, par. 8.5 “Double limite” [6] (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5) [17] and the corrections B.10 [18].

Summability of double sequences by weighted mean methods and Tauberian conditions for convergence in Pringsheim's sense

After a brief summary of Tauberian conditions for ordinary sequences of numbers, we consider summability of double sequences of real or complex numbers by weighted mean methods which are not necessarily products of related weighted mean methods in one variable. Our goal is to obtain Tauberian conditions under which convergence of a double sequence follows from its summability, where convergence is understood in Pringsheim's sense. In the case of double sequences of real numbers, we present necessary and sufficient Tauberian conditions, which are so-called one-sided conditions. Corollaries allow these Tauberian conditions to be replaced by Schmidt-type slow decrease conditions. For double sequences of complex numbers, we present necessary and sufficient so-called two-sided Tauberian conditions. In particular, these conditions are satisfied if the summable double sequence is slowly oscillating.