Dados dois conjuntos compactos e convexos K1, K2 em R², queremos saber se existem f e h, dois homeomorfismos de T², homotópicos à identidade, que comutam, com levantamentos F e H, tais que K1 e K2 são os seus conjuntos de rotação, respectivamente. Neste trabalho, mostramos alguns casos onde isto não pode acontecer, assumindo restrições nos conjuntos de rotação. Além disso, introduzimos o conceito de conjunto de rotação para semigrupos Abelianos finitamente gerados por homeomorfismos homotópicos à identidade, mostrando um caso em que o semigrupo é anular. / Let K1, K2 in R² be two convex, compact sets. We would like to know if there are commuting homeomorphisms f and h of T², homotopic to the identity, with lifts F and H, such that K1 and K2 are their rotation sets, respectively. In this work, we proof some cases where it cannot happen, assuming some restrictions on rotation sets. Besides that, we introduce the concept of rotation set for Abelian semi-groups finitely generated by homeomorphisms homotopic to the identity, showing a case where the semi-group is annular.

Dados dois conjuntos compactos e convexos K1, K2 em R², queremos saber se existem f e h, dois homeomorfismos de T², homotópicos à identidade, que comutam, com levantamentos F e H, tais que K1 e K2 são os seus conjuntos de rotação, respectivamente. Neste trabalho, mostramos alguns casos onde isto não pode acontecer, assumindo restrições nos conjuntos de rotação. Além disso, introduzimos o conceito de conjunto de rotação para semigrupos Abelianos finitamente gerados por homeomorfismos homotópicos à identidade, mostrando um caso em que o semigrupo é anular. / Let K1, K2 in R² be two convex, compact sets. We would like to know if there are commuting homeomorphisms f and h of T², homotopic to the identity, with lifts F and H, such that K1 and K2 are their rotation sets, respectively. In this work, we proof some cases where it cannot happen, assuming some restrictions on rotation sets. Besides that, we introduce the concept of rotation set for Abelian semi-groups finitely generated by homeomorphisms homotopic to the identity, showing a case where the semi-group is annular.

Thesis (MSc)--Stellenbosch University, 2011. / ENGLISH ABSTRACT: An integro-differential equation describing the dynamical behaviour of phytoplankton cells is considered in which the effects of cell division and aggregation are incorporated by coupling the coagulation-fragmentation equation with growth, and the McKendrick-von Foerster renewal model of an age-structured population. Under appropriate conditions on the model parameters, the associated initial-boundary value problem is shown to be well posed in a physically relevant Banach space using the theory of strongly continuous semigroups of operators, the theory of perturbation of positive semigroups and the semilinear abstract Cauchy problems theory. In particular, we provide sufficient conditions for honesty of the model. Finally, the results on the effects of the growth-fragmentation-coagulation on the overall evolution of the phytoplankton population are summarised. / AFRIKAANSE OPSOMMING: ’n Integro-differensiaalvergelyking wat die dinamiese ontwikkeling van fitoplanktonselle beskryf, word beskou. Die uitwerking van seldeling en -aggregasie is geïnkorporeer deur die vergelyking van koagulasie en fragmentasie met groeiaan die McKendrick-von Foerster hernuwingsmodel van ’n ouderdomsgestruktureerde populasie te koppel. Die teorie van sterk kontinue semigroepe van operatore, steuringsteorie van positiewe semigroepe en die teorie van semilineêre abstrakte Cauchy probleme word aangewend om, onder gepaste voorwaardes met betrekking tot die model se parameters, te bewys dat die geassosieerde beginwaarde-probleem met randvoorwaardes ‘goed gestel’ is in ’n fisies relevante Banach-ruimte. In die besonder word voldoende voorwaardes vir eerlikheid van die model verskaf. Ten slotte word ’n opsomming van die resultate met betrekking tot die gekombineerde uitwerking van groei-fragmentasie- koagulasie op die gesamentlike ontwikkeling van die fitoplanktonpopulasie verskaf.

