Formalizing Calculus without Limit Theory in Coq

Formal verification of mathematical theory has received widespread concern and grown rapidly. The formalization of the fundamental theory will contribute to the development of large projects. In this paper, we present the formalization in Coq of calculus without limit theory. The theory aims to found a new form of calculus more easily but rigorously. This theory as an innovation differs from traditional calculus but is equivalent and more comprehensible. First, the definition of the difference-quotient control function is given intuitively from the physical facts. Further, conditions are added to it to get the derivative, and define the integral by the axiomatization. Then some important conclusions in calculus such as the Newton–Leibniz formula and the Taylor formula can be formally verified. This shows that this theory can be independent of limit theory, and any proof does not involve real number completeness. This work can help learners to study calculus and lay the foundation for many applications.

Derivation of Commutative Rings and the Leibniz Formula for Power of Derivation

Summary In this article we formalize in Mizar [1], [2] a derivation of commutative rings, its definition and some properties. The details are to be referred to [5], [7]. A derivation of a ring, say D, is defined generally as a map from a commutative ring A to A-Module M with specific conditions. However we start with simpler case, namely dom D = rng D. This allows to define a derivation in other rings such as a polynomial ring. A derivation is a map D : A → A satisfying the following conditions: (i) D(x + y) = Dx + Dy, (ii) D(xy) = xDy + yDx, ∀x, y ∈ A. Typical properties are formalized such as: D ( ∑ i = 1 n x i ) = ∑ i = 1 n D x i D\left( {\sum\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {D{x_i}} and D ( ∏ i = 1 n x i ) = ∑ i = 1 n x 1 x 2 ⋯ D x i ⋯ x n ( ∀ x i ∈ A ) . D\left( {\prod\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {{x_1}{x_2} \cdots D{x_i} \cdots {x_n}} \left( {\forall {x_i} \in A} \right). We also formalized the Leibniz Formula for power of derivation D : D n ( x y ) = ∑ i = 0 n ( i n ) D i x D n - i y . {D^n}\left( {xy} \right) = \sum\limits_{i = 0}^n {\left( {_i^n} \right){D^i}x{D^{n - i}}y.} Lastly applying the definition to the polynomial ring of A and a derivation of polynomial ring was formalized. We mentioned a justification about compatibility of the derivation in this article to the same object that has treated as differentiations of polynomial functions [3].

Some Theorems on Leibniz n-Algebras from the Category Un (Lb)

We study the Leibniz [Formula: see text]-algebra [Formula: see text], whose multiplication is defined via the bracket of a Leibniz algebra [Formula: see text] as [Formula: see text]. We show that [Formula: see text] is simple if and only if [Formula: see text] is a simple Lie algebra. An analog of Levi's theorem for Leibniz algebras in [Formula: see text] is established and it is proven that the Leibniz [Formula: see text]-kernel of [Formula: see text] for any semisimple Leibniz algebra [Formula: see text] is the [Formula: see text]-algebra [Formula: see text].

"Efficiency Comparison of Algorithms for Finding Determinants Via Permutations "

"Determiners have been used extensively in a selection of applications throughout history. It also biased many areas of mathematics such as linear algebra. There are algorithms commonly used for computing a matrix determinant such as: Laplace expansion, LDU decomposition, Cofactor algorithm, and permutation algorithms. The determinants of a quadratic matrix can be found using a diversity of these methods, including the well-known methods of the Leibniz formula and the Laplace expansion and permutation algorithms that computes the determinant of any n×n matrix in O(n!). In this paper, we first discuss three algorithms for finding determinants using permutations. Then we make out the algorithms in pseudo code and finally, we analyze the complexity and nature of the algorithms and compare them with each other. We present permutations algorithms and then analyze and compare them in terms of runtime, acceleration and competence, as the presented algorithms presented different results.

A New Approach for Exponential Stability Criteria of New Certain Nonlinear Neutral Differential Equations with Mixed Time-Varying Delays

This work is concerned with the delay-dependent criteria for exponential stability analysis of neutral differential equation with a more generally interval-distributed and discrete time-varying delays. By using a novel Lyapunov–Krasovkii functional, descriptor model transformation, utilization of the Newton–Leibniz formula, and the zero equation, the criteria for exponential stability are in the form of linear matrix inequalities (LMIs). Finally, we present the effectiveness of the theoretical results in numerical examples to show less conservative conditions than the others in the literature.

The Discrete Analog of the Newton-Leibniz Formula in the Problem of Summation over Simplex Lattice Points

Definition of the discrete primitive function is introduced in the problem of summation over simplex lattice points. The discrete analog of the Newton-Leibniz formula is found

Some Leibniz bimodules of 𝔰𝔩2

We study complex finite-dimensional Leibniz algebra bimodule over [Formula: see text] that as a Lie algebra module is split into a direct sum of two simple [Formula: see text]-modules. We prove that in this case there are only two nonsplit Leibniz [Formula: see text]-bimodules and we describe the actions.

Pinning Synchronization for Complex Networks with Interval Coupling Delay by Variable Subintervals Method and Finsler’s Lemma

The pinning synchronous problem for complex networks with interval delays is studied in this paper. First, by using an inequality which is introduced from Newton-Leibniz formula, a new synchronization criterion is derived. Second, combining Finsler’s Lemma with homogenous matrix, convergent linear matrix inequality (LMI) relaxations for synchronization analysis are proposed with matrix-valued coefficients. Third, a new variable subintervals method is applied to expand the obtained results. Different from previous results, the interval delays are divided into some subdelays, which can introduce more free weighting matrices. Fourth, the results are shown as LMI, which can be easily analyzed or tested. Finally, the stability of the networks is proved via Lyapunov’s stability theorem, and the simulation of the trajectory claims the practicality of the proposed pinning control.