Dans cette thèse nous appliquons le calcul de Malliavin à l'estimation statistique de paramètres de certains processus stochastiques et à l'obtention de théorèmes de la limite centrale pour les variations quadratiques à poids de processus fractionnaires et/ou à deux paramètres ainsi qu'à l'approximation gaussienne de mesures de probabilités multidimensionnelles. Dans le Chapitre 1 nous construisons des estimateurs de type Stein pour la dérive de processus gaussiens et pour l'intensité de processus de Poisson. Dans le Chapitre 2 nous calculons l'estimateur bayésien du signal d'entrée d'un canal de Poisson et nous étendons notre résultat aux canaux dont le bruit est une martingale normale possédant la propriété de représentation chaotique. Dans le Chapitre 3 nous établissons des théorèmes de la limite centrale pour les variations quadratiques à poids du drap brownien standard (nous permettant de donner un estimateur asymptotiquement normal de la variation quadratique de certains processus de diffusion à deux paramètres) puis pour celles de certains draps browniens fractionnaires. Dans ce même chapitre nous établissons un théorème de la limite centrale pour les variations quadratiques à poids du mouvement brownien fractionnaire d'indice $H=1/4$ nous permettant de donner le comportement asymptotique des sommes de Riemann à signe alterné associées au mouvement brownien fractionnaire d'indice $H=1/4$. Enfin dans le Chapitre 4 nous appliquons la méthode de Stein et du calcul de Malliavin afin d'obtenir des bornes explicites pour l'approximation gaussienne multidimensionnelle de fonctionnelles de champs gaussiens. Nous appliquons en particulier nos résultats aux théorème de la limite centrale de Breuer et Major pour des champs associés à un mouvement brownien fractionnaire.

Le périodogramme est un outil naturel pour l'analyse spectrale d'une série temporelle stationnaire au second ordre. La littérature sur les séries temporelles en donne grand nombre de propriétés - principalement asymptotiques -, que le signal soit a dependence courte ou longue. Beaucoup de ces resultats font l'hypothese supplementaire de gaussianite. La principale contribution de ce travail est l'extension de nombreux resultats connus aux signaux non-gaussiens. Nous traiterons le periodogramme de l'i.i.d. et donnerons une expression asymptotique de ses moments a tout ordre. Nous montrerons que l'on peut traiter le cas plus général du signal linéaire selon deux méthodes. Soit en s'appuyant sur le résultat précédent et la decomposition de Bartlett, soit en traitant directement le periodogramme du lineaire par developpement asymptotique (developement d'Edgeworth) de sa distribution. La premiere methode conduit a des resultats de type "limite centrale" sur une large classe de tableaux triangulaires de fonctionnelles non-lineaire du periodogramme, alors que la seconde permet des resultats de consistance.

Dans cette thèse, on analyse par des méthodes de variétés invariantes deux problèmes distincts: le phénomène des roll-waves en hydraulique et l'existence de breathers discrets dans des réseaux non linéaires discrets. Les roll-waves sont des ondes progressives périodiques et discontinues solutions entropiques des équations de Saint Venant. Grace aux théorèmes de Fenichel, on montre l'existence de roll-waves continues "visqueuses" proches des roll-waves discontinues lorsqu'on ajouté aux équations un petit terme de viscosité. On étudie ensuite la stabilité linéaire de ces roll-waves discontinues. Enfin, on montre l'existence de roll-waves de petite amplitude dans des canaux à fond périodiques.\\ Les breathers discrets sont des oscillations périodiques, localisées en espace dans des réseaux non linéaires discrets. On analyse d'abord le modèle Fermi-Pasta-Ulam (FPU) diatomique. En formulant le problème sous la forme d'un mapping en dimension infinie, on montre, via une réduction à une variété centrale, l'existence de breathers discrets de petite amplitude pour des rapports de masses arbitraires. On utilise aussi cette approche pour montrer l'existence de breathers discrets dans des chaines de spins ferromagnétiques.

Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks.

Dans cette thèse, on étudie comment la positivité du fibré tangent d'une variété projective complexe infl uence la géométrie de la variété sous-jacente. Dans la première partie, on étudie les variétés (principalement les surfaces) dont le fibré tangent est pseudo-effectif. Dans la deuxième partie on montre que pour un entier strictement positif p, si la puissance tensorielle p-ème du fibré tangent d'une variété projective contient la puissance p-ème d'un fibré en droites ample, alors la variété est isomorphe à un espace projectif ou à une quadrique.

