Integration

Not based on measure

• Riemann
  • Coq, Coquelicot
  • no continuous probabilities
  • no
• HK - Gauge
  • HOL Light
  • extends Riemann et Lebesgue
  • 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

• Lebesgue
• Lebesgue-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

1. Divide the work in two parts using a module interface for Lesbesgue integral. In this interface:

• intergal has three parameters: domain, function, measure.
• the Lebesgue measure is provided as well.

2.A. Do the theory of this interface

2.B. Instantiation of this interface

2.C. Use of this symbol (provide statements of theorems for 2.A. to prove)