DSpace Kolekcja: http://hdl.handle.net/11320/6274 2020-11-29T22:27:01Z Dual Lattice of ℤ-module Lattice http://hdl.handle.net/11320/6283 Tytu&#322;: Dual Lattice of ℤ-module Lattice Autorzy: Futa, Yuichi; Shidama, Yasunari Abstrakt: SummaryIn this article, we formalize in Mizar  the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice ,  and . 2017-01-01T00:00:00Z Basel Problem http://hdl.handle.net/11320/6282 Tytu&#322;: Basel Problem Autorzy: Pąk, Karol; Korniłowicz, Artur Abstrakt: SummaryA rigorous elementary proof of the Basel problem [6, 1] ∑n=1∞1n2=π26 is formalized in the Mizar system . This theorem is item #14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. 2017-01-01T00:00:00Z About Quotient Orders and Ordering Sequences http://hdl.handle.net/11320/6280 Tytu&#322;: About Quotient Orders and Ordering Sequences Autorzy: Koch, Sebastian Abstrakt: SummaryIn preparation for the formalization in Mizar  of lotteries as given in , 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 ) and was first introduced into the MML in  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: ∑x∈Af(x)=∑X∈DΣf(X)(=∑X∈D∑x∈Xf(x)) After that (weakly) ascending/descending finite sequences (based on ) are introduced, in analogous notation to their infinite counterparts introduced in  and .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 , 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. ).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. 2017-01-01T00:00:00Z Basel Problem – Preliminaries http://hdl.handle.net/11320/6281 Tytu&#322;: Basel Problem – Preliminaries Autorzy: Korniłowicz, Artur; Pąk, Karol Abstrakt: SummaryIn the article we formalize in the Mizar system  preliminary facts needed to prove the Basel problem [7, 1]. Facts that are independent from the notion of structure are included here. 2017-01-01T00:00:00Z