Total variation

[zstone1]

Motivation for this change

Bounded variation stuff to build the lebesgue stieljes charge. The end goal being applying radon nikodym for FTC.
This 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.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

Here is a tentative to use path to define partition (that I renamed division because partition is a bit overloaded): https://github.com/affeldt-aist/analysis/blob/total_variation/theories/realfun.v#L680

I haven't yet completely ported the continuity proofs though (and the rest is still dirty but that can give a good idea of the difference).

[affeldt-aist]

The last commit redefines partition (renamed itv_partition to avoid overloading) using path and reproves the basic theory. The reimplementation is transparent enough so that the last bit of the development (about TV and continuity) is left unchanged.

[affeldt-aist]

the notation nondecreasing_fun and nonincreasing_fun have been introduced in realfun.v in the meantime

[affeldt-aist]

this lemma is now in normedtype.v and named cvg_at_leftNP

[affeldt-aist]

(I just made a few comments to mark a few lemmas that made their way into master recently.)

[affeldt-aist]

(If the itv_partition/bounded_partition/total_variation looks stable enough, we could maybe make a separated PR to merge it asap?)

[zstone1]

Cleaning up the duplicate lemmas and notations sounds good. Other than the admits, is there anything else required? I can make an attempt on those today/tomorrow.

[zstone1]

I filled in that last admitted. The statement of the admit was incorrect. That is

 {within `[a,b], continuous f} <-> {in `],a,b[, continuous f} /\ f ^'+a --> f a /\ f^'-b --> f b

is false. It needs a<b. Note that strictness is required, as even when a = b the LHS is trivially true, and the boundary conditions on the RHS are non-trivial. Thankfully a<b was already in scope, so it's simple to fix.

I've been working in Coq for 4 years now, and I'm still regularly caught of guard by how pedantic it is. Every time I try to use admits in my workflow I make a mistake like this. I'm just glad this one didn't involve any major rework.

[affeldt-aist]

I made a first pass for minor checks.
I could streamline a few proof scripts, fix comments
and naming, do some renaming, remove one or two unused lemmas.
The lemma path_lt_last_filter (my bad) still looks a bit ad hoc
but I couldn't find a generalization right away.
The name total_variation_jordan_decompE does not really
correspond to the elements used in the statement.
What about bounded_variation_neg_tvE?

[zstone1]

Changed jordan_decompE lemma to be

Lemma bounded_variation_pos_neg_tvE a b f : BV a b f ->
  {in `[a, b], f =1 (fine \o pos_tv a f) \- (fine \o neg_tv a f)}.

which is a little bit more obvious. As far as path_lt_last_filter goes, I agree it doesn't yield an immediate generalization in this context. I'm not sure how to improve it, so I'm fine with it's current state.

[affeldt-aist]

@IshiguroYoshihro Since you have been playing around with the definitions in this PR, could you take a quick look to see if there is something we can improve?

[affeldt-aist]

cd4bf11
is just the observation that we can write variation with next and prev from path.v.
This feels natural and I was therefore hoping that it would help reduce the size of the proof of variation_itv_partitionLR
which is the only lemma that uses variationE (variation using zip) but I failed.
The proof is getting much longer because of low-level manipulations of index and nth (that shows up because
of next_nth and prev_nth). Am I using the path library the wrong way?
In any case, aren't variation_next and variation_prev worth keeping around?

[zstone1]

Oh, nice. A bit sad it doesn't clean up the proof, but it should allow for nicer "term-by-term" comparisons in the future, so you should merge those in regardless.