Arrêt de service programmé du vendredi 10 juin 16h jusqu’au lundi 13 juin 9h. Pour en savoir plus
Accéder directement au contenu Accéder directement à la navigation
Rapport

A Coq Formalization of the Bochner integral

Résumé : L'intégrale de Bochner est une généralisation de l'intégrale de Lebesgue pour des fonctions à valeurs dans un espace de Banach. Sa définition mathématique et sa formalisation dans l'assistant de preuve Coq en sont donc plus difficiles puisque l'on ne peut pas s'appuyer sur les propriétés des nombres réels. Nos contributions incluent une formalisation originale des fonctions simples, l'intégrabilité de Bochner définie par un type dépendant, et la construction de la preuve de l'intégrabilité de fonctions mesurables sous une hypothèse de séparabilité faible. Puis, nous définissons l'intégrale de Bochner et prouvons plusieurs théorèmes, dont la convergence dominée et l'équivalence avec une formalisation préexistante de l'intégrale de Lebesgue pour les fonctions mesurables positives.
Liste complète des métadonnées

https://hal.inria.fr/hal-03516749
Contributeur : Francois Clement Connectez-vous pour contacter le contributeur
Soumis le : jeudi 10 février 2022 - 13:23:27
Dernière modification le : lundi 16 mai 2022 - 17:00:06

Fichiers

RR-9456.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-03516749, version 2
  • ARXIV : 2201.03242

Citation

Sylvie Boldo, François Clément, Louise Leclerc. A Coq Formalization of the Bochner integral. [Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022. ⟨hal-03516749v2⟩

Partager

Métriques

Consultations de la notice

117

Téléchargements de fichiers

68