Fundamental Theorem of Calculus

[zstone1]

Creating an issue to track the various tasks on the proof of FTC. Apparently it's pretty hard, and requires work from many sources, and we're working on several streams:

Track A: Tietze extension theorem (done)

1. Urysohn (Urysohn's Lemma #900 but the full statement is much easier once HB is done)
2. Urysohn -> Tietze (Tietze's theorem #971)

Track B: Continuous functions are dense in L1 (done)

1. outer regularity (Outer regularity for Lebesgue measure #957)
2. outer regularity -> inner regularity (More measure theory helpers #962)
3. measure cvg (More measure theory helpers #962)
4. measure cvg -> egorov (Egorov's theorem #964)
5. inner regularity + egorov -> lusin (Lusin #966 )
6. Tietze + lusin -> Density of continuous functions in L1 (Continuous functions are dense in L1 #1015 )

Track C: Hardy LIttlewood

1. Vitali Covering Lemma: (tentative formalization of Vitali's lemma #973 )
2. Vitali Covering Theorem (tentative formalization of Vitali's theorem #984) and (corollary to Vitali's theorem #1328)
3. Hardy Littlewood Maximal Inequality (Hardy littlewood #995)

Track D: Putting it all together

1. Lebesgue differentiation for continuous functions (Lebesgue differentiation for continuous functions #972)
2. Hardy littlewood + density -> lebesgue differentiation + FTC 1 (Lebesgue differentiation theorem and applications #1065)
3. radon-nikodym + lebesgue differentiation -> FTC 2 (maybe something hard about absolute continuity)

Memo taken from the conversion of PR #1118 @zstone1
--->8---
The end goal being applying radon nikodym for FTC.
This [PR #1118] proves that if f has bounded variation, it can be decomposed into a positive part and negative part. And that those have sane continuity behaviors.

The remaining bit to apply radon nikodym is

Definition lusinN (A : set R) (f: R -> \bar R) := forall E, E <= A -> measurable A -> mu A = 0 -> mu (f @` A) = 0
Definition absolute_continuity a b f := {within [a,b], continuous f} /\ bounded_variation a b f /\ lusinN [a,b] f. 
Lemma lusinN_TV a b f : absolute_continuity a b f -> lusinN (TV a ^~ f).
Lemma absolute_continuity a b f -> mu << "lebesgue_stiljes_charge f" (should be easy corrolary of lusinN_TV)

That'll give us enough to prove FTC. But to make it useful, we'll also need

Lemma differentiable_lusinN : {in (a,b), differentiable f} -> lusinN (a,b) f

which might be best to go through lipschitz, I'm not sure.
--->8---