Reversible equivariant Hopf bifurcation

In this paper we study codimension-one Hopf bifurcation from symmetric equilibrium points in reversible equivariant vector fields. Such bifurcations are characterized by a doubly degenerate pair of purely imaginary eigenvalues of the linearization of the vector field at the equilibrium point. The eigenvalue movements near such a degeneracy typically follow one of three scenarios: splitting (from two pairs of imaginary eigenvalues to a quadruplet on the complex plane), passing (on the imaginary axis), or crossing (a quadruplet crossing the imaginary axis). We give a complete description of the behaviour of reversible periodic orbits in the vicinity of such a bifurcation point. For non-reversible periodic solutions. in the case of Hopf bifurcation with crossing eigenvalues. we obtain a generalization of the equivariant Hopf Theorem.

Invex nonsmooth alternative theorem and applications

An invex constrained nonsmooth optimization problem is considered, in which the presence of an abstract constraint set is possibly allowed. Necessary and sufficient conditions of optimality are provided and weak and strong duality results established. Following Geoffrion's approach an invex nonsmooth alternative theorem of Gordan type is then derived. Subsequently, some applications on multiobjective programming are then pursued. © 2000 OPA (Overseas Publishers Association) N.V. Published by license under the Gordon and Breach Science Publishers imprint.

Landau and Kolmogoroff type polynomial inequalities II

Let 0 < j < m ≤ n. Kolmogoroff type inequalities of the form ∥f(j)∥2 ≤ A∥f(m)∥ 2 + B∥f∥2 which hold for algebraic polynomials of degree n are established. Here the norm is defined by ∫ f2(x)dμ(x), where dμ(x) is any distribution associated with the Jacobi, Laguerre or Bessel orthogonal polynomials. In particular we characterize completely the positive constants A and B, for which the Landau weighted polynomial inequalities ∥f′∥ 2 ≤ A∥f″∥2 + B∥f∥ 2 hold. © Dynamic Publishers, Inc.

A note on non-degenerate umbilics and the path formulation for bifurcation problems

Path formulation can be used to classify and structure efficiently multiparameter bifurcation problems around fundamental singularities: the cores. The non-degenerate umbilic singularities are the generic cores for four situations in corank 2: the general or gradient problems and the ℤ 2-equivariant (general or gradient) problems. Those categories determine an interesting 'Russian doll' type of structure in the universal unfoldings of the umbilic singularities. One advantage of our approach is that we can handle one, two or more parameters using the same framework (even considering some special parameter structure, for instance, some internal hierarchy). We classify the generic bifurcations that occur in those cases with one or two parameters.

Estabilidade global e bifurcação de Hopf em um modelo de HIV baseado em sistemas do tipo Lotka-Volterra

Pós-graduação em Matematica Aplicada e Computacional - FCT

Fourier series for quaternions and the square of the error theorem

In this paper we introduce a type of Hypercomplex Fourier Series based on Quaternions, and discuss on a Hypercomplex version of the Square of the Error Theorem. Since their discovery by Hamilton (Sinegre [1]), quaternions have provided beautifully insights either on the structure of different areas of Mathematics or in the connections of Mathematics with other fields. For instance: I) Pauli spin matrices used in Physics can be easily explained through quaternions analysis (Lan [2]); II) Fundamental theorem of Algebra (Eilenberg [3]), which asserts that the polynomial analysis in quaternions maps into itself the four dimensional sphere of all real quaternions, with the point infinity added, and the degree of this map is n. Motivated on earlier works by two of us on Power Series (Pendeza et al. [4]), and in a recent paper on Liouville’s Theorem (Borges and Mar˜o [5]), we obtain an Hypercomplex version of the Fourier Series, which hopefully can be used for the treatment of hypergeometric partial differential equations such as the dumped harmonic oscillation.

On bifurcation of solutions of the Yamabe problem in product manifolds

We study local rigidity and multiplicity of constant scalar curvature metrics in arbitrary products of compact manifolds. Using (equivariant) bifurcation theory we determine the existence of infinitely many metrics that are accumulation points of pairwise non-homothetic solutions of the Yamabe problem. Using local rigidity and some compactness results for solutions of the Yamabe problem, we also exhibit new examples of conformal classes (with positive Yamabe constant) for which uniqueness holds. (C) 2011 Elsevier Masson SAS. All rights reserved.

Kleiner's theorem for unitary representations of posets

A subspace representation of a poset S = {s(1), ..., S-t} is given by a system (V; V-1, ..., V-t) consisting of a vector space V and its sub-spaces V-i such that V-i subset of V-j if s(i) (sic) S-j. For each real-valued vector chi = (chi(1), ..., chi(t)) with positive components, we define a unitary chi-representation of S as a system (U: U-1, ..., U-t) that consists of a unitary space U and its subspaces U-i such that U-i subset of U-j if S-i (sic) S-j and satisfies chi 1 P-1 + ... + chi P-t(t) = 1, in which P-i is the orthogonal projection onto U-i. We prove that S has a finite number of unitarily nonequivalent indecomposable chi-representations for each weight chi if and only if S has a finite number of nonequivalent indecomposable subspace representations; that is, if and only if S contains any of Kleiner's critical posets. (c) 2012 Elsevier Inc. All rights reserved.

