Una visión general completa del teorema de diferenciación de Lebesgue en Coq

La formalización del análisis real ofrece la oportunidad de reconstruir pruebas tradicionales de teoremas importantes como teorías inequívocas que pueden ser exploradas interactivamente. Este artículo proporciona una visión general completa del teorema de diferenciación de Lebesgue formalizado en el asistente de prueba Coq, del cual se obtiene como un corolario el primer teorema fundamental del cálculo (FTC) para la integral de Lebesgue. Probar el primer FTC de esta manera tiene la ventaja de descomponerse en teorías débilmente acopladas de tamaño moderado y de interés independiente que se prestan bien al desarrollo incremental y colaborativo. Explicamos cómo formalizamos todos los constructos topológicos y todos los lemas estándar necesarios para eventualmente relacionar las definiciones de derivabilidad y de integración de Lebesgue de MathComp-Analysis, una formalización de análisis desarrollada sobre la biblioteca Mathematical Components. En el transcurso de este experimento, enriquecemos sustancialmente MathComp-Analysis e incluso ideamos una nueva prueba para el lema de Urysohn.