About Quotient Orders and Ordering Sequences

Summary In preparation for the formalization in Mizar [4] of lotteries as given in [14], this article closes some gaps in the Mizar Mathematical Library (MML) regarding relational structures. The quotient order is introduced by the equivalence relation identifying two elements x, y of a preorder as equivalent if x ⩽ y and y ⩽ x. This concept is known (see e.g. chapter 5 of [19]) and was first introduced into the MML in [13] and that work is incorporated here. Furthermore given a set A, partition D of A and a finite-support function f : A → ℝ, a function Σf : D → ℝ, Σf (X)= ∑x∈X f(x) can be defined as some kind of natural “restriction” from f to D. The first main result of this article can then be formulated as: $$\sum\limits_{x \in A} {f(x)} = \sum\limits_{X \in D} {\Sigma _f (X)\left( { = \sum\limits_{X \in D} {\sum\limits_{x \in X} {f(x)} } } \right)} $$ After that (weakly) ascending/descending finite sequences (based on [3]) are introduced, in analogous notation to their infinite counterparts introduced in [18] and [13]. The second main result is that any finite subset of any transitive connected relational structure can be sorted as a ascending or descending finite sequence, thus generalizing the results from [16], where finite sequence of real numbers were sorted. The third main result of the article is that any weakly ascending/weakly descending finite sequence on elements of a preorder induces a weakly ascending/weakly descending finite sequence on the projection of these elements into the quotient order. Furthermore, weakly ascending finite sequences can be interpreted as directed walks in a directed graph, when the set of edges is described by ordered pairs of vertices, which is quite common (see e.g. [10]). Additionally, some auxiliary theorems are provided, e.g. two schemes to find the smallest or the largest element in a finite subset of a connected transitive relational structure with a given property and a lemma I found rather useful: Given two finite one-to-one sequences s, t on a set X, such that rng t ⊆ rng s, and a function f : X → ℝ such that f is zero for every x ∈ rng s \ rng t, we have ∑ f o s = ∑ f o t.

Weakly directed self-avoiding walks

International audience We define a new family of self-avoiding walks (SAW) on the square lattice, called $\textit{weakly directed walks}$. These walks have a simple characterization in terms of the irreducible bridges that compose them. We determine their generating function. This series has a complex singularity structure and in particular, is not D-finite. The growth constant is approximately 2.54 and is thus larger than that of all natural families of SAW enumerated so far (but smaller than that of general SAW, which is about 2.64). We also prove that the end-to-end distance of weakly directed walks grows linearly. Finally, we study a diagonal variant of this model. Nous définissons une nouvelle famille de chemins auto-évitants (CAE) sur le réseau carré, appelés $\textit{chemins faiblement dirigés}$. Ces chemins ont une caractérisation simple en termes des ponts irréductibles qui les composent. Nous déterminons leur série génératrice. Cette série a une structure de singularité complexe et n'est en particulier pas D-finie. La constante de croissance est environ 2,54, ce qui est supérieur à toutes les familles naturelles de SAW étudiées jusqu'à présent, mais inférieur aux CAE généraux (dont la constante est environ 2,64). Nous prouvons également que la distance moyenne entre les extrémités du chemin croît linéairement. Enfin, nous étudions une variante diagonale du modèle.