1 |
Exploring the neural codes using parallel hardware / Explorer les codes neuronaux utilisant des machines parallèlesBaladron Pezoa, Javier 07 June 2013 (has links)
L'objectif de cette thèse est de comprendre la dynamique des grandes populations de neurones interconnectées. La méthode utilisée pour atteindre cet objectif est un mélange de modèles mésoscopiques et calculs de haute performance. Le premier permet de réduire la complexité du réseau neuronale et le second de réaliser des simulations à grandes échelles. Dans la première partie de cette thèse une nouvelle approche du champ moyen est utilisée pour étudier numériquement les effets du bruit sur un groupe extrêmement grand de neurones. La même approche a été utilisée pour créer un modèle d' hypercolonne du premier cortex visuel d'où l'unité basique, est des grandes populations de neurones au lieu d'une seule cellule. Les simulations sont réalisées en résolvant un système d'équation différentielle partielle qui décrit l'évolution de la fonction de densité de probabilité du réseau. Dans la deuxième partie de cette thèse est présentée une étude numérique de deux modèles de champs neuronaux du premier cortex visuel. Le principal objectif est de déterminer comment les contours sont sélectionnés dans le cortex visuel. La différence entre les deux modèles est la manière de représenter des préférences d'orientations des neurones. Pour l'un des modèles, l'orientation est une caractéristique de l'équation et la connectivité dépend d'elle. Dans l'autre, il existe une carte d'orientation qui définit une fonction d'entrée. Toutes les simulations sont réalisées sur un cluster de processeurs graphiques. Cette thèse propose des techniques pour simuler rapidement les modèles proposés sur ce type de machine. La vitesse atteinte est équivalente à un cluster standard très grand. / The aim of this thesis is to understand the dynamics of large interconnected populations of neurons. The method we use to reach this objective is a mixture of mesoscopic modeling and high performance computing. The rst allows us to reduce the complexity of the network and the second to perform large scale simulations. In the rst part of this thesis a new mean eld approach for conductance based neurons is used to study numerically the eects of noise on extremely large ensembles of neurons. Also, the same approach is used to create a model of one hypercolumn from the primary visual cortex where the basic computational units are large populations of neurons instead of simple cells. All of these simulations are done by solving a set of partial dierential equations that describe the evolution of the probability density function of the network. In the second part of this thesis a numerical study of two neural eld models of the primary visual cortex is presented. The main focus in both cases is to determine how edge selection and continuation can be computed in the primary visual cortex. The dierence between the two models is in how they represent the orientation preference of neurons, in one this is a feature of the equations and the connectivity depends on it, while in the other there is an underlying map which denes an input function. All the simulations are performed on a Graphic Processing Unit cluster. Thethesis proposes a set of techniques to simulate the models fast enough on this kind of hardware. The speedup obtained is equivalent to that of a huge standard cluster.
|
2 |
Paramétrisations physiques pour un modèle opérationnel de prévision météorologique à haute résolutionGérard, Luc 31 August 2001 (has links)
Les modèles de prévision opérationnelle du temps résolvent numériquement les équations de la mécanique des fluides en calculant l'évolution de champs (pression, température, humidité, vitesses) définis comme moyennes horizontales à l'échelle des mailles d'une grille (et à différents niveaux verticaux).
Les processus d'échelle inférieure à la maille jouent néanmoins un rôle essentiel dans les transferts et les bilans de chaleur, humidité et quantité de mouvement. Les paramétrisations physiques visent à évaluer les termes de source correspondant à ces phénomènes, et apparaissant dans les équations des champs moyens aux points de grille.
Lorsque l'on diminue la taille des mailles afin de représenter plus finement l'évolution des phénomènes atmosphériques, certaines hypothèses utilisées dans ces paramétrisations perdent leur validité. Le problème se pose surtout quand la taille des mailles passe en dessous d'une dizaine de kilomètres, se rapprochant de la taille des grands systèmes de nuages convectifs (systèmes orageux, lignes de grain).
Ce travail s'inscrit dans le cadre des développements du modèle à mailles fines ARPÈGE ALADIN, utilisé par une douzaine de pays pour l'élaboration de prévisions à courte échéance (jusque 48 heures).
Nous décrivons d'abord l'ensemble des paramétrisations physiques du modèle.
Suit une analyse détaillée de la paramétrisation actuelle de la convection profonde. Nous présentons également notre contribution personnelle à celle ci, concernant l'entraînement de la quantité de mouvement horizontale dans le nuage convectif.
Nous faisons ressortir les principaux points faibles ou hypothèses nécessitant des mailles de grandes dimensions, et dégageons les voies pour de nouveaux développements.
Nous approfondissons ensuite deux des aspects sortis de cette discussion: l'usage de variables pronostiques de l'activité convective, et la prise en compte de différences entre l'environnement immédiat du nuage et les valeurs des champs à grande échelle. Ceci nous conduit à la réalisation et la mise en œuvre d'un schéma pronostique de la convection profonde.
A ce schéma devraient encore s'ajouter une paramétrisation pronostique des phases condensées suspendues (actuellement en cours de développement par d'autres personnes) et quelques autres améliorations que nous proposons.
Des tests de validation et de comportement du schéma pronostique ont été effectués en modèle à aire limitée à différentes résolutions et en modèle global. Dans ce dernier cas l'effet du nouveau schéma sur les bilans globaux est également examiné.
Ces expériences apportent un éclairage supplémentaire sur le comportement du schéma convectif et les problèmes de partage entre la schéma de convection profonde et le schéma de précipitation de grande échelle.
La présente étude fait donc le point sur le statut actuel des différentes paramétrisations du modèle, et propose des solutions pratiques pour améliorer la qualité de la représentation des phénomènes convectifs.
L'utilisation de mailles plus petites que 5 km nécessite enfin de lever l'hypothèse hydrostatique dans les équations de grande échelle, et nous esquissons les raffinements supplémentaires de la paramétrisation possibles dans ce cas.
|
3 |
Approche multi-échelles morphologique et directe pour une classe de composites particulaires fortement chargés hyperélastiques et visco-hyperélastiques.Touboul, Marion 13 November 2007 (has links) (PDF)
Cette thèse est consacrée à la modélisation par transition d'échelles d'une large classe de composites particulaires fortement chargés tels que les propergols solides. L'approche (AM) repose en amont sur une schématisation géométrique et cinématique inspirée des travaux de Christoffersen (1983). L'objectif des présents travaux est double : prouver l'applicabilité de l'AM à la viscohyperélasticité (comportement de la matrice des élastomères chargés) et évaluer quantitativement ses performances. Pour traiter le 1er point, l'AM est appliquée à un composite aléatoire à matrice viscohyperélastique, généré numériquement. On montre le caractère direct de la résolution du problème de localisation-homogénéisation grâce à un algorithme opérant dans l'espace-temps réel. Les résultats obtenus sont qualitativement corrects. Concernant le 2ème point, les effets des hypothèses cinématiques propres à l'AM sont testés au travers de comparaisons entre résultats (locaux et globaux) AM et éléments finis (EF) sur des microstructures périodiques (simple et complexe) satisfaisant la schématisation géométrique et pour des comportements de phase hyperélastiques et viscohyperélastiques. Un certain nombre d'atouts et de points d'amélioration de l'AM sont ainsi dégagés. Enfin, un programme transversal de confrontation des estimations à des résultats expérimentaux et à des calculs EF sur un propergol réel est élaboré et mis en œuvre sur un composite énergétique : la butalite 400. Chaque étape –essais sur composite et constituants, caractérisation morphologique par tomographie, maillage EF automatique de la microstructure réelle, détermination des VER (plusieurs centaines de grains) relatifs aux deux méthodes (AM et EF)– est détaillée. De multiples confrontations entre les résultats expérimentaux et les premiers résultats numériques (AM et EF) permettent de préciser les perspectives à entreprendre pour terminer la validation.
|
4 |
Calculs et visualisation en nombres complexesTestard, Laurent 27 November 1997 (has links) (PDF)
Le but de cette thèse est de fournir des moyens de calcul et de visualisation d'objets mathématiques issus de l'analyse complexe. Dans ce cadre, de nombreux problèmes d'origine mathématique empêchent d'utiliser les nombres complexes aussi naturellement que les nombres réels : indéterminations dans les calculs, nombre élevé de dimensions empêchant les méthodes naïves de visualisation, phénomènes multiformes. Au niveau calcul, quelques méthodes ont été étudiées, menant à la définition d'un modèle de programmation permettant de gérer les indéterminations. Au niveau visualisation, des méthodes adaptées aux objets mathématiques complexes ont été mises au point, en particulier dans le cadre des solutions d'équations différentielles complexes. Toutes ces méthodes (calcul, visualisation) ont été implémentées sous forme de modules dans un environnement commun permettant le prototypage rapide d'expériences, axées notamment sur un couplage entre calcul et visualisation. Les différentes applications présentées dans le document (intégration numérique d'équations différentielles avec des fonctions multiformes, visualisation de solutions d'équations différentielles complexes, visualisation de l'erreur globale estimée pendant une intégration) y ont été intégrées.
|
5 |
Calcul Haute-Performance et Mécanique Quantique : analyse des ordonnancements en temps et en mémoireMaillard, Nicolas 19 November 2001 (has links) (PDF)
Ce travail présente l'apport de l'ordonnancement pour la programmation parallèle performante d'applications numériques en mécanique et chimie quantique. Nous prenons deux exemples types de résolution de l'équation de Schrödinger --- Boîte Quantique (BQ) et Méthode des Perturbations d'ordre 2 (MP2) --- qui nécessitent de grosses ressources en calcul et mémoire. La programmation traditionnelle (échange de messages et/ou multithreading) des machines parallèles (distribuées ou SMP) est illustrée par les performances obtenues avec le benchmark Linpack sur la grappe I-cluster (INRIA). Le manque de portabilité du code hautement performant obtenu montre l'importance d'un environnement de programmation parallèle permettant de découpler le codage de l'algorithme de son ordonnancement sur la machine cible. Nous introduisons alors Athapascan, qui repose sur l'analyse du flot de données, pour calculer dynamiquement des ordonnancements prouvés efficaces. Un premier critère d'efficacité est le temps de calcul. Sur certains modèles de machines, la théorie et l'expérience montrent que Athapascan permet des ordonnancements qui garantissent des exécutions efficaces pour certains algorithmes adaptés à BQ, de type itératif (méthode de Lanczos). Un deuxième critère fondamental est l'espace mémoire requis pour les exécutions parallèles en calcul numérique ; c'est particulièrement critique pour MP2. Nous proposons d'annoter le Graphe de Flot de Données (GFD) manipulé par Athapascan pour prendre en compte la mémoire et permettre des ordonnancements dynamiques efficaces en mémoire. Pour MP2, dont le GFD est connu statiquement, un ordonnancement efficace en temps et en mémoire est donné.
|
6 |
Étude du bilan d'eau atmosphérique sur l'Amérique du Nord par décomposition d'échelle pour les climats présent et futur, tels que simulés par le Modèle Régional Canadien du ClimatBresson, Raphaël January 2009 (has links) (PDF)
L'eau est à la fois ressource et source de danger dans nos sociétés. Elle est aussi l'un des principaux acteurs du climat. Que ce soit pour la gestion des ressources en eau, la prévention des extrêmes climatiques ou une meilleure compréhension du climat, une bonne connaissance du cycle hydrologique est clairement indispensable. Ce projet consiste en l'étude du bilan d'eau atmosphérique tel que simulé par le Modèle Régional Canadien du Climat (MRCC) piloté par le Modèle Climatique Canadien Global (MCCG3) au-dessus de l'Amérique du nord. Deux simulations de 30 ans sont considérées, représentant pour l'une le climat actuel, et pour l'autre un climat futur plus chaud, selon le scénario A2 du Rapport Spécial sur les Scénarios d'Emission. La climatologie actuelle du bilan d'eau atmosphérique de ces deux climats est étudiée par le calcul de statistiques saisonnières pour les saisons d'été et d'hiver. Les variables du bilan d'eau sont de plus décomposées en trois échelles spatiales: une très grande échelle résolue par le MCCG3 et imposée au MRCC par le pilotage, une grande échelle résolue à la fois par le MRCC et le MCCG3, et une petite échelle résolue uniquement par le MRCC. La divergence horizontale du flux d'humidité atmosphérique est également décomposée de façon alternative en 9 termes d'interaction impliquant une des trois échelles de vent et d'humidité. Cette décomposition d'échelle permet d'une part d'explorer la contribution des différentes échelles à la climatologie du bilan d'eau atmosphérique, et d'autre part d'évaluer la valeur ajoutée des fines échelles du MRCC en les comparant aux plus grandes échelles du modèle. Les résultats traduisent des climatologies distinctes du bilan d'eau atmosphérique pour la saison d'hiver, dominée par le passage des dépressions des moyennes latitudes, et la saison d'été, où davantage de convection se produit. La contribution des petites échelles à la moyenne saisonnière des variables du bilan d'eau apparaît très limitée. En revanche, elle s'avère être importante pour leur variabilité intrasaisonnière, suggérant une valeur ajoutée importante des petites échelles. La comparaison des deux simulations de climat révèle une intensification générale de la branche atmosphérique du cycle hydrologique dans le climat futur simulé par le MRCC, comparable en termes relatifs pour les champs de moyenne et de variabilité temporelle. Elle apparaît également plus forte en termes relatifs en hiver qu'en été. Les changements observés, ainsi que la contribution des différentes échelles à ces changements, présentent des patrons cohérents avec ceux des variables dans le climat présent et sont gradués en amplitude selon l'intensité des signaux du climat présent. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : MRCC, Décomposition d'échelle, Bilan d'eau atmosphérique, Changement climatique, Valeur ajoutée.
|
7 |
Les théories physiques face au calcul numérique : enjeux et conséquences de la mécanique discrète / Physical theories and numeral computation : studies and consequences of discrete mechanicsArdourel, Vincent 10 December 2013 (has links)
Avec le développement des ordinateurs, la résolution numérique des équations de la physique est devenue un outil de calcul puissant pour établir des prédictions physiques. Mais le recours au calcul numérique entraîne des changements plus profonds pour les théories physiques. Le but de cette thèse est de montrer que le calcul numérique sur machine conduit à une véritable reformulation des théories physiques. Les lois et les principes fondamentaux formulés à l'aide d'équations différentielles sont reformulés de manière discrète. Pour cela, je me concentre sur le cas d'une théorie physique: la mécanique classique. Je montre que depuis les années 1980 une mécanique discrète a été développée. J'analyse cette approche et j'examine en particulier ce qu'elle nous apprend sur la représentation du temps comme continu dans les théories physiques. Dans une première partie, j'examine la résolution numérique sur machine en tant qu'outil pour la prédiction quantitative en physique. Je montre la nécessité pour les scientifiques d'y recourir et je propose une analyse des concepts fondamentaux de ce type de résolution. Dans une deuxième partie, j'examine dans quelle mesure le calcul numérique est un élément constitutif des théories physiques. Je défends la thèse selon laquelle la mécanique discrète est une nouvelle théorie du mouvement classique. Dans une troisième partie, je soutiens une thèse sur la représentation du temps comme continu dans les théories physiques. C'est une représentation dont les scientifiques peuvent se passer. J'examine ensuite en quel sens la représentation traditionnelle du temps comme continu est plus simple que la représentation discrète. / The numerical computation of the solutions of equations in physical theories enables scientists to make powerful predictions. But numerical computation also challenges physical theories in a more fundamental way. The aim of this dissertation is to show how numerical computation leads to a reformulation of physical theories. Fundamental laws and first principles usually formulated with differential equations are reformulated with discrete equations. To fulfill this goal, I focus on the case of classical mechanics. I study a discrete approach called discrete mechanics developed since the 1980's and I discuss its consequences on the usual continuous representation of time in physics. First, I study numerical computation as a means to make predictions in physics. The fundamental concepts of exact and numerical computations of differential equations are discussed. In the second part, I examine how numerical computation changes the fundamental principles of physical theories. I claim that discrete mechanics has to be considered as a new theory of classical motion. In a third part, I investigate the consequences of discrete mechanics on the continuous representation of time in physics. I claim that physicists do not have to necessarily represent time as continuous in their theories. The discrete representation is another possible choice. Finally, I compare the continuous representation of time and the discrete one according to criteria of simplicity.
|
8 |
Développement d’un macroélément pour l’étude des fondations superficielles sous charge sismique / A macroelement based model for the seismic study of shallow foundationsAbboud, Youssef 28 September 2017 (has links)
Cette thèse vise à développer une méthode pour la justification des fondations superficielles sous charge sismique dans le cadre du nouveau zonage sismique de la France, entré en vigueur en 2011 et des justifications post Fukushima. Elle s’inscrit dans le cadre d’un contrat de recherche entre l’IFSTTAR et EDF CEIDRE.Un modèle basé sur le concept de macroélément est développé pour étudier l’interaction sol-structure (ISS) en prenant en compte les différentes non linéarités. Sa formulation se base sur la théorie de l’élastoplasticité et s’inspire des normes en vigueur (Eurocodes 7 et 8) et. Les différents paramètres sont définis à partir d’essais au laboratoire ou in situ, ou à partir de simulations numériques en conditions statiques. Les coûts de calcul sont réduits du fait que les non linéarités liées à l’interaction sol-structure sont concentrés en des points particuliers du modèle de calcul. L’avantage du macroélément réside dans une formulation en efforts et déplacements, ce qui facilite son utilisation pour la justification des fondations (capacité portante, glissement, décollement, tassements, translations, distorsions et rotations).Le macroélément est implémenté dans le code par éléments finis CESAR LCPC et permet de simuler le comportement statique et sismique d’une fondation superficielle. Trois approches pour la modélisation de la radiation des ondes sismiques dans le sol sont comparées en considérant des chargements statiques et sismiques.Ensuite, des études paramétriques sont réalisées sur une structure en mettant en jeu plusieurs signaux réels. L’influence des différents paramètres de nocivité sur le comportement de la structure est étudiée.Le comportement statique et sismique d’un ouvrage réel est aussi analysé. Il s’agit d’un bâtiment fondé sur un radier reposant sur un sol stratifié. L’aléa sismique est défini par 5 accélérogrames d’accélération maximale égale à 0.4g. Des justifications normatives sont menées en se basant sur les résultats des différentes simulations réalisées / This PhD work concerns the elaboration of a method to verify the seismic sustainability of shallow foundations considering 2011 seismic zoning of France. It is a part of a research contract between EDF CEIDRE and IFSTTAR.To this end, a macroelement based model is developed in order to assess nonlinear soil structure interaction. The elastoplastic formulation of the macroelement constitutive model is compliant with the classical plasticity theory. The formulations for the plastic mechanisms are inspired from the applied standard (Eurocodes 7 & 8). The rate dependent response and the effects of the embedment and the soil inertia efforts are taken into account. The parameters for the constitutive model are defined from laboratory or field tests, or calibrated from static finite element method simulations. The calculation cost is significantly reduced due to the simplified modelling of the soil and its non linearities. Another advantage is that the macroelement based tool is formulated in terms of generalized variables (forces and displacements): this promotes its application in the verification of the sustainability of shallow foundations (bearing capacity, sliding, overturning, settlements, translations, rotations and distortions).The macroelement is implemented in the Finite Element software CESAR LCPC. It allows to simulate the static and the seismic behaviour of a shallow foundation. Three alternative approaches to assess SSI through this model are possible. These alternative approaches are explained and tested under static and seismic load.Then, it is used to perform parametric studies involving various input motions derived from earthquake recordings. The seismic response of a simple structure is studied with respect to the input motion key parameters.Finally, the static and seismic behaviour of a real structure is analysed. The structure is founded on a large raft foundation laying on a multi-layered soil. The seismic hazard is defined by five 0.4 g-PGA accelerograms. Verification to the applied standards is performed on the base of the simulation results, considering many features of the seismic behaviour
|
9 |
Investigations in Computer-Aided Mathematics : Experimentation, Computation, and Certification / Investigations en Mathématiques Assistées par Ordinateur : Expérimentation, Calcul et CertificationSibut Pinote, Thomas 04 December 2017 (has links)
Cette thèse propose trois contributions aux preuves mathématiques assistées par ordinateur. On s'intéresse non seulement aux preuves reposant sur le calcul, mais aussi aux preuves formelles, qui sont àla fois produites et vérifiées à l'aide d'un logiciel appelé assistant à la preuve.Dans la première partie, nous illustrons le thème de l'expérimentation au service de la preuve en nous intéressant au problème de la complexité des algorithmes de multiplication matricielle. Cette question a historiquement été posée de manière de plus en plus abstraite: les approches modernes ne construisent pas d'algorithmes explicites mais utilisent des résultats théoriques pour améliorer la borne inférieure sur la célèbre constante oméga. Nous sommes revenus à une approche plus pratique en essayant de programmer certains des algorithmes impliqués par ces résultats théoriques. Cette approche expérimentale a révélé un motif inattendu dans des algorithmes existants. Alors que ces algorithmes contiennent une nouvelle variable epsilon dont la présence est réputée les rendre impraticables pour des tailles de matrices raisonnables, nous avons découvert que nous pouvions construire des algorithmes de multiplication matricielle en parallèle sans epsilon avec une complexité asymptotique qui peut théoriquement battre l'algorithme de Strassen pour les multiplications. Un sous-produit de cette exploration est un outil symbolique en Ocaml qui peut analyser, composer et exporter des algorithmes de multiplication matricielle. Nous pensons aussi qu'il pourrait être utilisé pour construire de nouveaux algorithmes pratiques de multiplication matricielle.Dans la deuxième partie, nous décrivons une preuve formelle de l'irrationalité de la constante zeta(3), en suivant la démonstration historique due à Apéry. L'étape cruciale de cette preuve est d'établir que deux suites de nombres rationnels satisfont une surprenante récurrence commune. Il est en fait possible de "découvrir"cette récurrence en utilisant des algorithmes symboliques, et leurs implémentations existantes dans un système de calcul formel. De fait,ce travail constitue un exemple d'une approche dite sceptique de la démonstration formelle de théorèmes, dans lequel des calculs sont principalement réalisés par un logiciel efficace de calcul formel puis vérifiés formellement dans un assistant à la preuve. Incidemment, ce travail questionne la valeur des certificats de télescopage créatif comme preuves complètes d'identités. Cette preuve formelle est également basée sur de nouvelles bibliothèques de mathématiques,formalisées pour ses besoins. En particulier, nous avons formalisé et simplifié une étude du comportement asymptotique de la suite ppcm(1,.., n). Ce travail est conduit dans l'assistant à la preuve Coq et prolonge les bibliothèques Mathematical Components.Dans la dernière partie, nous présentons une procédure qui calcule les approximations d'une classe d'intégrales propres et impropres tout en produisant simultanément un preuve formelle Coq de la correction du résultat de ce calcul. Cette procédure utilise une combinaison d'arithmétique d'intervalles et d'approximations polynomiales rigoureuses de fonctions. Ce travail utilise crucialement les possibilités de calculer efficacement à l'intérieur de la logique sous-jacente au système Coq. Il s'agit d'une extension de la bibliothèque CoqInterval d'approximation numérique d'une classe d'expressions réelles. Sa mise en œuvre a également donné lieu à des extensions de la bibliothèque Coquelicot d'analyse réelle, notamment pour améliorer le traitement des intégrales impropres. Nous illustrons l'intérêt de cet outil et ses performances en traitant des exemples standards mais non triviaux de la littérature, sur lesquels d'autres outils se sont en certains cas révélés incorrects. / This thesis proposes three contributions to computer-aidedmathematical proofs. It deals, not only with proofs relying oncomputations, but also with formal proofs, which are both produced andverified using a piece of software called a proof assistant.In the first part, we illustrate the theme of experimentation at theservice of proofs by considering the problem of the complexity ofmatrix multiplication algorithms. This problem has historically beenapproached in an increasingly abstract way: modern approaches do notconstruct algorithms but use theoretical results to improve the lowerbound on the famous omega constant. We went back to a more practicalapproach by attempting to program some of the algorithms implied bythese theoretical results. This experimental approach reveals anunexpected pattern in some existing algorithms. While these algorithmscontain a new variable epsilon whose presence is reputed to renderthem inefficient for the purposes of reasonable matrix sizes, we havediscovered that we could build matrix multiplication algorithms inparallel without epsilon's with an asymptotic complexity which cantheoretically beat Strassen's algorithm in terms of the number ofmultiplications. A by-product of this exploration is a symbolic toolin Ocaml which can analyze, compose and export matrix multiplicationalgorithms. We also believe that it could be used to build newpractical algorithms for matrix multiplication.In the second part, we describe a formal proof of the irrationality ofthe constant zeta (3), following the historical demonstration due toApéry. The crucial step of this proof is to establish that twosequences of rational numbers satisfy a suprising commonrecurrence. It is in fact possible to "discover" this recurrence usingsymbolic algorithms, and their existing implementations in a computeralgebra system. In fact, this work is an example of a skepticalapproach to the formal proof of theorems, in which computations aremainly accomplished by an efficient computer algebra program, and thenformally verified in a proof assistant. Incidentally, this workquestions the value of creative telescoping certificates as completeproofs of identities. This formal proof is also based on newmathematical libraries, which were formalised for its needs. Inparticular, we have formalized and simplified a study of theasymptotic behaviour of the sequence lcm(1,..., n). This work isdeveloped in the Coq proof assistant and extends the MathematicalComponents libraries.In the last part, we present a procedure which computes approximationsof a class of proper and improper integrals while simultaneouslyproducing a Coq formal proof of the correction of the result of thiscomputation. This procedure uses a combination of interval arithmeticand rigorous polynomial approximations of functions. This work makescrucial use of the possibility to efficiently compute inside Coq'slogic. It is an extension of the CoqInterval library providingnumerical approximation of a class of real expressions. Itsimplementation has also resulted in extensions to the Coquelicotlibrary for real analysis, including a better treatment of improperintegrals. We illustrate the value of this tool and its performanceby dealing with standard but nontrivial examples from the literature,on which other tools have in some cases been incorrect.
|
10 |
Caractérisation macroscopique du milieu végétal pour les modèles physiques de feux de forêts / Macroscopic characterization of the vegetal medium for physical forest fire modelingLamorlette, Aymeric 14 October 2008 (has links)
La description aux échelles macroscopiques et gigascopiques des feux de forêts permet l'établissement de modèles physiques aptes à représenter l'évolution d'un feu avec une meilleure précision que les modèles empiriques de type Rothermel développés jusqu'alors. Cependant ces modèles nécessitent l'ajustement de paramètres dont la mesure directe est impossible, car les équations associées à ces modèles ne sont pas relatives à l'air et à la matière végétale mais aux milieux équivalents à la végétation pour l'échelle considérée. Les propriétés des milieux équivalents sont alors liées aux propriétés des milieux les constituant, mais la connaissance des propriétés des milieux constitutifs ne permet pas de connaître directement les propriétés du milieu équivalent. Ce travail consistera tout d'abord en la reconstruction du milieu végétal à l'aide d'outils issus de la géométrie fractale. Des méthodes de mesures de paramètres géométriques venant de la foresterie ont ensuite été utilisées pour valider nos modèles de végétation. Enfin, des expériences numériques ont été menées sur nos structures reconstruites afin d'identifier les paramètres macroscopiques qui nous intéressent. Ces expériences permettent également de valider ou non les hypothèses effectuées lors de l'établissement des équations du milieu équivalent. Les paramètres ajustés sont la viscosité du milieu équivalent, le coefficient d'échange convectif et le coefficient d'extinction / The macroscopic and gigascopic scale description of forest fires allows physical modelings of the propagation which can predict the fire evolution with a better accuracy than usually developed empirical Rothermel-like models. However, those models need fitting for their parameters which cannot be measured directly as the models equations are related to the equivalent media at the considered scale and not related to the air and the vegetal material. The equivalent media properties are related to the inner media properties, but the inner media properties knowledge does not allow directly the equivalent media properties knowledge. This work is then aiming on the vegetal medium reconstruction using fractal geometry. Geometrical parameters measurement methods used in forestry sciences are applied for the vegetal modeling validation. Numerical studies are finally done on the reconstructed structures to fit the relevant macroscopic scale parameters. Those studies also allow us to validate or invalidate the assumptions which have been done for the equivalent medium equation development. Those parameters are: the equivalent medium viscosity, the convective heat transfer coefficient and the extinction coefficient
|
Page generated in 0.0647 seconds