TYPE-ZERO SADDLE-NODE BIFURCATIONS AND STABILITY REGION ESTIMATION OF NONLINEAR AUTONOMOUS DYNAMICAL SYSTEMS

A complete characterization of the stability boundary of a class of nonlinear dynamical systems that admit energy functions is developed in this paper. This characterization generalizes the existing results by allowing the type-zero saddle-node nonhyperbolic equilibrium points on the stability boundary. Conceptual algorithms to obtain optimal estimates of the stability region (basin of attraction) in the form of level sets of a given family of energy functions are derived. The behavior of the stability region and the corresponding estimates are investigated for parameter variation in the neighborhood of a type-zero saddle-node bifurcation value.

The tangential variation of a localized flux-type eigenvalue problem

In this work the differentiability of the principal eigenvalue lambda = lambda(1)(Gamma) to the localized Steklov problem -Delta u + qu = 0 in Omega, partial derivative u/partial derivative nu = lambda chi(Gamma)(x)u on partial derivative Omega, where Gamma subset of partial derivative Omega is a smooth subdomain of partial derivative Omega and chi(Gamma) is its characteristic function relative to partial derivative Omega, is shown. As a key point, the flux subdomain Gamma is regarded here as the variable with respect to which such differentiation is performed. An explicit formula for the derivative of lambda(1) (Gamma) with respect to Gamma is obtained. The lack of regularity up to the boundary of the first derivative of the principal eigenfunctions is a further intrinsic feature of the problem. Therefore, the whole analysis must be done in the weak sense of H(1)(Omega). The study is of interest in mathematical models in morphogenesis. (C) 2011 Elsevier Inc. All rights reserved.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Bifurcation and singularity analysis of a molecular network for the induction of long-term memory.

Withdrawal reflexes of the mollusk Aplysia exhibit sensitization, a simple form of long-term memory (LTM). Sensitization is due, in part, to long-term facilitation (LTF) of sensorimotor neuron synapses. LTF is induced by the modulatory actions of serotonin (5-HT). Pettigrew et al. developed a computational model of the nonlinear intracellular signaling and gene network that underlies the induction of 5-HT-induced LTF. The model simulated empirical observations that repeated applications of 5-HT induce persistent activation of protein kinase A (PKA) and that this persistent activation requires a suprathreshold exposure of 5-HT. This study extends the analysis of the Pettigrew model by applying bifurcation analysis, singularity theory, and numerical simulation. Using singularity theory, classification diagrams of parameter space were constructed, identifying regions with qualitatively different steady-state behaviors. The graphical representation of these regions illustrates the robustness of these regions to changes in model parameters. Because persistent protein kinase A (PKA) activity correlates with Aplysia LTM, the analysis focuses on a positive feedback loop in the model that tends to maintain PKA activity. In this loop, PKA phosphorylates a transcription factor (TF-1), thereby increasing the expression of an ubiquitin hydrolase (Ap-Uch). Ap-Uch then acts to increase PKA activity, closing the loop. This positive feedback loop manifests multiple, coexisting steady states, or multiplicity, which provides a mechanism for a bistable switch in PKA activity. After the removal of 5-HT, the PKA activity either returns to its basal level (reversible switch) or remains at a high level (irreversible switch). Such an irreversible switch might be a mechanism that contributes to the persistence of LTM. The classification diagrams also identify parameters and processes that might be manipulated, perhaps pharmacologically, to enhance the induction of memory. Rational drug design, to affect complex processes such as memory formation, can benefit from this type of analysis.

A Median Voter Theorem for Postelection Politics

We analyze a model of 'postelection politics', in which (unlike in the more common Downsian models of 'preelection politics') politicians cannot make binding commitments prior to elections. The game begins with an incumbent politician in office, and voters adopt reelection strategies that are contingent on the policies implemented by the incumbent. We generalize previous models of this type by introducing heterogeneity in voters' ideological preferences, and analyze how voters' reelection strategies constrain the policies chosen by a rent-maximizing incumbent. We first show that virtually any policy (and any feasible level of rent for the incumbent) can be sustained in a Nash equilibrium. Then, we derive a 'median voter theorem': the ideal point of the median voter, and the minimum feasible level of rent, are the unique outcomes in any strong Nash equilibrium. We then introduce alternative refinements that are less restrictive. In particular, Ideologically Loyal Coalition-proof equilibrium also leads uniquely to the median outcome.

The Zero-Removing Property and Lagrange-Type Interpolation Series

The classical Kramer sampling theorem, which provides a method for obtaining orthogonal sampling formulas, can be formulated in a more general nonorthogonal setting. In this setting, a challenging problem is to characterize the situations when the obtained nonorthogonal sampling formulas can be expressed as Lagrange-type interpolation series. In this article a necessary and sufficient condition is given in terms of the zero removing property. Roughly speaking, this property concerns the stability of the sampled functions on removing a finite number of their zeros.