adding domain restrictions and compact convergence

[zstone1]

EDIT by Cyril: reopened as PR #462

With an eye towards more interesting complex analysis, the topology of compact convergence is missing from the topologies defined here. So I've added it, in a slightly roundabout way.

Summary

The main issue is that if A is a compact set in U, there's no nice way to define a function from (A -> V). While I could use some dependent pairs to turn A into a type, it's going to interfere with differentiability definitions. The whole system is really built around function from R (or C). Turns out this is quite solvable.

The approach I'm using is to build a quotient like topology on (U -> V) that's effectively the same as the one I'd want for (A -> V). In particular, convergence depends on the A portion of functions. The main downside of this approach is that the topology is not hausdorff. The following result (proved in the PR), I expect to be good enough in practice.

forall (f g : A ~~> V), hausdorff V ->  eq_on A f g = close f g.

Next, I define a topology for convergence on a family of sets in terms of the supremum topology (thanks to whoever wrote that! Big time saver). There's a dependent pair here, but it's largely under the hood. One of the key facts for complex analysis in practice is that it's enough to prove convergence on squares. I prove a general form of this fact about finite coverings.

Then finally I define the topology I care about. A ~cc~> V.

Points of interest

1. Is the way I'm using these structures make sense? I've never really worked with this kind structure packing stuff before, so I'm just making it up as I go along.

2. Is the notation that I've introduced reasonable? For these non-canonical structures, I'm introducing a notation of "standard" uniform convergence ~~>, restricted uniform convergence ~~>_(A). And lastly, uniform convergence for a family as ~fam~>.

3. The proof techniques are... a bit sloppy sometimes. Like I need to do an induction with a \'bigcup over a finite set. I do some nasty casing, and an explicit call to finSet_rect. Something seems wrong with this.

4. In terms of axioms, I really need membership of A to be decidable. Seems like deciding stuff with asbool is the way to go, just want to be sure I'm following the convention here.

5. Naming/style conventions. Not all of the names I've chosen are reasonable. Suggestions are quite welcome.

6. There are lots of helper lemmas that are not really intended for use outside these proofs. Is there a nice way to indicate those?

Next steps

arzela ascoli is for compact convergence would be nice. Separately, there is some complex analysis stuff to do. Like show that the geometric series converges compactly on the unit ball.

[CohenCyril]

Hi @zstone1 thank you for your contribution. At first glance, it is interesting and I have many remarks to make but I am very short in time during this period of the year.

Just so you know, your restriction mechanism is akin to the one used in group theory {morphism G -> gT'} (where G is a subgroup of an enclosing groupe type gT).

You might also be interested in PR #224

[zstone1]

Ah, thanks for the heads up about the integral PR. And no worries on time. I'd love to hear your thoughts when you get to it.

[CohenCyril]

Hi, @zstone1 I have many remarks and questions about this PR, but I'll start "small": would you consider using function restriction like this one?

analysis/theories/csum.v

Lines 46 to 48 in 0eaabe8

	Definition fer T (R : realDomainType) (f : T -> {ereal R}) (D : set T) :=
	fun x => if `[<D x>] then f x else 0%E.
	Local Notation "f \|_ D" := (fer f D).

(defined in #294 and used in #224)

In your case, since you don't have 0, you could use point from pointedType instead (which we should make sure always coincides with 0 in Z-modules). Would that be a reasonable assumption that all your codomains are pointed?

[zstone1]

Thanks for this, it's an interesting point. First of all, pointedType is a very reasonable assumption. I think I already am assuming it everywhere. Second, I have a patch function which behaves similarly. For a given set A, the function patch_point A := patch A (fun=> point) is exactly the restriction you're recommending.

I did consider such restrictions, and I don't have a good reason to use dependent pairs over restriction functions. It looks like the restriction functions will fit better into the existing paradigm, so I'm happy to make that change. It should be quite straightforward. On the other hand, I believe the "exploded" topology has the advantage of using the same filter everywhere. The only way I could figure out to use that patch_point A function was to say

F ~~>_(A) :=  ((patch_point A) @` F --> (patch_point A f))

But then, for defining convergence over a family of sets, we'd need

