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
  • small extention
  • same architecture

Roadmap

• Biblio:
  • Analyse Reelle Et Complexe Cours Et Exercices, Walter Rudin
  • Cours de mathématiques-2 Analyse, Jean-Marie Arnaudiès et Henri Fraysse