Ce travail est un travail commun avec Sylvie Boldo, François Clément Florian Faissole et Vincent Martin dans le cadre du projet DIM-RFSI MILC. La résolution des équations aux dérivées partielles (EDP) est au cœur de nombreux programmes de simulation dans l'industrie et la méthode des éléments finis (MEF) est un outil très utilisé pour leur résolution numérique.

Je présenterai le but à long terme dans lequel s'inscrit ce travail, domaine de la sécurité, de la fiabilité et de la sûreté. Il s'agit de poser les fondements qui nous permettront de prouver la correction d'une bibliothèque implantant la MEF en C++, telle que FELiScE (Finite Elements for Life Sciences and Engineering). Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Ces travaux sont interdisciplinaires (logique/preuve de programmes/analyse numérique). Ces preuves reposent entre autres sur les bases mathématiques telles que la théorie de la mesure, l'intégrale de Lebesgue, les distributions, les espaces de Sobolev jusqu'à la construction de l'espace fonctionnel L2. Dans cet exposé je m'attarderai sur la formalisation de l'intégrale de Lebesgue pour les fonctions positives.

Un système de numération associe à chaque élément d’un ensemble donné un mot fini. Le plus connu de ces systèmes est le système décimal, qui associe à chaque entier positif un mot de l’alphabet $\{0, 1,\ldots , 9\}$. Cette idée peut facilement être généralisée à d’autres entiers positifs comme base comme le système binaire ou le système hexadécimal.

La première partie port sur les systèmes de numération signés. Dans ces systèmes, nous ajoutons d’autres chiffres à l’alphabet comme le chiffre $-1$ en système binaire. Sur certaines conditions, sur des chiffres consécutifs, nous obtenons des représentations uniques. Ceci est lié au concept de systèmes de numération abstraits. Nous étudierons le décalage et l’odomètre du point de vue des systèmes dynamiques.

Les restrictions numériques jouent également un rôle important dans un autre système de numération : la représentation de Zeckendorf. Il s’agit d’un exemple de système de numération basé sur des suites définie par récurrence, que nous traitons dans la deuxième partie. Un façon de analyser un système de numération consiste à examiner les fonctions opérant sur la représentation numérique. La plus célèbre de ces fonctions est la fonction de somme des chiffres et nous l’examinons d’un point de vue analytique.

Dans la représentation d’un réel choisi au hasard, nous nous attendons à ce que chaque bloc de chiffres se produis avec la même fréquence. Cela conduit au concept de nombres normaux et à la notion connexe des suites équirépartie. Dans la dernière partie, nous adoptons un point de vue probabiliste et nous construisons des nombres normaux et des suites équiréparties liées aux représentations numériques.