A Coq formalization of Lebesgue integration of nonnegative functions
From MaRDI portal
Publication:2673304
Recommendations
Cites work
- A garden of integrals
- An Isabelle/HOL formalisation of Green's theorem
- Canonical Big Operators
- Coquelicot: a user-friendly library of real analysis for Coq
- Dual of the class of HK_r integrable functions
- Formalization of real analysis: a survey of proof assistants and libraries
- Fubini's theorem
- Functional Analysis and the Feynman Operator Calculus
- Fundamentals of nonparametric Bayesian inference
- Generalized ordinary differential equations and continuous dependence on a parameter
- scientific article; zbMATH DE number 5841426 (Why is no real title available?)
- scientific article; zbMATH DE number 3173784 (Why is no real title available?)
- scientific article; zbMATH DE number 3491650 (Why is no real title available?)
- scientific article; zbMATH DE number 3575883 (Why is no real title available?)
- scientific article; zbMATH DE number 1324223 (Why is no real title available?)
- scientific article; zbMATH DE number 481023 (Why is no real title available?)
- scientific article; zbMATH DE number 635667 (Why is no real title available?)
- scientific article; zbMATH DE number 1022658 (Why is no real title available?)
- scientific article; zbMATH DE number 1549895 (Why is no real title available?)
- scientific article; zbMATH DE number 3806227 (Why is no real title available?)
- scientific article; zbMATH DE number 765034 (Why is no real title available?)
- scientific article; zbMATH DE number 6146040 (Why is no real title available?)
- scientific article; zbMATH DE number 6413793 (Why is no real title available?)
- scientific article; zbMATH DE number 3220452 (Why is no real title available?)
- scientific article; zbMATH DE number 3240665 (Why is no real title available?)
- scientific article; zbMATH DE number 3247316 (Why is no real title available?)
- scientific article; zbMATH DE number 3249395 (Why is no real title available?)
- scientific article; zbMATH DE number 3291139 (Why is no real title available?)
- scientific article; zbMATH DE number 3301572 (Why is no real title available?)
- scientific article; zbMATH DE number 3395017 (Why is no real title available?)
- scientific article; zbMATH DE number 3027621 (Why is no real title available?)
- Introduction to nonparametric estimation
- Isabelle/HOL. A proof assistant for higher-order logic
- Measure theory
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- On the formalization of the Lebesgue integration theory in HOL
- Probability
- The finite element methods for elliptic problems.
- The flow of ODEs
- The Lean theorem prover (system description)
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Theory and practice of finite elements.
- Three chapters of measure theory in Isabelle/HOL
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
Cited in
(6)- Proving tight bounds on univariate expressions with elementary functions in Coq
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Measure construction by extension in dependent type theory with application to integration
- A Coq formalization of Lebesgue induction principle and Tonelli's theorem
- A Coq Formalization of Lebesgue Integration of Nonnegative Functions
- Fourier series formalization in ACL2(r)
This page was built for publication: A Coq formalization of Lebesgue integration of nonnegative functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2673304)
