Topology of enat

Stream: maths

[Antoine Chambert-Loir]

enat is the type nat extended with an element at infinity. As such, it is a canonically_ordered_comm_semiring, and it gets a topology from this. However, this topology is defined by set.Ici, namely intervals closed on the left and unbounded on the right, which means that the element at infinity is isolated. As a consequence, tending to infinity in enat is quite different from tending to infinity in nat…

Am I missing a point ? Is this an intended property ?

[Yaël Dillies]

Wait, how does it get a topology from this?

[Antoine Chambert-Loir]

You're right, there's no topology, and I use filter.has_top — which precisely is generated by set.Ici.

[Antoine Chambert-Loir]

So I should use another filter in this case, generated by set.Ioi, I don't know whether it exists.

[Yaël Dillies]

docs3#order_topology?

[Antoine Chambert-Loir]

Thanks! That topology is the correct one (obviously, I was missing a point), I will use that one… (It's not an instance, apparently).

[Sebastien Gouezel]

It should probably be a global instance, in fact.

[Antoine Chambert-Loir]

Since docs#ereal.order_topology is already an instance, that would make sense.

(But what I need is lighter: just the other version of docs3#filter.at_top when the ordered set has a top element. I wonder why docs3#filter.at_top has been defined using closed intervals.)

[Sebastien Gouezel]

If you use open intervals, then when there is a top element the at_top filter is trivial (i.e., there is no way to tend to top).

[Yury G. Kudryashov]

What you need is ⨅ n : ℕ, 𝓟(Ioi (n : ℕ∞)) or, equivalently, ⨅ (n : ℕ∞) (_ : n < ⊤), 𝓟(Ioi n)

[Antoine Chambert-Loir]

Exactly, that's how I would naturally define filter.has_top.

[Antoine Chambert-Loir]

(Well, up to the precise Lean syntax which I hadn't sorted out yet.)

[Yury G. Kudryashov]

How would you define it if the type has no top element?

[Yury G. Kudryashov]

⨅ (n : α) (_ : ¬(IsTop n)), 𝓟(Ioi n)? ⨅ (n : α) (_ : ¬(IsMax n)), 𝓟(Ioi n)? Something else?

[Yury G. Kudryashov]

docs#IsTop docs#IsMax

[Antoine Chambert-Loir]

Yes, something mathematically equivalent to that. (Just because I had expected that docs3#filter.at_top would have coincided with the filter of neighborhoods at the top element…)

[Yury G. Kudryashov]

IsTop or IsMax?

[Yury G. Kudryashov]

Anyway, this discussion should wait till after the port.

[Antoine Chambert-Loir]

My only concern would be that the inclusion from the the type to its with_top version gives the same notion of limit at _top.

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

Anyway, this discussion should wait till after the port.

I'm not even insisting that some modification be made. It was a genuine question that appeared when I had misinterpreted the function name and people who have implemented docs#filter.at_top like it is may have serious reasons for which it's done as it is.

[Johan Commelin]

If anything, this suggest that we should have more documentation on atTop

[Antoine Chambert-Loir]

You see, I had read the doc of docs3#filter.at_top, in particular the parenthesis:

(The preorder need not have a top element for this to be well defined, and indeed is trivial when a top element exists.)

However, when using it later on, I forgot about this and naïvely thought that it would be the filter of neighborhoods of ⊤.

(This led to a funny error, by the way, because I detected that error when trying to prove the converse of something I had proved: the proof didn't work out exactly because of this problem, which meant my direct proof proved something different from what I had in mind — converging to docs3#filter.at_top meant that the function was eventually ⊤, and I didn't realize I had made a too strong hypothesis.)

[Kevin Buzzard]

I guess this is a great example of "you're proving theorems about your definitions, so you had better make sure they're right" (what the computer scientists are always warning us about) plus also "if the definitions are wrong then you're going to find out pretty quickly" (which is what the mathematians say to reassure the computer scientists)

[Anatole Dedecker]

This new definition of docs#Filter.atTop would mess with our definition of docs#HasSum right? Because if the index type is finite then Finset \alpha has a top element. I think that with this new definition, a function would only have its (algebraic) sum as a topological sum if it’s zero at at least one point, which is very wrong.

[Anatole Dedecker]

Never mind, this is not true at all.

[Anatole Dedecker]

So I guess I’m in favor of this change then, probably with the IsTop version rather than IsMax because then we make sure to get back our original version in any NoTopOrder

[Floris van Doorn]

@Anatole Dedecker I think you're still right that this gives the wrong answer sometimes, at least for sums on a domain with 1 point (which under the new definition will always be 0) or 0 points (the sum doesn't exist under the new definition).

I think we shouldn't redefine Filter.atTop, but make a new definition (or just use the nhds filter in the order topology).

[Kyle Miller]

I wonder if Filter.atTop should be the inf over principal filters of order filters rather than over principal filters of Set.Ici? Then that would more directly be the filter at a top in the ideal completion of the type (for example, for Nat that's ENat), and I think it would be equivalent.

Then the ENat's infinity filter would be the pushforward of Nat's Filter.atTop

[Kyle Miller]

This suggests that having two different filters like Floris suggested is the right thing to do: there's the infinity filter on the original order and the infinity filter on the completed order.

[Anatole Dedecker]

Floris van Doorn said:

Anatole Dedecker I think you're still right that this gives the wrong answer sometimes, at least for sums on a domain with 1 point (which under the new definition will always be 0) or 0 points (the sum doesn't exist under the new definition).

I think it does still work for 1 point domain, but not for zero. Anyways, this does seem like a bad idea :sweat_smile:

[Anatole Dedecker]

@Kyle Miller What do you mean by "principal filters of order filters" ?

[Kyle Miller]

Filter.atTop = ⨅ (f : Order.PFilter α), Filter.principal f

[Anatole Dedecker]

Ooooooh that's interesting

[Floris van Doorn]

For the one point domain, there are two finsets, empty and univ, so I think the new proposal gives you the filter (⊤ : Filter (Finset Unit)), not 𝓟 (Finset.univ)

[Floris van Doorn]

I'm quite sure Kyle's definition is equivalent to the existing one.

[Anatole Dedecker]

Floris van Doorn said:

For the one point domain, there are two finsets, empty and univ, so I think the new proposal gives you the filter (⊤ : Filter (Finset Unit)), not 𝓟 (Finset.univ)

Yes there are two finsets but one of them is top, so you only consider the empty finset which gives you 𝓟 (Finset.univ), right?

[Anatole Dedecker]

Floris van Doorn said:

I'm quite sure Kyle's definition is equivalent to the existing one.

For ENat at least yes, that would give the current definition.

[Floris van Doorn]

One filter that gives the "right" notion in all the types I've considered so far (ℝ, Finset α, ENat, Nat, finite orders, ...) is

def Filter.atTop'' [Preorder α] : Filter α :=
  ⨅ (n : α) (_ : ¬ IsSuccLimit n ∨ ¬ IsMax n), 𝓟 (Ici n)

This should be the current atTop filter in most cases. Only if there is a maximal element that is not the successor of another element then this filter gives you the notion of "tending to this maximal element" (or all such maximal elements, if you have multiple).
However, this definition is quite ugly, and I don't propose adopting it as the default definition in mathlib.

[Floris van Doorn]

Oh wait, Yury's definition uses Ioi, not Ici, I missed that. You're right, Anatole... I think my suggestion in that case is equivalent to Yury's, and has the same defect for 1-element α's.

[Peter Nelson]

Has there been any progress on this? I've just found myself wanting to sum a function f : α → ℕ∞ over α in such a way that the sum is defined for all f, and has value ⊤ in the infinitely supported case. If I'm not mistaken, this would require tsum with the topology begin talked about here.

[Anatole Dedecker]

Do you mean adding a TopologicalSpace instance on ENat (with the order topology)? I think the answer is no, but I can do that quickly if you need it.

[Peter Nelson]

I guess this would only be useful to me if there were also all the infrastructure would be needed to get tsum working smoothly. If I added the instance myself in Mathlib.Topology.Instances.ENat along with some of this API, would this be well-received?

[Anatole Dedecker]

Of course! Which kind of API specific to ENat do you need for tsum, only that it's a topological monoid or do you need more? But don't hesitate to open a PR in any case!

[Peter Nelson]

As a dyed-in-the-wool combinatorialist, I just want to be able to sum an arbitrary function f : α → ℕ∞so that it has the 'correct' value (ie. equal to ⊤ iff some summand is ⊤ or the support is infinite). In this case, every function should be Summable, so the API for tsum should be very clean. I'll have a tinker.

[Anatole Dedecker]

It's possible that we have to generalize some lemmas about docs#ENNReal to topological monoids with a top element, but apart from that I would naively guess that you don't need that much more API. Let's see how it goes!

[Peter Nelson]

I'm having a little trouble getting the right set of instances. For α to have the property that every function f: ι → α is summable, it seems I need a lemma like this:

import Mathlib.Topology.Algebra.InfiniteSum.Basic
import Mathlib.Topology.Order.Basic
import Mathlib.Data.Finset.Sum
import Mathlib.Topology.Instances.ENNReal

open scoped BigOperators

theorem hasSum {α ι : Type _} [CanonicallyLinearOrderedAddMonoid α] [CompleteLattice α]
    [TopologicalSpace α]  [OrderTopology α] {f : ι → α} :
    HasSum f (⨆ s : Finset ι, ∑ a in s, f a) := by
  sorry
  -- Proof should be
  -- exact tendsto_atTop_iSup fun _ _ => Finset.sum_le_sum_of_subset

The canonicality is needed because (for instance) this would fail for the extended reals, and the completeness is needed for the statement to even make sense. But the problem is that the first two instances contain orderings as data, so a mismatch occurs with the obvious proof. Is there a way around this?

[Jireh Loreaux]

You could phrase this in terms of docs3#with_top.complete_linear_order. It probably wouldn't apply directly to ENat or ENNReal, but these lemmas could be proven directly as a consequence of this one.

[Jireh Loreaux]

To be clear, you assume alpha is a ConditionallyCompleteLinearOrderBot, and then the lemma is that a function into WithTop alpha is summable. And you get the complete lattice structure for free from the instance mentioned above.

[Jireh Loreaux]

Oops, sorry, that doesn't work. There's no additive structure. Sorry!

[Peter Nelson]

Yeah, it’s the ‘additive order’ and the ‘completeness order’ that are clashing

[Anatole Dedecker]

I don't think the canonicity the right way to avoid problems here, what you really need is the fact that all elements are positive. Actually, I'm surprised we don't have this lemma for any summable and nonnegative f

[Anatole Dedecker]

I think what we could have is some ZeroLEClass or ZeroBotClass that would do that, but in the meantime you can (1) prove the general lemma I described above, using docs#Finset.sum_le_sum_of_subset and (2) specialize it to ENat without the nonnegativity assumption

[Anatole Dedecker]

Or maybe the right solution is to say that the nonnegativity argument of the general lemma should be solved by positivity, but I never remember the syntax for that.

[Peter Nelson]

Summability isn’t the hypothesis of the lemma above - it’s a lemma used to prove summability. A lemma needs to hold like that for every function (without hypotheses) to show that every function is summable.

[Anatole Dedecker]

Ah right sorry I mixed things up, indeed the first thing to prove is that everything is summable. I'd still say that it would be nice to have a lemma actually computing the sum that would work in any case, but that's orthogonal to what you want.

[Anatole Dedecker]

docs#hasSum_of_isLUB_of_nonneg seems like the perfect match here.

[Anatole Dedecker]

I'd say the simplest option is to just use this lemma to prove that any ENat-valued family is summable. I'm not sure if we can conveniently state this fact more generally atm.

[Peter Nelson]

My worry is that that involves duplicating a good amount of tsum API which is identical to the ENNreal case.

[Peter Nelson]

'Type where summing any function makes sense' feels like a good class to have, and it's a shame if the existing setup can't accommodate that.

[Peter Nelson]

(The reason the tsum API is so nice for ENNReal is that it none of it needs summability hypotheses.)

[Jireh Loreaux]

In what other situations does this come up besides ENNReal and ENat? I guess maybe functions into these types?

[Peter Nelson]

Yeah, I can't think of any others. Is n = 2 not still a good argument for abstraction?

[Peter Nelson]

What about a [Summable] typeclass, with instances for ENat and ENNReal? That would probably involve minimal refactoring.

[Jireh Loreaux]

It just depends on how much work it is to create a generic API versus duplicating the lemmas.

[Eric Wieser]

WithTop NNRat?

[Anatole Dedecker]

Peter Nelson said:

My worry is that that involves duplicating a good amount of tsum API which is identical to the ENNreal case.

In an ideal world there should be almost no lemma stated for ENNReal that is not a special case of the general theory (except of course those really specific to ENNReal), so if you have a "everything is summable" lemma you could use it to get basically everything you want.
Then, I get that it's even more convenient if we find a nice way to abstract it, but my claim was that it shouldn't be that annoying to just write ENat.summable wherever you need to provide a proof of summability, at least as a first solution.

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

E.g docs#ENNReal.tsum_le_tsum_comp_of_surjective (picked at random) should definitely be generalized in a way that requires summability and nonnegativity assumptions, and then we can discuss about wether we should have "convenient" versions in specific settings.

[Jireh Loreaux]

Eric, WithTop NNRat doesn't apply. Take a series whose coercion to ENNReal converges to an irrational. Such a series is not summable.

[Mario Carneiro]

the same property is shared with any closed additive subsemigroup of ENNReal IIRC, but that basically means scaled versions of ENat minus finitely many elements, and ENNReal

[Yury G. Kudryashov]

And products / pi types.

[Peter Nelson]

#6159 is my attempt at defining the appropriate typeclass

[Peter Nelson]

(A couple of things are still broken)

[Peter Nelson]

Ok, I believe I'm finished handling all those downstream errors.

The solution was to define a LEIffExistsMul mixin typeclass that relates an ordering to a monoid structure without extending any classes that contain le or mul as data. This can be used to define a 'complete canonically ordered add monoid', which should be the right structure so that tsums always exists. (CanonicallyOrderedMonoid is still a type, and just implements the new typeclass. )

More generally, LEIffExistsMul can be used to arbitrarily combine monoid and order structures canonically. I feel that I might not be aware of some of the tradeoffs, but this really feels more convenient, and could also be used to completely remove the need for CanonicallyLinearOrderedMonoid as well.

[Eric Rodriguez]

There is docs#ExistsMulOfLE yours is an iff, sorry!

[Yuyang Zhao]

I think there was a proposed refactor to make CanonicallyOrdered... mixin.

[Peter Nelson]

I'm looking at this again, and I'm not sure what to do.

I don't think that using the existing tsum API for ENat is an easy option. It's not just a matter of invokingSummable in a few places; there are quite a few pieces that don't fit. For instance, none of the existing versions of tsum_mul_leftwill work, because ENat isn't a topological semiring (at least, I don't think it is). So proving that needs mul_iSup-type lemmas, etc etc. The scope quickly creeps to cover a large chunk of what's in ENNReal.

But it didn't seem like there was much appetite for #6159 when I made it as an attempted fix - it eventually became buried and now has merge conflicts. Maybe someone with a better understanding of the tradeoffs in the hierarchy could have another look at this.

[Yaël Dillies]

Well, I think you could still define CompleteCanonicallyOrderedAddMonoid. I would be happy with that. I was mostly reluctant with the mixin design.

[Peter Nelson]

I'm not clear on how extends works here. If I write

class CompleteCanonicallyOrderedCommMonoid (α : Type*)
  extends CompleteLattice α, CanonicallyOrderedCommMonoid α

will le be the same for the two structures? Do the two examples below correspond to different sets of assumptions?

example {α : Type*} [CompleteLattice α] [CanonicallyOrderedCommMonoid α] : False := sorry

example {α : Type*} [CompleteCanonicallyOrderedCommMonoid α] : False := sorry

[Yaël Dillies]

First question: Yes, that's the entire point of extending.
Second question: Yes, the first one has two unrelated orders. The second one does not.

[Yaël Dillies]

Also it's worth considering whether you even need CompleteCanonicallyOrderedCommMonoid and not directly something stronger like CompleteCanonicallyOrderedSemiring.

[Yaël Dillies]

You're reaching a point where there's basically only three examples we could ever care about: extended nonnegative reals, extended natural numbers, extended nonnegative rationals. They all are semirings, so I think we do not care about CompleteCanonicallyOrderedCommMonoids that are not CompleteCanonicallyOrderedSemiring.

[Yaël Dillies]

Okay that's not quite right. Products and pi types thereof also are examples.

[Yaël Dillies]

But those would also be semirings, so I still think there's no harm in skipping the monoid version.

[Yaël Dillies]

Unrelated remark, but since you mentioned it earlier, the correct generality for mul_iSup is quantales.

[Yaël Dillies]

Annoyingly, there does not seem to be an infimum version of quantales in the literature.

[Eric Wieser]

Presumably we also care about the semifield version for ennrat/ennreal? Which is perhaps an argument for a mixing typeclass, since we need only one of those, vs two for "regular" typeclasses

[Eric Wieser]

Of course, 1 vs 2 isn't very significant; if it were more like 1 vs 5 I would feel more strongly

[Eric Wieser]

Are we likely to want lemmas about the interaction with norm? That would be another point in favor of a mixin.

[Yaël Dillies]

Currently, mathlib only talks about norms on groups, so this is mostly irrelevant.

[Yaël Dillies]

The problem I find with algebraic order mixins is that they are too easy to create and too hard to contextualise. I much prefer extending structures as a way to know which concrete structures we care about from the onset.

[Eric Wieser]

Just to be clear: is #6159 sufficient for your goals @Peter Nelson, or are you finding you need more things on top of it?

[Peter Nelson]

I don't know yet - What I want is a reasonable API for summations in ENat, and the scope of this isn't yet clear. @Yaël Dillies 's suggestion of using a semiring does make sense, though - both ENat and ENNReal are going to want mul_tsum`-type lemmas.

As @Jireh Loreaux commented earlier, ENNRat isn't an example, because of series with irrational sum. So it really is just two.

I think that, for summations to exist, one actually needs a linear order. The following works with Linear but
fails without, and I think the relevant missing typeclass (SupConvergenceClass α) fails without a linear order.

class CompleteCanonicallyLinearOrderedAddCommMonoid (α : Type*)
  extends CompleteLinearOrder α, CanonicallyOrderedAddCommMonoid α

variable {α : Type*} [CompleteCanonicallyLinearOrderedAddCommMonoid α]

theorem hasSum' (f : ι → α) : (HasSum f (⨆ (s : Finset ι), ∑ i in s, f i)) :=
  fun _ hn ↦ tendsto_atTop_iSup (fun _ _  h ↦ Finset.sum_le_sum_of_subset h) hn

theorem tsum_eq_iSup' (f : ι → α) : ∑' i, f i = ⨆ (s : Finset ι), (∑ i in s, f i) :=
  (hasSum' f).tsum_eq

I'll see how far this goes without additional assumptions being needed.