forall A, fam A -> (patch_point A) @` F --> (patch_point A f)

Now we've got different filters for each set. So I can't really use the nice sup_topology stuff. My goal was to make the definition

Notation "F ~ famA ~> f" := 
  (F --> (f : family_cvg_topologicalType famA)) (at level 100).

as clean as possible. This also should prevent having to sprinkle in excess restrictions at application time.

That being said, in another draft PR I just posted, I prove that geometric series converge compactly. I ended up using cvg_restrict_dep anyway. So when it comes to proving things converge over families, having the clean definition didn't help much. So if it ends up that all of the sup_topology stuff is a distraction, then I'm fine to remove it, and just use the restriction definitions.

Does this explain my reasoning clearly? If I've missed something, please let me know. I'd love to simplify the PR.

[CohenCyril]

I agree that restrictions using dependent types might not be the most usable in general, though it could sometimes prove useful. When one stays with topology and more generally non algebraic structures, they might be ok (even if one has to pay the price of going back and forth a type and its subtype, it could be manageable). When one enters the realm of algebra, the predicate must satisfy more structure. So it's ok to keep them as a side tool, provided the theory is done once and applied to the other.

About changing the topology on spaces of function, while it is unavoidable for the pointwise one, maybe the best strategy would be to change the topology on the domain using within, e.g. by having a canonical structure on an alias of the domain e.g.

Definition restrict_type U (A : set U) := U.
Notation "U `\_ A" := (restrict_type U A) : type_scope.

Then, filters on F --> (f : U`\_A -> _) correspond to your current F ~~>_(A) f (I hope, please check I'm not saying something wrong).

[zstone1]

I remember trying something like that, but gave up. The uniform topology for functions doesn't use a topology on the domain; it's just a choiceType. (I'll admit this detail surprised me.) This line of thinking is how I ended up with dependent pairs in the first place. I agree with the approach wholeheartedly, though. Only altering the function domain would be quite elegant. But I never figured out how to do it. I suspect it's not possible, but don't have any supporting evidence.

[CohenCyril]

Only altering the function domain would be quite elegant. But I never figured out how to do it. I suspect it's not possible, but don't have any supporting evidence.

Ah right, I understand the problem, I think this could be done by adding some machinery that try to detect a restriction of a domain for the product topology....

[CohenCyril]

Then I guess a solution would be to have a type {restricted A -> T} function (note that in the mathcomp tradition, annotation of the sort are prefered over LaTeX style subscripts of the arrow, and that we use curly brackets for types and square brackets for terms).

[zstone1]

Ok, that's quite reasonable. I've updated the proofs with the new syntax, as well as the docs. All this raises a (possibly out of scope) question. Should U -> V have a canonical topology? I'm not sure I why uniform is a better choice than pointwise. Even though removing the Canonical declaration would force people to be explicit about their topologies, new syntax is a fairly lightweight way to annotate it. And when you're working with only one kind of convergence, the existing F --> f (vs {unif, F --> f} ) notation still works just fine.

[affeldt-aist]

There is maybe a need for one more pass of linting.

[zstone1]

Ok, three things done:

1. I've created aliases for U -> V for each topology, and given the canonical filters, topologies, uniform, as appropriate. I kept all the same notations. I believe this is the requested change, but please correct me if I'm wrong.
2. I've added a new function restrict which is just patch with (fun=> point). I've kept the patch function. Is this ok, or would you prefer I do some more substantial renaming?
3. I've proven that restrict in the uniform topology behaves like the restricted topology.

Are there any other blockers for merging this?

[affeldt-aist]

I tried to use pred instead of set in patch following what was said during the last meeting.

[CohenCyril]

@zstone1 sorry for taking so much time to review. Please ask if something is unclear about my review.

[CohenCyril]

It would be nice to have the bigcupD1 and bigcapD1 as in mathcomp bigD1.

[zstone1]

Agreed, although I would prefer to do it as a separate pull request.

[affeldt-aist]

I also missed them in another PR, hence PR #409

[zstone1]

Ah, those notations suggestions are a nice improvement. I will address these issues this week.

Separately, I had a realization that I can define {uniform A -> V} as the weak topology of restrict_dep A : (X -> Y) -> ({x : X| x \in A} -> Y). I believe this will save several hundred lines of proofs, but I can't be sure until I try.

[zstone1]

Alright, I believe I've updated all the issues you identified. Also, using the weak topology of the restriction map has saved saved nearly 300 lines, and removed many of the awkward internal lemmas, such as all the explode stuff.

[CohenCyril]

Hi, I'm going to make a pass on this one next week.

[CohenCyril]

@zstone1 please never merge master into a PR, use rebase instead with squashing when necessary.
However please do not touch it for now, I will be working on it it's ok with you.

[zstone1]

Just wanted to check the status of this diff. Is there anything I can do here?

[CohenCyril]

Just wanted to check the status of this diff. Is there anything I can do here?

I am back from vacation, I will attend this matter asap now.

[CohenCyril]

@zstone1 I pushed some refactorings in the branch domain_restriction, I need to do a proper rebase and update the changelog. May I force-push on your zstone1:master branch?

[zstone1]

Yes, do whatever you need.

[CohenCyril]

Sorry, when the remote branch is master it makes things really error prone (for me)... I will reopen it under a new branch