SearcharxivSearch

arXiv subjects

Weijie Lu

Publications and source records attributed to Weijie Lu.

8 recordsLinked to original sources

Differentiable normal linearization of partially hyperbolic dynamical systems

A result on $C^0$ linearization which is differentiable at the hyperbolic fixed point is known. In this paper, we further investigate a partially hyperbolic diffeomorphism $F$ to find a local $C^0$ conjugacy, which is $C^1$ on the center manifold, to linearize the hyperbolic component (normal to the center direction) and obtain its Takens' normal form. Our result is optimal, as it needs no non-resonant condition usually required for smooth conjugacy (e.g., as in the Takens' theorem) and the $C^{1,α}$ $(α>0)$ smoothness condition is sharp. For the proof, the center direction obstructs the decoupling of $F$ as the stable and unstable foliations do not intersect. We overcome this difficulty via a semi-decoupling method only with the unstable foliation, where a modified Lyapunov-Perron equation needs to be established along the center direction. Subsequent issues of cocycle reduction and differentiable linearization for an expansive fiber-preserving mapping are then addressed by the Whitney's extension theory and a lifting technique, respectively. In the local context, our result improves the result of $C^0$ normal linearization by [C. Pugh and M. Shub, Invent. Math., 10 (1970): 187-198] to a differentiable one.

math.DS

Array-Carrying Symbolic Execution for Function Contract Generation

Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in inter-procedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ACSL assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.

cs.PL

Pugh's global linearization for the nonautonomous unbounded system with $μ$-dichotomy via Lyapunov theory

The classical global linearization theorem for autonomous system given in [C. Pugh, Amer. J. Math., 91 (1969) 363-367] requires that nonlinear system with hyperbolicity satisfies boundedness and Lipschitz continuity.In this paper, we establish an {\em unbounded} global linearization theorem for nonautonomous systems subject to unbounded Lipschitz perturbations, under the assumption that the linear system admits a nonuniform $μ$-dichotomy (more general than classical exponential dichotomy). To this end, we first develop a comprehensive Lyapunov function framework for systems exhibiting nonuniform $μ$-dichotomy. Subsequently, we establish a characterization of nonuniform $μ$-dichotomy in terms of strict quadratic Lyapunov functions. Building upon these theoretical foundations, we then employ these Lyapunov functions to derive a linearization result under the nonuniform $μ$-dichotomy assumption. In the proof, we give a splitting lemma for nonuniform $μ$-dichotomy to decouple hyperbolic system into a contractive system and an expansive system. Then we construct a transformation to linearize contractive/expansive system, which is defined by the crossing time with respect to the unit sphere.

math.DS

Stable invariant manifold for generalized ODEs with applications to measure differential equations

This paper establishes the stable invariant manifold for a new kind of differential equations defined by Kurzweil integral, so-called {\em generalized ODEs} on a Banach space. The nonlinear generalized ODEs are formulated as $$ \frac{dz}{dτ}=D[Λ(t)z+F(z,t)], $$ where $Λ(t)$ is a bounded linear operator on a Banach space $\mathscr{Z}$ and $F(z,t)$ is a nonlinear Kurzweil integrable function on $\mathscr{Z}$. The letter $D$ represents that generalized ODEs are defined via its solution, and $\frac{dz}{dτ}$ only a notation. Hence, generalized ODEs are fundamentally a notational representation of a class of integral equations. Due to the differences between the theory of generalized ODEs and ODEs, it is difficult to extended the stable manifold theorem of ODEs to generalized ODEs. In order to overcome the difficulty, we establish a generalized Lyapunov-Perron equation in the frame of Kurzweil integral theory. Subsequently, we present a stable invariant manifold theorem for nonlinear generalized ODEs when their linear parts exhibit an exponential dichotomy. As effective applications, we finally derive results concerning the existence of stable manifold for measure differential equations and impulsive differential equations.

math.CA

Linearization and Hölder continuity of generalized ODEs with application to measure differential equations

