2019 05 07 Meeting

Integration

Not based on measure

• Riemann
  • Coq, Coquelicot
  • no continuous probabilities
  • no
• HK - Gauge
  • HOL Light
  • extends Riemann et Lebesgues
  • some properties are not stable
  • no
• Riemann-Stieljes
• Daniell

All notions suffer from not using measure and this causes problems for modularity and theorems relying on measurable functions such as Fubini.

Based on measure

• Lebesgues
• Lebesgues-Stielges