Le mouvement Brownien fractionnaire (mBf) est devenu un processus incontournable dès que l'on veut s'affranchir des propriétés de Markov et d'indépendance des accroissements. Nous verrons les principales propriétés de ce processus, nous insisterons sur certains aspects de son utilisation comme modèle de file fluide. On développe ensuite la construction d'une intégrale anticipative relative au mBf à partir de l'intégrale anticipative relative au mouvement Brownien. Fort de cette idée, nous avons introduit une intégrale anticipative relative à des processus de Poissons filtrés (pPf) à partir d'une intégrale anticipative pour des processus de Poissons marqués, intégrale que nous relions à l'intégrale de Stieltjès. L'étude se poursuit par une formule de Itô pour des fonctionnelles cylindriques et par un résultat sur la continuité de Holdër des processus intégrés. Pour finir, un théorème de convergence en loi d'une suite de pPf vers un processus de Volterra est établi.

Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d'Isabelle/HOL nous avons fourni une intégration vérifiée d'UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d'Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d'Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié.

Dans le cadre du présent travail, nous nous intéressons à la transition du secondaire vers le collégial, spécialement en ce qui concerne la démonstration et le formalisme. Nous avons choisi d'évaluer la complexité des tâches de démonstration soumises aux étudiants d'un cours du collégial, Algèbre linéaire et géométrie vectorielle, tel qu'il a été donné au Collège de Maisonneuve à l'hiver 2006, dans le cadre du programme DEC intégré. Nous faisons ensuite une analyse des éléments qui peuvent constituer une préparation à ces tâches, dans le cadre des cours de mathématiques de quatrième et de cinquième secondaires. Par l'analyse de tâches de démonstration de niveau collégial, nous dégageons plusieurs caractéristiques qui contribuent à complexifier largement la production de démonstrations. Nous relevons donc ces caractéristiques et vérifions à travers l'étude des programmes actuels et en processus d'implantation, comment les élèves sont outillés pour faire face à ces éléments de complexité. En conclusion, nous proposons des pistes de réflexions et d'interventions visant à minimiser les impacts de cette transition secondaire-collégial. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Didactique des mathématiques, Arrimage secondaire-collégial, Algèbre linéaire, Démonstration, Formalisme.

La production de conjectures, de preuves et de démonstrations mathématiques chez les élèves de l'école secondaire est depuis plusieurs années un thème important de la recherche en didactique des mathématiques. La problématique sous-jacente se complexifie quand on considère de surcroît le rôle que peut jouer la technologie dans l'apprentissage de la preuve et de la démonstration, notamment vis-à-vis la production de conjectures, comme préalable au travail sur une preuve donnée. Ces questions sont ici spécifiées aux élèves de 5e secondaire de l'école québécoise. Le contenu mathématique que nous avons choisi pour étudier ces questions est celui des coniques, approchées avec un logiciel de géométrie dynamique. Plus particulièrement, nous nous sommes intéressés à l'analyse des stratégies et démarches des élèves de 5e secondaire au moment où ils travaillent une démonstration, dans le contexte du thème choisi, d'abord avec papier-crayon et ensuite, avec technologie. Des activités ad hoc ont été élaborées et soumises aux élèves auprès desquels nous avons expérimenté. Les productions qui ont résulté de ces tâches nous ont permis d'analyser les erreurs et obstacles en lien avec la production des conjectures, des preuves et des démonstrations par les élèves. Les résultats issus de l'expérimentation et de l'analyse des productions montrent les aspects positifs et négatifs du travail avec papier-crayon, et aussi de l'environnement technologique. La comparaison de ces deux milieux de travail, des possibilités qu'ils offrent et des contraintes qu'ils sous-tendent pourront servir de piste pour une éventuelle amélioration de l'enseignement des mathématiques à l'école secondaire. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Conjecture, preuve, démonstration, travail papier-crayon, géométrie dynamique, coniques.

Nous nous intéressons à la représentation de graphes dans le prouveur Coq. Nous avons choisi de les représenter par des types coinductifs dont nous voulions explorer l'utilisation. Ceux-ci permettent de rendre succincte et élégante la représentation et d'obtenir la navigabilité par construction. Nous avons dû contourner la condition de garde dont le but est d'assurer la validité des opérations effectuées sur les objets coinductifs. Son implantation dans Coq est restrictive et interdit parfois des définitions sémantiquement correctes. Une formalisation canonique des graphes dépasse ainsi l'expressivité directe de Coq. Nous avons donc proposé une solution respectant ces limitations, puis nous avons défini une relation sur les graphes nous permettant d'obtenir la même notion d'équivalence qu'avec une représentation classique tout en gardant les avantages de la coinduction. Nous montrons qu'elle est équivalente à une relation basée sur des observations finies.