Arzela main lemmas

[zstone1]

This has the hard parts of Arzela-Ascoli. The forward direction is done, but the backwards direction still needs a little work to get it done fully. But this is an appropriate place to stop, considering the size of the change already.

1. We introduce a sets_of filter that, given a filter over T, gives a filter over set T which has the "small" sets. That is, it's the filter of downward closed members of F. The purpose of this is to let us write near (sets_of entourage) to get an "epsilon" without having a metric space and using posnum. This is super practical for both of the main lemmas.

2. I have a near_compact_cover lemma which dramatically factors out the two main lemmas. It let's us factor a quantifier out of a \near, turning a "global" property into two local ones. The analogy to open coverings is that if you can index an open cover by a filter (E.G. some epsilon), you can construct a filter which converges to counter-examples.

3. The theorems themselves compact_equicontinuous and ptws_compact_cvg (names could be improved). Thanks to the two tools above, they are fairly short. But the topology is indeed tricky.

4. I still need to update the changelog. I'm also sure there's a bunch of linting I missed.

I ran into some rather frustrating trouble with the \near notation where the near lemma did not like the g \near (nbhs f) that was in scope. Sometimes it was conflicting stuff in the evar's context (I had to try to define everything possible before entering the near to avoid this. Why can't it unfold context elements it doesn't recognize to see if they're defined in terms it does know?). Other times I'm not really sure what was wrong. I can provide repros if you all want.

The only remaining steps for Arzela Ascoli are:

• Prove uniform limits of continuous functions are continuous (I think this is easy from the cvg_switch?)
• The next meaningful lemma takes compact_equicontinuous and weakens the condition to only require precompact instead of compact
• Then the final step is to prove a weaker, but highly practical version that says

{ptws F --> f} /\ F is equicontinuous -> {family compact, F --> f}

[CohenCyril]

sets_of sounds too generic a name, do you have another suggestion?

[zstone1]

That's true. I've updated with powerset_filter_from which is marginally better. Maybe small_set_filter_from is more descriptive?

[CohenCyril]

This is really nice. I'd love to see the reproduction of the problems with near that you mentioned. And yes, the no-unfolding stuff is annoying, since we piggyback on Coq evar we should introduce the unfolding in the tactic, but it needs to be smart and thus be reprogrammed in another metalanguage (e.g. ltac2 or coq-elpi), which I meant to do at some point anyways.

[zstone1]

Thank you, I'm pretty happy with how it worked out. I still have some questions about near_compact_covering to think about. In particular, I'm very much hoping the converse is false, because means there's a possibility of a novel generalization of arzela-ascoli.

I will post a branch with the broken near application once this is merged.

Also, I remember @affeldt-aist mentioned something about uniform series convergence proofs (in R or C). Once this is merged, you can use ptws_compact_cvg + local compactness. (I believe it'll be easier to formalize this way, rather copying textbook proofs that use Weierstrass M-test and deal with boundary conditions).

[zstone1]

Well, it was a nice thought. I have a proof of the converse of near_compact_covering. I'll post it separately once I clean it up.

[CohenCyril]

Good to go