Add definition of divergent orbits invariant set #9
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
I added both the one from @marcolenci's note and the one from Katok-Hasselblatt Signed-off-by: Marcello Seri <marcello.seri@gmail.com>
Signed-off-by: Marcello Seri <marcello.seri@gmail.com>
| /- define `A := { x | sup_n ∑_{i=0}^{n} f(T^i x) = ∞}`. -/ | ||
| define `A := { x | lim_n ∑_{i=0}^{n} f(T^i x) = ∞}`. | ||
| -/ | ||
| def A := { x : α | Filter.Tendsto (fun n ↦ ∑ i in Finset.range n, f (T^[i] x)) Filter.atTop Filter.atTop } |
There was a problem hiding this comment.
Is this correct mathematically? Doesn't this require some degree of convergence towards infinity? It seems to me that,
def A := { x : α | ∀ C : ℝ, ∃ n, ∑ i in Finset.range n, f (T^[i] x) > C }
includes some extra points since f is not bounded and can be negative and positive.
There was a problem hiding this comment.
Yes, it is not f that we ultimately want to use, I will need to update the definition to after we define the modified observable (the one that gives a monotonically increasing sequence)
|
I prepared a few things that could be useful but this is Noemi's first week
back at work and my first week full time looking after our son during the
day so I'm slow communicating anything. I'll try to collate it tonight.
…On Thu, 7 Mar 2024, 15:49 Marcello Seri, ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In BET/Birkhoff.lean
<#9 (comment)>:
>
-/- define `A := { x | sup_n ∑_{i=0}^{n} f(T^i x) = ∞}`. -/
+define `A := { x | lim_n ∑_{i=0}^{n} f(T^i x) = ∞}`.
+-/
+def A := { x : α | Filter.Tendsto (fun n ↦ ∑ i in Finset.range n, f (T^[i] x)) Filter.atTop Filter.atTop }
Yes, it is not f that we ultimately want to use, I will need to update the
definition to after we define the modified observable (the one that gives a
monotonically increasing sequence)
—
Reply to this email directly, view it on GitHub
<#9 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AMLZETLCVFI2US6X7DLLLQDYXB5ATAVCNFSM6AAAAABD7XTDUGVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTSMRSGY2DGNRYHE>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
|
Don’t worry. There is no rush. Take your time
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I added both the one from @marcolenci's note and the one from Katok-Hasselblatt