Ce travail est constitué de deux parties indépendantes traitant chacune d'un problème issu de la théorie du contrôle des équations aux dérivées partielles. La première partie est consacrée à l'étude d'un feedback explicite et déjà connu, s'appliquant à des systèmes linéaires, réversibles en temps et éventuellement munis d'un opérateur de contrôle non-borné. On justifie le caractère bien posé du problème en boucle fermée via la théorie des semi-groupes puis on étudie le taux de décroissance des solutions du système régulé. La seconde partie concerne un problème d'observation pour la corde vibrante : on détermine comment choisir des instants d'observation pour que la position de la corde à ces instants permette de retrouver les conditions initiales tout en préservant une certaine régularité. La méthode, qui repose sur des résultats d'approximation diophantienne, est ensuite étendue à d'autres systèmes. En utilisant une méthode de dualité on démontre aussi un résultat de contrôlabilité exacte. / This works contains two independent parts, each one dealing with the control of partial differential equations. In the first part, we study an explicit and already known feedback law that applies to linear, time-reversible systems, with a possibly unbounded control operator. We prove the well-posedness of the closed-loop problem in the semi-group framework and we study the decay rate of the solutions. In the second part, we give conditions on the choice of some time instants, such that the positions of a vibrating string (or beam) at these times enable to recover the initial data. The method relies on Diophantine approximation results. Using a duality method, we give a related exact controllability result.

La Commande prédictive ou Commande Optimale à Horizon Glissant (COHG) devient de plus en plus populaire dans de nombreuses applications pratiques en raison de ses avantages importants tels que la stabilisation et la prise en compte des contraintes. Elle a été bien étudiée pour des systèmes en dimension finie même dans le cas non linéaire. Cependant, son extension aux systèmes en dimension infinie n'a pas retenu beaucoup d'attention de la part des chercheurs. Ce travail de thèse apporte des contributions à l'application de cette approche aux systèmes de lois de conservation. Nous présentons tout d'abord une preuve de stabilité complète de la COHG pour certaines classes de systèmes en dimension infinie. Ce résultat est ensuite utilisé pour les systèmes hyperboliques 2x2 commandés aux frontières et appliqué à un problème de contrôle de canal d'irrigation. Nous proposons aussi l'extension de cette stratégie au cas de réseaux de systèmes hyperboliques 2x2 en cascade avec une application à un ensemble de canaux d'irrigation connectés. Nous étudions également les avantages de la COHG dans le contexte des systèmes non linéaires et semi-linéaires notamment vis-à-vis des chocs. Toutes les analyses théoriques sont validées par simulation afin d'illustrer l'efficacité de l'approche proposée. / The predictive control or Receding Horizon Optimal Control (RHOC) is becoming increasingly popular in many practical applications due to its significant advantages such as the stabilization and constraints handling. It has been well studied for finite dimensional systems even in the nonlinear case. However, its extension to infinite dimensional systems has not received much attention from researchers. This thesis proposes contributions on the application of this approach to systems of conservation laws. We present a complete proof of stability of RHOC for some classes of infinite dimensional systems. This result is then used for 2x2 hyperbolic systems with boundary control, and applied to an irrigation canal. We also propose the extension of this strategy to networks of cascaded 2x2 hyperbolic systems with an application to a set of connected irrigation canals. Furthermore, we study the benefits of RHOC in the context of nonlinear and semi-linear systems in particular with respect to the problem of shocks. All theoretical analyzes are validated by simulation in order to illustrate the effectiveness of the proposed approach.

Dependent type theories are a kind of mathematical foundations investigated both for the formalisation of mathematics and for reasoning about programs. They are implemented as the kernel of many proof assistants and programming languages with proofs (Coq, Agda, Idris, Dedukti, Matita, etc). Dependent types allow to encode elegantly and constructively the universal and existential quantifications of higher-order logics and are therefore adapted for writing logical propositions and proofs. However, their usage is not limited to the area of pure logic. Indeed, some recent work has shown that they can also be powerful for driving the construction of programs. Using more precise types not only helps to gain confidence about the program built, but it can also help its construction, giving rise to a new style of programming called Type-Driven Development. However, one difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories (like CIC and ML) from the fact that in a non-empty context, the propositional equality allows us to prove as equal (with the induction principles) terms that are not judgementally equal, which implies that the typechecker can't always obtain equality proofs by reduction. As far as possible, we would like to solve such proof obligations automatically, and we absolutely need it if we want dependent types to be use more broadly, and perhaps one day to become the standard in functional programming. In this thesis, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. However, the method that we follow is independent from the language being used, and this work could be reproduced in any dependently-typed language. We present an original type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression that they represent, and show how it allows us to easily construct and manipulate proofs. We build a hierarchy of correct-by-construction tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs. Finally, and as a conclusion, we discuss the trust we can have in such machine-checked proofs.

