Dans cette thèse, on s'intéresse à l'analyse harmonique et aux fonctions spéciales associées aux opérateurs de Dunkl rationnels qui sont des déformations des dérivées directionnelles par des réflexions. Ils fournissent un outil décisif pour étendre, dans le cadre des systèmes de racines et des groupes de réflexions associés, l'analyse de Fourier euclidienne et l'analyse sur les espaces symétriques riemanniens plats. Après avoir donné un panorama détaillé de la théorie de Dunkl, on étudie l'opérateur maximal défini dans ce contexte. On commence par apporter des améliorations sur le comportement des constantes du théorème maximal de Thangavelu et Xu pour un groupe de réflexions quelconque. On étend ensuite dans un cadre vectoriel leur théorème en établissant dans le cas Z_2^d des inégalités de Fefferman-Stein. Pour y parvenir et puisque les techniques d'analyse réelle ne se prêtent pas à cet opérateur maximal, on construit un opérateur de type Hardy-Littlewood plus commode à étudier. A cet effet, on donne une estimation fine de la translation généralisée de l'indicatrice d'une boule. Notre étude est ensuite consacrée à des résultats d'intégrabilité exponentielle qui complètent les inégalités de Fefferman-Stein, et à un théorème maximal vectoriel pour des hypergroupes de Bessel-Kingman. Enfin, on développe l'analyse de Dunkl dans le cas d'un sous-système positif de racines orthogonales. On y établit une formule explicite du noyau de Dunkl et une formule produit qui implique le caractère borné de la translation de Dunkl. Le cas particulier d'un système de type A_1 est étudié afin d'établir une égalité liant les fonctions de Bessel normalisées et les polynômes de Gegenbauer.

L'analyse réelle a de nombreuses applications car c'est un outil approprié pour modéliser de nombreux phénomènes physiques et socio-économiques. En tant que tel, sa formalisation dans des systèmes de preuve formelle est justifié pour permettre aux utilisateurs de vérifier formellement des théorèmes mathématiques et l'exactitude de systèmes critiques. La bibliothèque standard de Coq dispose d'une axiomatisation des nombres réels et d'une bibliothèque de théorèmes d'analyse réelle. Malheureusement, cette bibliothèque souffre de nombreuses lacunes. Par exemple, les définitions des intégrales et des dérivées sont basées sur les types dépendants, ce qui les rend difficiles à utiliser dans la pratique. Cette thèse décrit d'abord l'état de l'art des différentes bibliothèques d'analyse réelle disponibles dans les assistants de preuve. Pour pallier les insuffisances de la bibliothèque standard de Coq, nous avons conçu une bibliothèque facile à utiliser : Coquelicot. Une façon plus facile d'écrire les formules et les théorèmes a été mise en place en utilisant des fonctions totales à la place des types dépendants pour écrire les limites, dérivées, intégrales et séries entières. Pour faciliter l'utilisation, la bibliothèque dispose d'un ensemble complet de théorèmes couvrant ces notions, mais aussi quelques extensions comme les intégrales à paramètres et les comportements asymptotiques. En plus, une hiérarchie algébrique permet d'appliquer certains théorèmes dans un cadre plus générique comme les nombres complexes pour les matrices. Coquelicot est une extension conservative de l'analyse classique de la bibliothèque standard de Coq et nous avons démontré les théorèmes de correspondance entre les deux formalisations. Nous avons testé la bibliothèque sur plusieurs cas d'utilisation : sur une épreuve du Baccalauréat, pour les définitions et les propriétés des fonctions de Bessel ainsi que pour la solution de l'équation des ondes en dimension 1. / Real analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, the definitions of integrals and derivatives are based on dependent types, which make them cumbersome to use in practice. This thesis first describes various state-of-the-art libraries available in proof assistants. To palliate the inadequacies of the Coq standard library, we have designed a user-friendly formalization of real analysis: Coquelicot. An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals and asymptotic behaviors. Moreover, an algebraic hierarchy makes it possible to apply some of the theorems in a more generic setting, such as complex numbers or matrices. Coquelicot is a conservative extension of the classical analysis of Coq's standard library and we provide correspondence theorems between the two formalizations. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation.

Cette recherche étudie l'enseignement des premiers éléments de l'Analyse réelle à la transition lycée/université à travers un modèle de variables macro-didactiques (VMD) relatives aux niveaux de formalisation et de familiarité des savoirs mathématiques proposés aux élèves. Lorsque l'on passe du lycée à l'université, les valeurs de ces variables sont dichotomiques et témoignent d'une profonde mutation dans le travail mathématique demandé. Nous nous posons la question des moyens que peut se donner l'enseignement des mathématiques, à l'entrée à l'université, pour gérer des variations aussi importantes et permettre aux étudiants d'accéder aux objets de l'Analyse réelle. <br />Une ingénierie a porté sur la construction et l'expérimentation, dans le cadre de la TSD (Théorie des Situations Didactiques), de deux situations sur les limites, que nous avons expérimentées à un niveau du cursus où seule l'existence formelle des objets de l'Analyse réelle a été établie par les professeurs. Nous avons ciblé le travail des étudiants sur les méthodes d'approximation, afin de favoriser des allers/retours entre les "preuves pragmatiques" géométriques ou numériques et l'utilisation des théorèmes d'Analyse. Les situations prennent en compte la dialectique sémantique/ syntaxique dans un processus de preuve, et permettent un retour efficace sur les savoirs visés. L'entrée dans un processus de preuves mixtes – pragmatiques vs formelles – a ainsi été rendu obligatoire dans le travail des étudiants, à travers l'émergence du problème général de l'existence et de l'accessibilité des nombres, des limites et des suites. <br />En conclusion, nous proposons de poursuivre l'étude du milieu théorique des situations de l'Analyse réelle, d'introduire d'autres situations expérimentales et d'étudier plus en profondeur les connaissances des étudiants dans le contrat didactique instauré par de telles situations.