In this paper, we study the topological conjugacy between the linear generalized ODEs (for short, GODEs) \[ \frac{dx}{dτ}=D[A(t)x] \] and their nonlinear perturbation \[ \frac{dx}{dτ}=D[A(t)x+F(x,t)] \] on Banach space $\mathscr{X}$, where $A:\mathbb{R}\to\mathscr{B}(\mathscr{X})$ is a bounded linear operator on $\mathscr{X}$ and $F:\mathscr{X}\times \mathbb{R}\to \mathscr{X}$ is Kurzweil integrable. GODEs are completely different from the classical ODEs. Note that the GODEs in Banach space are defined via its solution. $\frac{dx}{dτ}$ is only a notation and %$\frac{dx}{dτ}$ it does not indicate that the solution has a derivative. The solution of the GODEs can be discontinuous and even the number of discontinuous points is countable, so that many classical theorems and tools are no longer applicable to the GODEs. For instances, the chain rule and the multiplication rule of derivatives, differential mean value theorem, and integral mean value theorem are not valid for the GODEs. In this paper, we study the linearization and its Hölder continuity of the GODEs. Firstly, we construct the formula for bounded solutions of the nonlinear GODEs in the Kurzweil integral sense. Afterwards, we establish a Hartman-Grobman type linearization theorem which is a bridge connecting the linear GODEs with their nonlinear perturbations. Further, we show that the conjugacies are both Hölder continuous by using the Gronwall-type inequality (in the Perron-Stieltjes integral sense) and other nontrivial estimate techniques. %The GODEs include measure differential equations, impulsive differential equations, functional differential equations and the classical ordinary differential equations as special cases. Finally, applications to the measure differential equations and impulsive differential equations, our results are very effective.

math.CA

Sharpness of $C^0$ conjugacy for the non-autonomous differential equations with Lipschitzian perturbation

The classical $C^0$ linearization theorem for the non-autonomous differential equations states the existence of a $C^0$ topological conjugacy between the nonlinear system and its linear part. That is, there exists a homeomorphism (equivalent function) $H$ sending the solutions of the nonlinear system onto those of its linear part. It is proved in the previous literature that the equivalent function $H$ and its inverse $G=H^{-1}$ are both Hölder continuous if the nonlinear perturbation is Lipschitzian. Questions: is it possible to improve the regularity? Is the regularity sharp? To answer this question, we construct a counterexample to show that the equivalent function $H$ is exactly Lipschitzian, but the inverse $G=H^{-1}$ is merely Hölder continuous. Furthermore, we propose a conjecture that such regularity of the homeomorphisms is sharp (it could not be improved anymore). We prove that the conjecture is true for the systems with linear contraction. Furthermore, we present the special cases of linear perturbation, which are closely related to the spectrum.

math.CA

Higher regularity of homeomorphisms in the Hartman-Grobman theorem and a conjecture on its sharpness

Hartman-Grobman theorem states that there is a homeomorphism H sending the solutions of the nonlinear system onto those of its linearization under suitable assumptions. Many mathematicians have made contributions to prove Hölder continuity of the homeomorphisms. However, is it possible to improve the Hölder continuity to Lipschitzian continuity? This paper gives a positive answer. We formulate the first result that the homeomorphism is Lipschitzian, but not $C^1$, while its inverse is merely Hölder continuous, but not Lipschitzian. It is interesting that the regularity of the homeomorphism is different from its inverse. Moreover, some illustrative examples are presented to show the effectiveness of our results. Further, motivated by our example, we also propose a conjecture, saying, the regularity of the homeomorphisms is sharp and it could not be improved any more.

math.CA

Higher regularity of homeomorphisms in the Hartman-Grobman theorem for semilinear evolution equations

Hein and Prüss [J. Differential Equations, 261(2016)4709-4727] presented a version of Hartman-Grobman type $C^{0}$ linearization result for semilinear hyperbolic evolution equations. They showed that the linearising map (homomorphism) and its inverse are Hölder continuous. An important question: is it possible to improve the regularity of the homomorphisms? In the present paper, we prove that if the mild solutions of semilinear system are bounded, then the regularity of the homomorphisms is Lipchitzian, but the inverse is merely Hölder continuous. We also give a generalized local linearization result in this paper. Finally, some applications end the paper. As pointed out by Backes [J. Differential Equations, 297 (2021) 536-574], even if the diffeomorphism $F$ is $C^{\infty}$, the homomorphism can fail to be locally Lipschitz. The homomorphisms are in general only locally Hölder continuous. However, by establishing two effective dichotomy integral inequalities, we prove that the conjugacy is Lipchitzian, but the inverse is Hölder continuous. Our result is the first one to observe the higher regularity of homomorphisms in the Hartman-Grobman theorem.

math.CA