In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].
In this article, we formalize the differentiability of functions from the set of real numbers into a normed vector space [14].
In this article, we formalize differentiability of functions on normed linear spaces. Partial derivative, mean value theorem for vector-valued functions, continuous differentiability, etc. are formalized. As it is well known, there is no exact analog of the mean value theorem for vector-valued functions. However a certain type of generalization of the mean value theorem for vector-valued functions is obtained as follows: If ||ƒ'(x + t · h)|| is bounded for t between 0 and 1 by some constant M, then...
Let F be a polynomial mapping of ℝ², F(O) = 0. In 1987 Meisters and Olech proved that the solution y(·) = 0 of the autonomous system of differential equations ẏ = F(y) is globally asymptotically stable provided that the jacobian of F is everywhere positive and the trace of the matrix of the differential of F is everywhere negative. In particular, the mapping F is then injective. We give an n-dimensional generalization of this result.
In this paper we consider the nonlocal (nonstandard) Cauchy problem for differential inclusions in Banach spaces x'(t) ∈ F(t,x(t)), x(0)=g(x), t ∈ [0,T] = I. Investigation over some multivalued integrals allow us to prove the existence of solutions for considered problem. We concentrate on the problems for which the assumptions are expressed in terms of the weak topology in a Banach space. We recall and improve earlier papers of this type. The paper is complemented...
We study Lebesgue points for Sobolev functions over other collections of sets than balls. Our main result gives several conditions for a differentiation basis, which characterize the existence of Lebesgue points outside a set of capacity zero.
The main result of this paper is that if f is n-convex on a measurable subset E of ℝ, then f is n-2 times differentiable, n-2 times Peano differentiable and the corresponding derivatives are equal, and except on a countable set. Moreover is approximately differentiable with approximate derivative equal to the nth approximate Peano derivative of f almost everywhere.
In this article, we define and develop differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [16] and [17]).
We investigate the connection between certain logarithmic Sobolev inequalities and generalizations of Gagliardo-Nirenberg inequalities. A similar connection holds between reverse logarithmic Sobolev inequalities and a new class of reverse Gagliardo-Nirenberg inequalities.