Browse

You are looking at 1 - 10 of 724 items for :

  • Numerical and Computational Mathematics x
Clear All
Open access

Roland Coghetto and Adam Grabowski

Summary

In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.

We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST).

Open access

Sora Otsuki, Pauline N. Kawamoto and Hiroshi Yamazaki

Summary

In this article, we formalized in Mizar [4], [1] simple partial differential equations. In the first section, we formalized partial differentiability and partial derivative. The next section contains the method of separation of variables for one-dimensional wave equation. In the last section, we formalized the superposition principle.We referred to [6], [3], [5] and [9] in this formalization.

Open access

Kazuhisa Nakasho

Summary

In the first chapter, the notion of multilinear operator on real linear spaces is discussed. The algebraic structure [2] of multilinear operators is introduced here. In the second chapter, the results of the first chapter are extended to the case of the normed spaces. This chapter shows that bounded multilinear operators on normed linear spaces constitute the algebraic structure. We referred to [3], [7], [5], [6] in this formalization.

Open access

Hiroyuki Okazaki, Koh-ichi Nagao and Yuichi Futa

Summary

In this article we formalize in Mizar [1], [2] the maximum number of steps taken by some number theoretical algorithms, “right–to–left binary algorithm” for modular exponentiation and “Euclidean algorithm” [5]. For any natural numbers a, b, n, “right–to–left binary algorithm” can calculate the natural number, see (Def. 2), AlgoBPow(a, n, m) := ab mod n and for any integers a, b, “Euclidean algorithm” can calculate the non negative integer gcd(a, b). We have not formalized computational complexity of algorithms yet, though we had already formalize the “Euclidean algorithm” in [7].

For “right-to-left binary algorithm”, we formalize the theorem, which says that the required number of the modular squares and modular products in this algorithms are ⌊1+log2 n⌋ and for “Euclidean algorithm”, we formalize the Lamé’s theorem [6], which says the required number of the divisions in this algorithm is at most 5 log10 min(|a|, |b|). Our aim is to support the implementation of number theoretic tools and evaluating computational complexities of algorithms to prove the security of cryptographic systems.

Open access

Noboru Endou

Summary

Fubini theorem is an essential tool for the analysis of high-dimensional space [8], [2], [3], a theorem about the multiple integral and iterated integral. The author has been working on formalizing Fubini’s theorem over the past few years [4], [6] in the Mizar system [7], [1]. As a result, Fubini’s theorem (30) was proved in complete form by this article.

Open access

Roland Coghetto

Summary

Using Mizar [1], in the context of a real vector space, we introduce the concept of affine ratio of three aligned points (see [5]).

It is also equivalent to the notion of “Mesure algèbrique”1, to the opposite of the notion of Teilverhältnis2 or to the opposite of the ordered length-ratio [9].

In the second part, we introduce the classic notion of “cross-ratio” of 4 points aligned in a real vector space.

Finally, we show that if the real vector space is the real line, the notion corresponds to the classical notion3 [9]:

The cross-ratio of a quadruple of distinct points on the real line with coordinates x 1, x 2, x 3, x 4 is given by:

(x1,x2;x3,x4)=x3-x1x3-x2.x4-x2x4-x1

In the Mizar Mathematical Library, the vector spaces were first defined by Kusak, Leonczuk and Muzalewski in the article [6], while the actual real vector space was defined by Trybulec [10] and the complex vector space was defined by Endou [4]. Nakasho and Shidama have developed a solution to explore the notions introduced by different authors4 [7]. The definitions can be directly linked in the HTMLized version of the Mizar library5.

The study of the cross-ratio will continue within the framework of the Klein- Beltrami model [2], [3]. For a generalized cross-ratio, see Papadopoulos [8].

Open access

Kazuhisa Nakasho and Yasunari Shidama

Summary

In this article, various definitions of contuity of multilinear operators on normed linear spaces are discussed in the Mizar formalism [4], [1] and [2]. In the first chapter, several basic theorems are prepared to handle the norm of the multilinear operator, and then it is formalized that the linear space of bounded multilinear operators is a complete Banach space.

In the last chapter, the continuity of the multilinear operator on finite normed spaces is addressed. Especially, it is formalized that the continuity at the origin can be extended to the continuity at every point in its whole domain. We referred to [5], [11], [8], [9] in this formalization.

Open access

Rafał Ziobro

Summary

The coexistence of “classical” finite sequences [1] and their zero-based equivalents finite 0-sequences [6] in Mizar has been regarded as a disadvantage. However the suggested replacement of the former type with the latter [5] has not yet been implemented, despite of several advantages of this form, such as the identity of length and domain operators [4]. On the other hand the number of theorems formalized using finite sequence notation is much larger then of those based on finite 0-sequences, so such translation would require quite an effort.

The paper addresses this problem with another solution, using the Mizar system [3], [2]. Instead of removing one notation it is possible to introduce operators which would concatenate sequences of various types, and in this way allow utilization of the whole range of formalized theorems. While the operation could replace existing FS2XFS, XFS2FS commands (by using empty sequences as initial elements) its universal notation (independent on sequences that are concatenated to the initial object) allows to “forget” about the type of sequences that are concatenated on further positions, and thus simplify the proofs.

Open access

Kazuhisa Nakasho

Summary

The main aim of this article is proving properties of bilinear operators on normed linear spaces formalized by means of Mizar [1]. In the first two chapters, algebraic structures [3] of bilinear operators on linear spaces are discussed. Especially, the space of bounded bilinear operators on normed linear spaces is developed here. In the third chapter, it is remarked that the algebraic structure of bounded bilinear operators to a certain Banach space also constitutes a Banach space.

In the last chapter, the correspondence between the space of bilinear operators and the space of composition of linear opearators is shown. We referred to [4], [11], [2], [7] and [8] in this formalization.

Open access

Orazio Muscato and Vincenza Di Stefano

Abstract

The Wigner transport equation can be solved stochastically by Monte Carlo techniques based on the theory of piecewise deterministic Markov processes. A new stochastic algorithm, without time discretization error, has been implemented and studied in the case of the quantum transport through a rectangular potential barrier.