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.

Toward a Difference Approach: A Discrete Meat Demand System

While the differential approach to economic analysis is useful, the difference approach is indispensable as almost all economic data are discrete, rather than continuous. Thus, we must to investigate the integration of the differential with difference approaches. We show a difference quotient corresponding to a differential quotient, which is generally called a derivative, and a partial difference quotient corresponding to a partial differential quotient, which is generally called a partial derivative. From these, the difference approach produces a discrete demand system with logarithmic mean elasticities as parameters that corresponds to a continuous demand system with point elasticities as parameters produced by the differential approach. These systems should satisfy each budget constraint: the former for finite-change variables and the latter for infinitesimal-change variables. Based on these, we consider a discrete meat demand system, apply it to monthly demand for fresh meat in Japan, and estimate it using a weighted RAS method. The estimated demand system has two desirable properties: each estimated demand (theoretical value) of the conditional demand function coincides with each observed demand, and this system satisfies the difference budget constraint.

The math modeling research of constant temperature bath

This paper studies how the temperature in the bathroom keeps changing when people bathe in the bathtub. The shape, capacity, behavior and body posture of people in the bathroom are considered. In fluid mechanics point of view, we consider the impact of the flow of heat transfer, by the energy differential equations and boundary-layer momentum to establish a set of PDE, and use Laplace operator rewrite it. We use finite difference method, with Taylor series expansion. We use the function value of grid nodes of difference quotient instead of control equation of derivative, and discretize it, and solve the heat conduction equation.

Characterization of generalized Orlicz spaces

The norm in classical Sobolev spaces can be expressed as a difference quotient. This expression can be used to generalize the space to the fractional smoothness case. Because the difference quotient is based on shifting the function, it cannot be used in generalized Orlicz spaces. In its place, we introduce a smoothed difference quotient and show that it can be used to characterize the generalized Orlicz–Sobolev space. Our results are new even in Orlicz spaces and variable exponent spaces.

Characterization of the variable exponent Sobolev norm without derivatives

The norm in classical Sobolev spaces can be expressed as a difference quotient. This expression can be used to generalize the space to the fractional smoothness case. Since the difference quotient is based on shifting the function, it cannot be generalized to the variable exponent case. In its place, we introduce a smoothed difference quotient and show that it can be used to characterize the variable exponent Sobolev space.