-
Notifications
You must be signed in to change notification settings - Fork 43
2019 05 07 Meeting
Cyril Cohen edited this page May 7, 2019
·
13 revisions
- 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.
- Lebesgue
- Lebesgue-Stielges
- small extention
- same architecture
- 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
- 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
- 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)