Restricting to a backwards invariant set

Stream: maths

[Lua Viana Reis]

A bit off-topic, but in case anyone reading knows: given an invariant $s = f^{-1}(s)$, is there a canonical way to write the restriction $f|_s \colon s \to s$? There is docs#Set.restrictPreimage but it doesn't use the invariance hypothesis right away so you get $f^{-1}(s) \to s$. I imagine something bundled would be useful for dynamics in general.

[Aaron Liu]

docs#Set.MapsTo.restrict

[Lua Viana Reis]

Would it make sense to have a def IsInvariant : (a → a) → Set a → Prop, so that things could be stated in terms of that? Then it would be possible to have IsInvariant.restrict f : s → s, and so on. Perhaps also easier to search in Loogle?

[Lua Viana Reis]

Aaron Liu said:

docs#Set.MapsTo.restrict

Note this is the same of what I linked, just one step behind.

[Aaron Liu]

It gives you s -> s

[Lua Viana Reis]

Ah, so have MapsTo f s s as hypothesis

[Aaron Liu]

Lua Viana Reis said:

Would it make sense to have a def IsInvariant : (a → a) → Set a → Prop, so that things could be stated in terms of that?

What's the definition? Are there many theorems that have this specific combination of hypotheses?

[Lua Viana Reis]

I think MapsTo f s s is still not ideal, because it is not equivalent to $s = f^{-1}(s)$ and in ergodic theory we really want the latter

[Aaron Liu]

I guess you can add on MapsTo f sᶜ sᶜ if you really want

[Lua Viana Reis]

Aaron Liu said:

What's the definition? Are there many theorems that have this specific combination of hypotheses?

The definition would be $s = f^{-1}(s)$. Many things in ergodic theory would have it. Loogle returns 19 matches

[Lua Viana Reis]

(sorry, I had a hard time to quote your message :sweat_smile:)

[Aaron Liu]

@loogle ?f ⁻¹' ?t = ?t

[loogle]

:search: Set.preimage_id, Set.preimage_id', and 17 more

[Aaron Liu]

nineteen, did you maybe miscount?

[Lua Viana Reis]

(and apparently I also don't know how to read)

[Lua Viana Reis]

yes, 19

[Lua Viana Reis]

/poll So, should it be...
my_theorem (h : f ⁻¹ s = s) : Ergodic (MapsTo.of_invariant h |>.restrict _ _ _) μ
my_theorem (h : s.IsInvariantFor f) : Ergodic h.restrict μ
other

[Lua Viana Reis]

(modulo better names for things, etc. MapsTo.of_invariant is also a suggestion and does not exist)

[Lua Viana Reis]

By the way, is there a good reason for all four arguments of Set.MapsTo.restrict being explicit, given the first three could be inferred from the fourth?

[Lua Viana Reis]

@loogle ?f ⁻¹' ?s =ᵐ[?μ] ?s

[loogle]

:search: MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq, MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae, and 16 more

[Lua Viana Reis]

And there is also this a.e. form

[Notification Bot]

22 messages were moved here from #maths > Weak-Mixing (Ergodic Theory) by Lua Viana Reis.

[Sébastien Gouëzel]

I think the correct assumption for most theorems should be the MapsTo one, not the stronger one where the preimage is equal to the set. Do you have examples where the stronger one is important?

[Lua Viana Reis]

Sébastien Gouëzel said:

I think the correct assumption for most theorems should be the MapsTo one, not the stronger one where the preimage is equal to the set. Do you have examples where the stronger one is important?

Hmm, sorry, this was in the context of #maths > Weak-Mixing (Ergodic Theory).

I don't see how this could work for Ergodic in general, even more so for PreErgodic and QuasiErgodic (unless the definition is changed). docs#Ergodic.ae_empty_or_univ_of_image_ae_le' take a hypothesis that the set has finite measure, and don't exist for the other two.

The counterexample I can think of now is $X= \Z_{<0} \sqcup \Z$ (the integers with an extra copy of the negative numbers), with the shift $\sigma(i)=i+1$ on each copy, but sending both copies of -1 to 0. This would be measure-preserving and ergodic for the measure that is half the counting measure on the negative part, and the counting measure on the nonnegative side. But $\Z$ is a forward-invariant set that is not almost empty nor full.

[Lua Viana Reis]

Or perhaps, you mean that if the map is {Pre,Quasi,}Ergodic and $S$ is forward invariant, then the restriction to $S$ is also {Pre,Quasi,}Ergodic?

[Lua Viana Reis]

In my example, the restriction not ergodic, because it's not measure-preserving anymore.

[Aaron Liu]

What's the theorem here?

[Anatole Dedecker]

I agree that this is a very sensible assumption in the context of noninvertible ergodic theory (and also dynamics). But I think we already have way too much restriction operators so I would say that the restriction should still be spelled using docs#Set.MapsTo.restrict, eventually with some API to make it easier to use here.

[Lua Viana Reis]

So, (MapsTo.of_invariant h |>.restrict f s s)? Where MapsTo.of_invariant : (f ⁻¹' s = s) → MapsTo f s s could be added.

[Lua Viana Reis]

And I think I came up with an explanation for MapsTo being explicit in its four parameters, it makes it easier to search with Loogle via pattern matching.