Cette thèse est consacrée à l'étude théorique mathématique des équations de Stokes et de Navier-Stokes dans un domaine borné de R^3 en utilisant la théorie des semi-groupes. Trois différents types de conditions seront considérés : des conditions aux limites de Navier, de type-Navier et des conditions qui dépendent de la pression. Ce manuscrit est composé de six chapitres. Tout d'abord nous commençons par un état de l'art sur les équations de Navier-Stokes. Ensuite nous démontrons l'analyticité du semi-groupe de Stokes avec chacune des conditions ci-dessus. Ceci permet de résoudre le problème d'évolution en utilisant la théorie des semi-groupes. Nous étudions également les puissances complexes et fractionnaires de l'opérateur de Stokes pour lesquelles nous démontrons certaines propriétés et estimations. Ces résultats seront utilisés dans la suite pour obtenir des estimations de type L^p-L^q pour le semi-groupe de Stokes, un résultat de régularité L^p-L^q maximale pour le problème de Stokes inhomogène et des résultats d'existence et d'unicité locale pour le problème non-linéaire. Après nous étudions le problème d'évolution de Stokes. Outre la régularité L^p-L^q maximale, nous démontrons l'existence des solutions faibles u∈L^q (0,T; W^(1,p) (Ω)), fortes u∈L^q (0,T; W^(2,p) (Ω)) et très faibles u∈L^q (0,T; L^p (Ω)) du problème de Stokes. On termine par l'étude du problème de Navier-Stokes avec chacune des conditions aux limites citées ci-dessus. Tout d'abord, en utilisant les estimations L^p-L^q on démontre l'existence d'une unique solution locale u qui vérifieu∈BC([0,T_0 ); L_(σ,τ)^p (Ω))∩L^q (0,T_0; L_(σ,τ)^r (Ω)), q,r>p, 2/q+3/r=3/p.De plus, pour une donnée initiale petite, on obtient l'existence globale des solutions. Ensuite en estimant le terme non-linéaire en fonction des puissances fractionnaires de l'opérateur de Stokes on démontre la régularité de la solution. / This thesis is devoted to the mathematical theoretical study of the Stokes and Navier-Stokes equations in a bounded domain of R^3 using the semi-group theory. Three different types of boundary conditions will be considered: Navier boundary conditions, Navier-type boundary conditions and boundary condition involving the pressure. This manuscript contains six chapters. We prove first the analyticity of the Stokes semi-group with each of the boundary conditions stated above. This allows us to solve the time dependent Stokes problem using the semi-group theory. We will study also the complex and fractional powers of the Stokes operator for which we prove some properties and estimations. These results will be used in the sequel to prove an estimate of type L^p-L^q for the Stokes semigroup, as well as the maximal L^p-L^q regularity for the inhomogeneous Stokes problem and an existence result for the non-linear problem. Next we study the time dependent Stokes problem, besides the maximal L^p-L^q regularity, we prove the existence of weak u∈L^q (0,T; W^(1,p) (Ω)), strong u∈L^q (0,T; W^(2,p) (Ω)) and very weak u∈L^q (0,T; L^p (Ω)) solutions to the Stokes problem. We end with the study of the Navier-Stokes problem. First using the L^p-L^q estimate for the Stokes semi-group we prove the existence of a unique local in time mild solution for the Navier-Stokes problem that verifies u∈BC([0,T_0 ); L_(σ,τ)^p (Ω))∩L^q (0,T_0; L_(σ,τ)^r (Ω)), q,r>p, 2/q+3/r=3/p.Furthermore, for some initial data the solution is global in time. Finally, by estimating the non-linear term as a function of the fractional powers of the Stokes operator we prove that the solution is regular.

La thèse est portée essentiellement sur la stabilisation et la contrôlabilité de deux équations des ondes moyennant un seul contrôle agissant sur le bord du domaine. Dans le cas du contrôle dynamique, le contrôle est introduit dans le système par une équation différentielle agissant sur le bord. C'est en effet un système hybride. Le contrôle peut être aussi applique directement sur le bord d'une équation, c'est le cas du contrôle indirecte mais non borne. La nature du système ainsi coupledépend du couplage des équations, et ceci donne divers résultats par la stabilisation (exponentielle et polynomiale) et la contrôlabilité exacte (espace contrôlable). Des nouvelles inégalités d'énergie permettent de mettre en oeuvre la Méthode fréquentielle et la Méthode d'Unicité de Hilbert. / This thesis is concerned with the stabilization and the exact controllability of two wave equations by means of only one control acting on the boundary of the domain. In the case of dynamic control, the control is introduced into the system by differential equation acting on the boundary. It is indeed a hybrid system. The control can be also applied directly on the boundary of one of the equations. In this case, the control is indirect but unbounded. The behavior of the obtained system depends on theways of coupling. Various results are established for the stabilization (exponential or polynomial) and the exact controllability (controllable space of initial data). A new inequality of energy allows to apply the Frequency Method and the Hilbert Uniqueness Method.