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

Biblio:

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

Sujets

• Definition of sigma-algebra (interface)
• Definition of measure (interface)
• Definition of Lebesgue measure, Carathéodory Theorem (instance)
• Definition of integral (parametrized par mesure)
• Fréchet-Riesz Theorem
• Fubini Theorem, Fatou Lemma, Dominated convergence theorem
• Radon–Nikodym theorem

Roadmap

Divide the work in two parts using a module interface for Lesbesgue integral.