From 12e421d348d3b869b131e0f7521d8f955279d0be Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 08:05:20 +0100 Subject: [PATCH 1/8] =?UTF-8?q?=F0=9F=A7=B9=20clarification=20notes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .gitignore | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/.gitignore b/.gitignore index bd37e55..fdab8e0 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,10 @@ -/build -/lake-packages +# Created by `lake exe cache get` if no home directory is available /.cache -/.lake +# Prior to v4.3.0-rc2 lake stored files in these locations. +/build/ +/lake-packages/ /lakefile.olean -.DS_Store \ No newline at end of file +# After v4.3.0-rc2 lake stores its files here: +/.lake/ +# macOS leaves these files everywhere: +.DS_Store From 9057f6a7c371ecdcfc1c983fb01f92e44935dfde Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 08:05:57 +0100 Subject: [PATCH 2/8] =?UTF-8?q?=F0=9F=A7=B9=20bump=20lean=20version?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Birkhoff.lean | 3 +-- lake-manifest.json | 14 +++++++------- lean-toolchain | 2 +- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/Birkhoff.lean b/Birkhoff.lean index a00411d..f4d17f6 100644 --- a/Birkhoff.lean +++ b/Birkhoff.lean @@ -315,8 +315,7 @@ theorem omegaLimit_nonwandering (x : α) : rw [this] apply (hf 2) . simp - apply hφ - norm_num + exact Nat.sub_ne_zero_of_lt (hφ Nat.le.refl) done /- Show that the non-wandering set is non-empty -/ diff --git a/lake-manifest.json b/lake-manifest.json index d30d713..4be01b7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096", + "rev": "4c366aba55d28778421b8a1841e5512fd5c53c43", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "1c88406514a636d241903e2e288d21dc6d861e01", + "rev": "fd760831487e6835944e7eeed505522c9dd47563", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c", + "rev": "e4660fa21444bcfe5c70d37b09cc0517accd8ad7", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35", + "rev": "f5b2b6ff817890d85ffd8ed47637e36fcac544a6", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.25", + "inputRev": "v0.0.28", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3", + "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "19ab970d5f9f0204e7bb92cb15cf9862bf3ef449", + "rev": "410db9009f4e34a6bcd70cd795bba47e0222502a", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 3f21e50..cfcdd32 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.5.0-rc1 +leanprover/lean4:v4.6.0-rc1 From 6cedbc305d76fd2c76ea7bac356726e2c4287304 Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 08:06:25 +0100 Subject: [PATCH 3/8] =?UTF-8?q?=F0=9F=A7=B9=20streamline?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/build.yml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index ac5060e..884d62f 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -19,13 +19,12 @@ jobs: name: Build project steps: - name: Checkout project - uses: actions/checkout@v2 - with: - fetch-depth: 0 + uses: actions/checkout@v4 - name: Install elan - run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 + run: | + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y + echo "$HOME/.elan/bin" >> $GITHUB_PATH - name: Get cache - run: ~/.elan/bin/lake -Kenv=dev exe cache get || true + run: lake exe cache get || true - name: Build project - run: ~/.elan/bin/lake -Kenv=dev build Birkhoff - + run: lake build \ No newline at end of file From 2b6f3c02071b7cd83bb60b726809ec74508e9839 Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 08:07:19 +0100 Subject: [PATCH 4/8] =?UTF-8?q?=F0=9F=A7=B9=20vscode=20settings?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .vscode/extensions.json | 5 +++++ .vscode/settings.json | 10 ++++++++++ 2 files changed, 15 insertions(+) create mode 100644 .vscode/extensions.json create mode 100644 .vscode/settings.json diff --git a/.vscode/extensions.json b/.vscode/extensions.json new file mode 100644 index 0000000..54b27a8 --- /dev/null +++ b/.vscode/extensions.json @@ -0,0 +1,5 @@ +{ + "recommendations": [ + "leanprover.lean4", + ] +} \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..f06ff95 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,10 @@ +{ + "editor.insertSpaces": true, + "editor.tabSize": 2, + "editor.rulers": [100], + "files.encoding": "utf8", + "files.eol": "\n", + "files.insertFinalNewline": true, + "files.trimFinalNewlines": true, + "files.trimTrailingWhitespace": true +} From 00ffcf27c2e065f4f40ea3106dc6bbb02eb3bc40 Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 08:07:46 +0100 Subject: [PATCH 5/8] =?UTF-8?q?=F0=9F=A7=B9=20add=20license?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LICENSE | 201 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 201 insertions(+) create mode 100644 LICENSE diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..8dada3e --- /dev/null +++ b/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "{}" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright {yyyy} {name of copyright owner} + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. From 554bd09e24b9b23cddb5e71585095f8c87cbfe82 Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 08:14:42 +0100 Subject: [PATCH 6/8] =?UTF-8?q?=F0=9F=A7=B9=20minor=20tidy=20to=20readme?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CONTRIBUTING.md | 19 +++++++++++++++++++ README.md | 25 ++++++++++++++----------- 2 files changed, 33 insertions(+), 11 deletions(-) create mode 100644 CONTRIBUTING.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..b3aaa7a --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,19 @@ +# Contributing to this project + +We welcome anyone who can contribute something to this project. + +## Discussion + +Mostly discussion related to the project happens on Zulip. + +## Style + +We aim to follow the Mathlib style guidelines for all definitions, statements, proofs and documentation. + +- [Library Style Guidelines](https://leanprover-community.github.io/contribute/style.html) +- [Documentation style](https://leanprover-community.github.io/contribute/doc.html) +- [Mathlib naming conventions](https://leanprover-community.github.io/contribute/naming.html) + +## Collaborating on this project + +Contributions should be made by forking the repo and then opening a pull request. Most often some discussion in advance is useful. diff --git a/README.md b/README.md index 9adeadd..cd1eaf6 100644 --- a/README.md +++ b/README.md @@ -1,30 +1,33 @@ -# Birkhoff's ergodic theorem in LEAN4 +# Birkhoff's ergodic theorem in Lean 4 ![Lean build](https://github.com/mseri/birkhoff/actions/workflows/build.yml/badge.svg) -This repository contains the output of our project -at the [Machine-Checked Mathematics Workshop](https://www.lorentzcenter.nl/machine-checked-mathematics.html) -at the Lorentz Center, 10-14 July 2023. +This project was initiated at the [Machine-Checked Mathematics Workshop](https://www.lorentzcenter.nl/machine-checked-mathematics.html) at the Lorentz Center, 10-14 July 2023. -The project was developed with @marcolenci and Guillaume Dubach, -under the support and supervision of Sébastien Gouëzel. +Developed with @mseri, @marcolenci and Guillaume Dubach, under the support and supervision of Sébastien Gouëzel. ## How to use -I am assuming you have already lean4 and mathlib4 installed. -If not, [start here](https://leanprover-community.github.io/). +Make sure that Lean 4 is installed, if not, [start here](https://leanprover-community.github.io/). + +Clone this repo -To start your project, clone this repo with ``` git clone https://github.com/mseri/birkhoff.git ``` + then enter the folder + ``` cd birkhoff ``` -and download mathlib's cache with + +download mathlib's cache + ``` lake exe cache get ``` -The project file is `Birkhoff.lean`. +and open the folder in vscode to view and edit the Lean code. + +[Contribution guidelines](CONTRIBUTING.md) for this project. From 452cab24b440cc1792ac7b65c096d015cb76c2eb Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 08:55:24 +0100 Subject: [PATCH 7/8] =?UTF-8?q?=F0=9F=A7=B9=20splitting=20lean=20code=20in?= =?UTF-8?q?to=20multiple=20files?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Birkhoff.lean | 559 +------------------------------------- Birkhoff/Birkhoff.lean | 61 +++++ Birkhoff/Topological.lean | 510 ++++++++++++++++++++++++++++++++++ lakefile.lean | 10 +- 4 files changed, 582 insertions(+), 558 deletions(-) create mode 100644 Birkhoff/Birkhoff.lean create mode 100644 Birkhoff/Topological.lean diff --git a/Birkhoff.lean b/Birkhoff.lean index f4d17f6..d8a4b34 100644 --- a/Birkhoff.lean +++ b/Birkhoff.lean @@ -1,555 +1,4 @@ -import Mathlib.Tactic -import Mathlib.Dynamics.OmegaLimit -import Mathlib.Dynamics.Ergodic.AddCircle - -open MeasureTheory Filter Metric Function Set -open scoped omegaLimit -set_option autoImplicit false - -/- For every objective, first write down a statement that Lean understands, with a proof given -by `sorry`. Then try to prove it! -/ - -section Topological_Dynamics - -/- TODO: at some point translate to topological spaces -/ - -/- We could do everything in a topological space, using filters and neighborhoods, but it will -be more comfortable with a metric space. -/ -variable {α : Type _} [MetricSpace α] - -/- Define the non-wandering set of `f`-/ -def nonWanderingSet (f : α → α) : Set α := - {x | ∀ ε, 0 < ε → ∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε ∧ f^[n] y ∈ ball x ε ∧ n ≠ 0} - -variable [CompactSpace α] (f : α → α) (hf : Continuous f) - -/- Show that periodic points belong to the non-wandering set -/ -theorem periodicpts_is_mem (x : α) (n : ℕ) (nnz: n ≠ 0) (pp: IsPeriodicPt f n x) : - x ∈ nonWanderingSet f := by - intro ε hε - use x, n - -- unfold IsPeriodicPt at pp - -- unfold IsFixedPt at pp - refine' ⟨_, _, _⟩ - . exact mem_ball_self hε - . rw [pp] - exact mem_ball_self hε - . exact nnz - done - -lemma periodic_arbitrary_large_time (N : ℕ) (m : ℕ) (hm : 0 < m) (ε : ℝ) (hε : 0 < ε) (x : α) - (hx : IsPeriodicPt f m x) : - ∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε ∧ f^[n] y ∈ ball x ε ∧ N ≤ n := by - use x, m * N - refine' ⟨_,_,_⟩ - · exact mem_ball_self hε - · rw [IsPeriodicPt.mul_const hx N] - exact mem_ball_self hε - · exact Nat.le_mul_of_pos_left N hm - done - -lemma inter_subset_empty_of_inter_empty (A : Set α) (B: Set α) (C : Set α) (D: Set α) : -(A ⊆ C) → (B ⊆ D) → (C ∩ D = ∅) → (A ∩ B = ∅) := by - intro hAC hBD hCD - have hincl : A ∩ B ⊆ C ∩ D := inter_subset_inter hAC hBD - rw [hCD] at hincl - exact Iff.mp subset_empty_iff hincl - done - -/- Un lemme d'exercice: boules separees -/ -lemma separated_balls (x : α) (hfx : x ≠ f x) : ∃ ε, 0 < ε ∧ (ball x ε) ∩ (f '' (ball x ε)) = ∅ := by - have hfC : ContinuousAt f x := Continuous.continuousAt hf - rw [Metric.continuousAt_iff] at hfC - have h00 : 0 < ((dist x (f x))/4) := by - apply div_pos - rw [dist_pos] - exact hfx - exact four_pos - have hfCp := hfC ((dist x (f x))/4) h00 - rcases hfCp with ⟨a, b, c⟩ - use min a ((dist x (f x))/4) - refine' ⟨_,_⟩ - · exact lt_min b h00 - · rw [Set.ext_iff] - intro y - constructor - · intro ⟨hy1,hy2⟩ - unfold ball at hy1 - dsimp at hy1 - have hha : min a (dist x (f x) / 4) ≤ a := min_le_left a (dist x (f x) / 4) - have hy3 : dist y x < a := hy1.trans_le hha - unfold ball at hy2 - rw [mem_image] at hy2 - rcases hy2 with ⟨z , hz1, hz2⟩ - dsimp at hz1 - have hz3 : dist z x < a := hz1.trans_le hha - have hy4 := c hz3 - rw [hz2] at hy4 - have hha2 : min a (dist x (f x) / 4) ≤ (dist x (f x) / 4) := min_le_right a (dist x (f x) / 4) - have hy5 : dist y x < (dist x (f x) / 4) := hy1.trans_le hha2 - rw [dist_comm] at hy5 - exfalso - have gg := dist_triangle x y (f x) - linarith - · exact fun l => l.elim - done - --- Perhaps this should go inside Mathlib.Dynamics.PeriodicPts.lean -def IsNotPeriodicPt (f : α → α) (x : α) := ∀ n : ℕ, 0 < n -> ¬IsPeriodicPt f n x - -lemma separated_ball_image_ball (n : ℕ) (hn : 0 < n) (x : α) (hfx : IsNotPeriodicPt f x) : ∃ (ε : ℝ), 0 < ε ∧ (ball x ε) ∩ (f^[n] '' (ball x ε)) = ∅ := by - have hfx2 := hfx n hn - have hfnC : Continuous f^[n] := Continuous.iterate hf n - have hfx2' : x ≠ f^[n] x := Ne.symm hfx2 - exact separated_balls (f^[n]) hfnC x hfx2' - -lemma separated_balls_along_non_periodic_orbit (N : ℕ) (x : α) (hfx : IsNotPeriodicPt f x) : ∃ δ, (δ > 0) ∧ ∀ (n : ℕ), (0 < n) ∧ (n ≤ N + 1) → (ball x δ) ∩ (f^[n] '' ball x δ) = ∅ := by - have hkill : ∀ (n : ℕ), 0 < n → ∃ ε, 0 < ε ∧ (ball x ε) ∩ (f^[n] '' (ball x ε)) = ∅ := by - intro n hnpos - obtain ⟨ε,hε⟩ := separated_ball_image_ball f hf n hnpos x hfx - use ε - choose! ε2 hε2 h'ε2 using hkill - have A : Finset.Nonempty ((Finset.Icc 1 (N+1)).image ε2) := by simp - let δ := ((Finset.Icc 1 (N+1)).image ε2).min' A - have δmem: δ ∈ (Finset.Icc 1 (N+1)).image ε2 := Finset.min'_mem _ _ - simp at δmem - rcases δmem with ⟨n, ⟨npos, _⟩, h'n⟩ - change ε2 n = δ at h'n - use δ - constructor - exact Eq.trans_gt h'n (hε2 n npos) - intro n2 hnrange - have hA : δ ≤ ε2 n2 := by - apply Finset.min'_le - simp - use n2 - refine' ⟨_, rfl⟩ - apply hnrange - have hbigball := h'ε2 n2 hnrange.left - apply inter_subset_empty_of_inter_empty (ball x δ) (f^[n2] '' ball x δ) (ball x (ε2 n2)) (f^[n2] '' ball x (ε2 n2)) - · exact ball_subset_ball (x := x) hA - · exact image_subset (f^[n2]) (ball_subset_ball (x := x) hA) - · exact hbigball - done - - -theorem ball_non_periodic_arbitrary_large_time (ε : ℝ) (hε : 0 < ε) (x : α) (hx : x ∈ nonWanderingSet f) (hfx : IsNotPeriodicPt f x) : - ∀ (N : ℕ), ∃ (n : ℕ), N+1 < n ∧ (f^[n] '' ball x ε) ∩ ball x ε ≠ ∅ := by - -- Suppose, for sake of contradiction, `∃ N, ∀ (n : ℕ), N + 1 < n → f^[n] '' ball x ε ∩ ball x ε = ∅` - by_contra h₁ - push_neg at h₁ - -- Since x is not periodic, ∃ ε₂ > 0 such that, ∀ (n : ℕ), 0 < n ∧ n ≤ N + 1 → ball x ε₂ ∩ f^[n] '' ball x ε₂ = ∅. - obtain ⟨N,h₂⟩ := h₁ - choose ε₂ h₃ using separated_balls_along_non_periodic_orbit f hf N x hfx - obtain ⟨h₈,h₉⟩ := h₃ - -- Choose ε₃ less than ε and ε₂. - let ε₃ := min ε ε₂ - have h₅ : ε₃ ≤ ε₂ := min_le_right ε ε₂ - have h₆ : ε₃ ≤ ε := min_le_left ε ε₂ - have hε2 : 0 < ε₃ := by - rw [lt_min_iff] - constructor - exact hε - exact h₈ - -- We have therefore shown that, for all n, f^n(B(x,ε₃)) ∩ B(x,ε₃) = ∅ - have h₇ : ∀ (n : ℕ), (0 < n) → f^[n] '' ball x ε₃ ∩ ball x ε₃ = ∅ := by - intro n hnn - by_cases hcases : n ≤ N + 1 - .apply inter_subset_empty_of_inter_empty (f^[n] '' ball x ε₃) (ball x ε₃) (f^[n] '' ball x ε₂) (ball x ε₂) - apply image_subset - apply ball_subset_ball - exact h₅ - apply ball_subset_ball - exact h₅ - rw [inter_comm] - exact h₉ n ⟨hnn, hcases⟩ - .apply inter_subset_empty_of_inter_empty (f^[n] '' ball x ε₃) (ball x ε₃) (f^[n] '' ball x ε) (ball x ε) - apply image_subset - apply ball_subset_ball - exact h₆ - apply ball_subset_ball - exact h₆ - push_neg at hcases - exact h₂ n hcases - -- And this contradicts the non wandering assumption. - unfold nonWanderingSet at hx - dsimp at hx - choose y n hy hyn hnpos using hx ε₃ hε2 - push_neg at hnpos - have hu := h₇ n (Nat.pos_of_ne_zero hnpos) - have hw := mem_inter (mem_image_of_mem f^[n] hy) hyn - rw [hu] at hw - exact hw - done - - -lemma non_periodic_arbitrary_large_time (N : ℕ) (ε0 : ℝ) (hε0 : 0 < ε0) (x : α) (hfx : IsNotPeriodicPt f x) (hxf : x ∈ nonWanderingSet f) -: ∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε0 ∧ f^[n] y ∈ ball x ε0 ∧ N+1 < n := by - choose n h2 h3 using (ball_non_periodic_arbitrary_large_time f hf ε0 hε0 x hxf hfx N) - choose z h5 using (inter_nonempty_iff_exists_left.mp (nmem_singleton_empty.mp h3)) - choose y h7 h8 using ((mem_image f^[n] (ball x ε0) z).mp (mem_of_mem_inter_left h5)) - use! y, n - have hb : f^[n] y ∈ ball x ε0 := by - rw [h8] - exact h5.2 - exact ⟨h7, hb, h2⟩ - done - - -theorem arbitrary_large_time (N : ℕ) (ε : ℝ) (hε : 0 < ε) (x : α) (hx : x ∈ nonWanderingSet f) : -∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε ∧ f^[n] y ∈ ball x ε ∧ N + 1 < n := -by - by_cases hfx : IsNotPeriodicPt f x - -- hard case: if x is non-periodic, we use continuity of f - · exact non_periodic_arbitrary_large_time f hf N ε hε x hfx hx - -- easy case: if x is periodic, then y = x is a good candidate - · unfold IsNotPeriodicPt at hfx - push_neg at hfx - obtain ⟨n, hn, hn2⟩ := hfx - -- rcases hfx with ⟨n, hn⟩ also works - use x - use n * (N+2) - refine' ⟨_,_,_⟩ - · exact mem_ball_self hε - · have h4 : IsPeriodicPt f n x := by - unfold IsPeriodicPt - unfold IsFixedPt - exact hn2 - rw [IsPeriodicPt.mul_const h4 (N+2)] - exact mem_ball_self hε - · have h5 := Nat.le_mul_of_pos_left (N + 1) hn - linarith - done - - -/- Show that the non-wandering set of `f` is closed. -/ -theorem is_closed : IsClosed (nonWanderingSet f : Set α) := by - rw [← isSeqClosed_iff_isClosed] - unfold IsSeqClosed - intro u x hu ulim - rw [tendsto_atTop_nhds] at ulim - intro ε hepos - have e2pos : 0 < ε / 2 := by linarith - have h1 : IsOpen (ball x (ε / 2)) := isOpen_ball - have h2 : ∃ (z : α), z ∈ ball x (ε/ 2) ∧ z ∈ nonWanderingSet f := by - have k1 := ulim (ball x (ε / 2)) - have k2 : x ∈ (ball x (ε / 2)) := by - exact mem_ball_self e2pos - obtain ⟨N, k3⟩ := k1 k2 h1 - have k4 : u N ∈ ball x (ε / 2) := by - have k5 : N ≤ N := by - exact Nat.le_refl N - exact k3 N k5 - exact ⟨u N, k4, hu N⟩ - rcases h2 with ⟨z, h3, h4⟩ - have h5 : ∃ (y : α), ∃ (n : ℕ), y ∈ ball z (ε / 2) ∧ f^[n] y ∈ ball z (ε / 2) ∧ n ≠ 0 := by - simp [nonWanderingSet] at h4 - -- let l1 := h4 (ε / 2) e2pos - -- rcases l1 with ⟨y, l1, ⟨n, l2, l3⟩⟩ - -- obtain below is equivalent to the above two lines - obtain ⟨y, l1, ⟨n, l2, l3⟩⟩ := h4 (ε / 2) e2pos - use y, n -- note `use y, n` which is the same as `use y` and `use n` - -- simp -- was repeatedly doing `mem_ball.mp: y ∈ ball x ε -> dist y x < ε ` - exact ⟨l1, l2, l3⟩ - rcases h5 with ⟨y, n, h6, h7, h8⟩ - have h9 : y ∈ ball x ε := by - -- simp -- was doing `mem_ball.mp: y ∈ ball x ε -> dist y x < ε ` - have m1 : dist y z + dist z x < ε := by - rw [mem_ball] at h3 h6 - linarith - have : dist y x ≤ dist y z + dist z x := by - exact dist_triangle _ _ _ -- why can I omit argument, but I can't in the line below? - exact lt_of_le_of_lt this m1 - have h10 : f^[n] y ∈ ball x ε := by - -- simp -- was doing `mem_ball.mp: y ∈ ball x ε -> dist y x < ε ` - have p1 : dist (f^[n] y) z + dist z x < ε := by - rw [mem_ball] at h7 h3 - linarith - have : dist (f^[n] y) x ≤ dist (f^[n] y) z + dist z x := by - exact dist_triangle _ _ _ -- why can I omit argument, but I can't in the line below? - exact lt_of_le_of_lt this p1 - exact ⟨y, n, h9, h10, h8⟩ - done - - -/- Show that the non-wandering set of `f` is compact. -/ -theorem is_cpt : IsCompact (nonWanderingSet f : Set α) := by - apply isCompact_of_isClosed_isBounded - . exact is_closed f - . exact isBounded_of_compactSpace - done - -/- Show that the omega-limit set of any point is nonempty. -/ -/- Click F12 on ω⁺ below to go to its definition, and browse a little bit the file to get a -feel of what is already there. -/ -theorem omegaLimit_nonempty (x : α) : Set.Nonempty (ω⁺ (fun n ↦ f^[n]) ({x})) := by - apply nonempty_omegaLimit atTop (fun n ↦ f^[n]) {x} - exact Set.singleton_nonempty x - done - -/- Show that the omega-limit set of any point is contained in the non-wandering set. -/ -theorem omegaLimit_nonwandering (x : α) : - (ω⁺ (fun n ↦ f^[n]) ({x})) ⊆ (nonWanderingSet f) := by - intro z hz - rewrite [mem_omegaLimit_iff_frequently] at hz - simp at hz - have subsequence : ∀ U ∈ nhds z, ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), f^[φ n] x ∈ U := by - intro U hU - apply Filter.extraction_of_frequently_atTop (hz U hU) - done - -- unfold nonWanderingSet - intro ε hε - have ball_in_nbd : ball z ε ∈ nhds z := by - exact ball_mem_nhds z hε - -- same as `let ⟨φ, hφ, hf⟩ := subsequence (ball z ε) ball_in_nbd` but nicer - obtain ⟨φ, hφ, hf⟩ : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), f^[φ n] x ∈ ball z ε := - subsequence (ball z ε) ball_in_nbd - use f^[φ 1] x, φ 2 - φ 1 - refine' ⟨_, _, _⟩ - . exact (hf 1) - . have : f^[φ 2 - φ 1] (f^[φ 1] x) = f^[φ 2] x := by - rw [ <-Function.iterate_add_apply, Nat.sub_add_cancel ] - apply le_of_lt; - apply hφ - linarith - rw [this] - apply (hf 2) - . simp - exact Nat.sub_ne_zero_of_lt (hφ Nat.le.refl) - done - -/- Show that the non-wandering set is non-empty -/ -theorem nonWandering_nonempty [hα : Nonempty α] : Set.Nonempty (nonWanderingSet f) := by - have (x : α) : Set.Nonempty (ω⁺ (fun n ↦ f^[n]) ({x})) -> Set.Nonempty (nonWanderingSet f) := by - apply Set.Nonempty.mono - apply omegaLimit_nonwandering - apply this - apply omegaLimit_nonempty f - apply Nonempty.some hα - done - - -/- Define the recurrent set of `f`. The recurrent set is the set of points that are recurrent, - i.e. that belong to their omega-limit set. -/ -def recurrentSet {α : Type _} [TopologicalSpace α] (f : α → α) : Set α := - { x | x ∈ ω⁺ (fun n ↦ f^[n]) ({x}) } - -theorem recurrentSet_iff_accumulation_point (x : α) : - x ∈ recurrentSet f ↔ ∀ (ε : ℝ) (N : ℕ), 0 < ε - -> ∃ m : ℕ, N ≤ m ∧ f^[m] x ∈ ball x ε := by - constructor - . intro recur_x - unfold recurrentSet at recur_x - -- simp is fine as well, but we only need - -- `x ∈ { y | p y } = p x` here - -- I hope that being explicit makes compilation faster - simp only [mem_setOf_eq] at recur_x - rw [mem_omegaLimit_iff_frequently] at recur_x - intro ε N hε - have recur_x_in_ball := recur_x (ball x ε) (ball_mem_nhds x hε) - simp [frequently_atTop] at recur_x_in_ball - exact recur_x_in_ball N - . intro hf - unfold recurrentSet - simp only [mem_setOf_eq] -- `x ∈ { y | p y } = p x` - rw [mem_omegaLimit_iff_frequently] - intro U hU - simp [frequently_atTop] -- reduces the goal to `∀ (a : ℕ), ∃ b, a ≤ b ∧ f^[b] x ∈ U` - -- same as `rcases Metric.mem_nhds_iff.mp hU with ⟨ε, hε, rest⟩` but nicer - obtain ⟨ε, hε, ball_in_U⟩ : ∃ ε, ε > 0 ∧ ball x ε ⊆ U := Metric.mem_nhds_iff.mp hU - intro a - obtain ⟨m, hm, fm_in_ball⟩ := (hf ε a hε) - exact ⟨m, hm, mem_of_subset_of_mem ball_in_U fm_in_ball⟩ - done - -/- Show that periodic points belong to the recurrent set. -/ -theorem periodicpts_mem_recurrentSet - (x : α) (n : ℕ) (nnz: n ≠ 0) (hx: IsPeriodicPt f n x) : - x ∈ recurrentSet f := by - -- unfold IsPeriodicPt at hx - -- unfold IsFixedPt at hx - -- unfold recurrentSet - have x_in_omegaLimit : x ∈ ω⁺ (fun n ↦ f^[n]) ({x} : Set α) := by - rw [mem_omegaLimit_iff_frequently] - intro U hU - simp [frequently_atTop] - intro a - have hb : ∃ b, a ≤ b ∧ f^[b] x ∈ U := by - use a * n - constructor - . exact Nat.le_mul_of_pos_right a (Nat.pos_of_ne_zero nnz) - . -- have : f^[a * n] x = x := by - -- exact Function.IsPeriodicPt.const_mul hx a - -- rw [this] - rw [Function.IsPeriodicPt.const_mul hx a] - exact mem_of_mem_nhds hU - done - exact hb - done - apply x_in_omegaLimit - done - -/- Show that the recurrent set is included in the non-wandering set -/ -theorem recurrentSet_nonwandering : recurrentSet f ⊆ (nonWanderingSet f) := by - intro z hz - unfold recurrentSet at hz - simp only [mem_setOf_eq] at hz -- `x ∈ { y | p y } = p x` - apply omegaLimit_nonwandering - exact hz - done - -/- Define minimal subsets for `f`, as closed invariant subsets in which all orbits are dense. - Note that `IsInvariant.isInvariant_iff_image` is a useful function when we use `invariant`. - Using a structure here allows us to get the various properties via dot notation, - search e.g. for `hf.minimal` below -/ -structure IsMinimalSubset (f : α → α) (U : Set α) : Prop := - (closed : IsClosed U) - (invariant: IsInvariant (fun n x => f^[n] x) U) - (minimal: ∀ (x y : α) (_: x ∈ U) (_: y ∈ U) (ε : ℝ), ε > 0 -> ∃ n : ℕ, f^[n] y ∈ ball x ε) - -/- Define a minimal dynamics (all orbits are dense) -/ -def IsMinimal (f : α → α) : Prop := IsMinimalSubset f univ - -/- Show that in a minimal dynamics, the recurrent set is all the space -/ -theorem recurrentSet_of_minimal_is_all_space (hf: IsMinimal f) : - ∀ x : α, x ∈ recurrentSet f := by - intro z - -- unfold recurrentSet - -- unfold IsMinimal at hf - -- simp - have : ∀ (x : α) (ε : ℝ) (N : ℕ), ε > 0 - -> ∃ m : ℕ, m ≥ N ∧ f^[m] x ∈ ball x ε := by - intro x ε N hε - -- rcases (hf x (f^[N] x) ε hε) with ⟨n, hball⟩ - obtain ⟨n, hball⟩ : ∃ n, f^[n] (f^[N] x) ∈ ball x ε := - hf.minimal x (f^[N] x) (mem_univ _) (mem_univ _) ε hε - refine' ⟨n + N, _, _⟩ - . linarith - . rw [ <-Function.iterate_add_apply ] at hball - exact hball - done - apply (recurrentSet_iff_accumulation_point f z).mpr - exact this z - done - --- An example to learn to define maps on the unit interval -noncomputable def doubling_map (x : unitInterval) : unitInterval := - ⟨Int.fract (2 * x), by exact unitInterval.fract_mem (2 * x)⟩ - -/- Give an example of a continuous dynamics on a compact space in which the recurrent set is all -the space, but the dynamics is not minimal -/ -example : ¬IsMinimal (id : unitInterval -> unitInterval) := by - intro H - have minimality := H.minimal - contrapose minimality - -- `push_neg` pushes negations as deep as possible into the conclusion of a hypothesis - push_neg - use 0, 1, (mem_univ 0), (mem_univ 1), (dist (1 : unitInterval) (0 : unitInterval))/2 - -- we need this helper twice below - have dist_pos : 0 < dist (1 : unitInterval) 0 := by - apply dist_pos.mpr - apply unitInterval.coe_ne_zero.mp; norm_num -- 1 ≠ 0 - constructor - . apply div_pos dist_pos - linarith -- 0 < 2 - . intro n - -- `simp` is necessary to go from `¬id^[n] 1 ∈ ball 0 (dist 1 0 / 2)` - -- to `0 ≤ dist 1 0` - simp - exact le_of_lt dist_pos - done - -example (x : unitInterval) : - x ∈ recurrentSet (id : unitInterval -> unitInterval) := by - -- unfold recurrentSet - apply periodicpts_mem_recurrentSet _ _ 1 - . linarith - . exact is_periodic_id 1 x - done - - -/- Show that every point in a minimal subset is recurrent -/ -theorem minimalSubset_mem_recurrentSet (U : Set α) (hU: IsMinimalSubset f U) : - U ⊆ recurrentSet f := by - intro x hx - obtain ⟨_, hInv, hMin⟩ := hU - apply (recurrentSet_iff_accumulation_point f x).mpr - intro ε N hε - have iterates_in_U : ∀ n : ℕ, f^[n] x ∈ U := by - -- unfold IsInvariant at hInv - intro n - -- let f' := hInv n; simp at f' - -- apply Set.mapsTo'.mp at f' - -- leads us to `f^[n] x ∈ (fun n x ↦ f^[n] x) n '' U` - -- which simplifies to `∃ x', x' ∈ U ∧ f^[n] x' = f^[n] x` - -- as one can check with `simp` - apply Set.mapsTo'.mp (hInv n) - -- once we `use x` - -- we get the statement from `exact ⟨hx, rfl⟩` - -- this can be summarized to - exact ⟨x, hx, rfl⟩ - obtain ⟨n, hball⟩ : ∃ n, f^[n] (f^[N] x) ∈ ball x ε := by - apply hMin x (f^[N] x) hx (iterates_in_U N) ε hε - refine' ⟨n + N, _, _⟩ - . exact le_add_self -- N ≤ n + N - . rw [ <-Function.iterate_add_apply ] at hball - exact hball - done - -/- Show that every invariant nonempty closed subset contains at least a minimal invariant subset, -using Zorn lemma. -/ -theorem nonempty_invariant_closed_subset_has_minimalSubset - (U : Set α) (hne: Nonempty U) (hC: IsClosed U) (hI: IsInvariant (fun n x => f^[n] x) U) : - ∃ V : Set α, V ⊆ U -> (hinv: MapsTo f U U) -> IsMinimalSubset f U := by - sorry - - - -/- Show that the recurrent set of `f` is nonempty -/ -theorem recurrentSet_nonempty [Nonempty α]: Set.Nonempty (recurrentSet f) := by - sorry - -end Topological_Dynamics - -section Ergodic_Theory - -open BigOperators - -/- standing assumptions: `f` is a measure preserving map of a probability space `(α, μ)`, and -`g : α → ℝ` is integrable. -/ - -variable {α : Type _} [MetricSpace α] [CompactSpace α] [MeasurableSpace α] [BorelSpace α] - {μ : MeasureTheory.Measure α} [IsProbabilityMeasure μ] {f : α → α} - (hf : MeasurePreserving f μ) {g : α → ℝ} (hg : Integrable g μ) - - -/- Define Birkhoff sums. -/ -noncomputable def birkhoffSum {α : Type _} (f : α → α) (g : α → ℝ) (n : ℕ) (x : α) : ℝ := - 1 / n * (∑ i in Finset.range n, g (f^[i] x)) - - -/- Define the invariant sigma-algebra of `f` -/ - - - -/- Main lemma to prove Birkhoff ergodic theorem: -assume that the integral of `g` on any invariant set is strictly negative. Then, almost everywhere, -the Birkhoff sums `S_n g x` are bounded above. --/ - - -/- Deduce Birkhoff theorem from the main lemma, in the form that almost surely, `S_n f / n` -converges to the conditional expectation of `f` given the invariant sigma-algebra. -/ - - -/- If `f` is ergodic, show that the invariant sigma-algebra is ae trivial -/ - - -/- Show that the conditional expectation with respect to an ae trivial subalgebra is ae -the integral. -/ - - -/- Give Birkhoff theorem for ergodic maps -/ - - -end Ergodic_Theory +-- This module serves as the root of the `BET` library. +-- Import modules here that should be built as part of the library. +import «Birkhoff».Birkhoff +import «Birkhoff».Topological diff --git a/Birkhoff/Birkhoff.lean b/Birkhoff/Birkhoff.lean new file mode 100644 index 0000000..28286e1 --- /dev/null +++ b/Birkhoff/Birkhoff.lean @@ -0,0 +1,61 @@ +import Mathlib.Tactic +import Mathlib.Dynamics.OmegaLimit +import Mathlib.Dynamics.Ergodic.AddCircle + +/-! +# Birkhoff's ergodic theorem + +This file defines Birkhoff sums, other related notions and proves Birkhoff's ergodic theorem. + +## Implementation notes + +... + +## References + +* .... + +-/ + +section Ergodic_Theory + +open BigOperators MeasureTheory + +/- standing assumptions: `f` is a measure preserving map of a probability space `(α, μ)`, and +`g : α → ℝ` is integrable. -/ + +variable {α : Type _} [MetricSpace α] [CompactSpace α] [MeasurableSpace α] [BorelSpace α] + {μ : MeasureTheory.Measure α} [IsProbabilityMeasure μ] {f : α → α} + (hf : MeasurePreserving f μ) {g : α → ℝ} (hg : Integrable g μ) + + +/- Define Birkhoff sums. -/ +noncomputable def birkhoffSum {α : Type _} (f : α → α) (g : α → ℝ) (n : ℕ) (x : α) : ℝ := + 1 / n * (∑ i in Finset.range n, g (f^[i] x)) + + +/- Define the invariant sigma-algebra of `f` -/ + + + +/- Main lemma to prove Birkhoff ergodic theorem: +assume that the integral of `g` on any invariant set is strictly negative. Then, almost everywhere, +the Birkhoff sums `S_n g x` are bounded above. +-/ + + +/- Deduce Birkhoff theorem from the main lemma, in the form that almost surely, `S_n f / n` +converges to the conditional expectation of `f` given the invariant sigma-algebra. -/ + + +/- If `f` is ergodic, show that the invariant sigma-algebra is ae trivial -/ + + +/- Show that the conditional expectation with respect to an ae trivial subalgebra is ae +the integral. -/ + + +/- Give Birkhoff theorem for ergodic maps -/ + + +end Ergodic_Theory diff --git a/Birkhoff/Topological.lean b/Birkhoff/Topological.lean new file mode 100644 index 0000000..10cb83e --- /dev/null +++ b/Birkhoff/Topological.lean @@ -0,0 +1,510 @@ +import Mathlib.Tactic +import Mathlib.Dynamics.OmegaLimit +import Mathlib.Dynamics.Ergodic.AddCircle + +/-! +# Topological dynamics + +This file defines Birkhoff sums, other related notions and proves Birkhoff's ergodic theorem. + +## Implementation notes + +We could do everything in a topological space, using filters and neighborhoods, but it will +be more comfortable with a metric space. + +TODO: at some point translate to topological spaces + +## References + +* .... + +-/ + +open MeasureTheory Filter Metric Function Set +open scoped omegaLimit +set_option autoImplicit false + +section Topological_Dynamics + +variable {α : Type _} [MetricSpace α] + +/-- The non-wandering set of `f` is the set of points which return arbitrarily close after some iterate. -/ +def nonWanderingSet (f : α → α) : Set α := + {x | ∀ ε, 0 < ε → ∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε ∧ f^[n] y ∈ ball x ε ∧ n ≠ 0} + +variable [CompactSpace α] (f : α → α) (hf : Continuous f) + +/-- Periodic points belong to the non-wandering set. -/ +theorem periodicpts_is_mem (x : α) (n : ℕ) (nnz: n ≠ 0) (pp: IsPeriodicPt f n x) : + x ∈ nonWanderingSet f := by + intro ε hε + use x, n + refine' ⟨_, _, _⟩ + . exact mem_ball_self hε + . rw [pp] + exact mem_ball_self hε + . exact nnz + done + +lemma periodic_arbitrary_large_time (N : ℕ) (m : ℕ) (hm : 0 < m) (ε : ℝ) (hε : 0 < ε) (x : α) + (hx : IsPeriodicPt f m x) : + ∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε ∧ f^[n] y ∈ ball x ε ∧ N ≤ n := by + use x, m * N + refine' ⟨_,_,_⟩ + · exact mem_ball_self hε + · rw [IsPeriodicPt.mul_const hx N] + exact mem_ball_self hε + · exact Nat.le_mul_of_pos_left N hm + done + +lemma inter_subset_empty_of_inter_empty (A : Set α) (B: Set α) (C : Set α) (D: Set α) : +(A ⊆ C) → (B ⊆ D) → (C ∩ D = ∅) → (A ∩ B = ∅) := by + intro hAC hBD hCD + have hincl : A ∩ B ⊆ C ∩ D := inter_subset_inter hAC hBD + rw [hCD] at hincl + exact Iff.mp subset_empty_iff hincl + done + +lemma separated_balls (x : α) (hfx : x ≠ f x) : ∃ ε, 0 < ε ∧ (ball x ε) ∩ (f '' (ball x ε)) = ∅ := by + have hfC : ContinuousAt f x := Continuous.continuousAt hf + rw [Metric.continuousAt_iff] at hfC + have h00 : 0 < ((dist x (f x))/4) := by + apply div_pos + rw [dist_pos] + exact hfx + exact four_pos + have hfCp := hfC ((dist x (f x))/4) h00 + rcases hfCp with ⟨a, b, c⟩ + use min a ((dist x (f x))/4) + refine' ⟨_,_⟩ + · exact lt_min b h00 + · rw [Set.ext_iff] + intro y + constructor + · intro ⟨hy1,hy2⟩ + unfold ball at hy1 + dsimp at hy1 + have hha : min a (dist x (f x) / 4) ≤ a := min_le_left a (dist x (f x) / 4) + have hy3 : dist y x < a := hy1.trans_le hha + unfold ball at hy2 + rw [mem_image] at hy2 + rcases hy2 with ⟨z , hz1, hz2⟩ + dsimp at hz1 + have hz3 : dist z x < a := hz1.trans_le hha + have hy4 := c hz3 + rw [hz2] at hy4 + have hha2 : min a (dist x (f x) / 4) ≤ (dist x (f x) / 4) := min_le_right a (dist x (f x) / 4) + have hy5 : dist y x < (dist x (f x) / 4) := hy1.trans_le hha2 + rw [dist_comm] at hy5 + exfalso + have gg := dist_triangle x y (f x) + linarith + · exact fun l => l.elim + done + +/-- The set of points which are not periodic of any period. -/ +def IsNotPeriodicPt (f : α → α) (x : α) := ∀ n : ℕ, 0 < n -> ¬IsPeriodicPt f n x + +lemma separated_ball_image_ball (n : ℕ) (hn : 0 < n) (x : α) (hfx : IsNotPeriodicPt f x) : ∃ (ε : ℝ), 0 < ε ∧ (ball x ε) ∩ (f^[n] '' (ball x ε)) = ∅ := by + have hfx2 := hfx n hn + have hfnC : Continuous f^[n] := Continuous.iterate hf n + have hfx2' : x ≠ f^[n] x := Ne.symm hfx2 + exact separated_balls (f^[n]) hfnC x hfx2' + +lemma separated_balls_along_non_periodic_orbit (N : ℕ) (x : α) (hfx : IsNotPeriodicPt f x) : ∃ δ, (δ > 0) ∧ ∀ (n : ℕ), (0 < n) ∧ (n ≤ N + 1) → (ball x δ) ∩ (f^[n] '' ball x δ) = ∅ := by + have hkill : ∀ (n : ℕ), 0 < n → ∃ ε, 0 < ε ∧ (ball x ε) ∩ (f^[n] '' (ball x ε)) = ∅ := by + intro n hnpos + obtain ⟨ε,hε⟩ := separated_ball_image_ball f hf n hnpos x hfx + use ε + choose! ε2 hε2 h'ε2 using hkill + have A : Finset.Nonempty ((Finset.Icc 1 (N+1)).image ε2) := by simp + let δ := ((Finset.Icc 1 (N+1)).image ε2).min' A + have δmem: δ ∈ (Finset.Icc 1 (N+1)).image ε2 := Finset.min'_mem _ _ + simp at δmem + rcases δmem with ⟨n, ⟨npos, _⟩, h'n⟩ + change ε2 n = δ at h'n + use δ + constructor + exact Eq.trans_gt h'n (hε2 n npos) + intro n2 hnrange + have hA : δ ≤ ε2 n2 := by + apply Finset.min'_le + simp + use n2 + refine' ⟨_, rfl⟩ + apply hnrange + have hbigball := h'ε2 n2 hnrange.left + apply inter_subset_empty_of_inter_empty (ball x δ) (f^[n2] '' ball x δ) (ball x (ε2 n2)) (f^[n2] '' ball x (ε2 n2)) + · exact ball_subset_ball (x := x) hA + · exact image_subset (f^[n2]) (ball_subset_ball (x := x) hA) + · exact hbigball + done + + +theorem ball_non_periodic_arbitrary_large_time (ε : ℝ) (hε : 0 < ε) (x : α) (hx : x ∈ nonWanderingSet f) (hfx : IsNotPeriodicPt f x) : + ∀ (N : ℕ), ∃ (n : ℕ), N+1 < n ∧ (f^[n] '' ball x ε) ∩ ball x ε ≠ ∅ := by + -- Suppose, for sake of contradiction, `∃ N, ∀ (n : ℕ), N + 1 < n → f^[n] '' ball x ε ∩ ball x ε = ∅` + by_contra h₁ + push_neg at h₁ + -- Since x is not periodic, ∃ ε₂ > 0 such that, ∀ (n : ℕ), 0 < n ∧ n ≤ N + 1 → ball x ε₂ ∩ f^[n] '' ball x ε₂ = ∅. + obtain ⟨N,h₂⟩ := h₁ + choose ε₂ h₃ using separated_balls_along_non_periodic_orbit f hf N x hfx + obtain ⟨h₈,h₉⟩ := h₃ + -- Choose ε₃ less than ε and ε₂. + let ε₃ := min ε ε₂ + have h₅ : ε₃ ≤ ε₂ := min_le_right ε ε₂ + have h₆ : ε₃ ≤ ε := min_le_left ε ε₂ + have hε2 : 0 < ε₃ := by + rw [lt_min_iff] + constructor + exact hε + exact h₈ + -- We have therefore shown that, for all n, f^n(B(x,ε₃)) ∩ B(x,ε₃) = ∅ + have h₇ : ∀ (n : ℕ), (0 < n) → f^[n] '' ball x ε₃ ∩ ball x ε₃ = ∅ := by + intro n hnn + by_cases hcases : n ≤ N + 1 + .apply inter_subset_empty_of_inter_empty (f^[n] '' ball x ε₃) (ball x ε₃) (f^[n] '' ball x ε₂) (ball x ε₂) + apply image_subset + apply ball_subset_ball + exact h₅ + apply ball_subset_ball + exact h₅ + rw [inter_comm] + exact h₉ n ⟨hnn, hcases⟩ + .apply inter_subset_empty_of_inter_empty (f^[n] '' ball x ε₃) (ball x ε₃) (f^[n] '' ball x ε) (ball x ε) + apply image_subset + apply ball_subset_ball + exact h₆ + apply ball_subset_ball + exact h₆ + push_neg at hcases + exact h₂ n hcases + -- And this contradicts the non wandering assumption. + unfold nonWanderingSet at hx + dsimp at hx + choose y n hy hyn hnpos using hx ε₃ hε2 + push_neg at hnpos + have hu := h₇ n (Nat.pos_of_ne_zero hnpos) + have hw := mem_inter (mem_image_of_mem f^[n] hy) hyn + rw [hu] at hw + exact hw + done + + +lemma non_periodic_arbitrary_large_time (N : ℕ) (ε0 : ℝ) (hε0 : 0 < ε0) (x : α) (hfx : IsNotPeriodicPt f x) (hxf : x ∈ nonWanderingSet f) +: ∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε0 ∧ f^[n] y ∈ ball x ε0 ∧ N+1 < n := by + choose n h2 h3 using (ball_non_periodic_arbitrary_large_time f hf ε0 hε0 x hxf hfx N) + choose z h5 using (inter_nonempty_iff_exists_left.mp (nmem_singleton_empty.mp h3)) + choose y h7 h8 using ((mem_image f^[n] (ball x ε0) z).mp (mem_of_mem_inter_left h5)) + use! y, n + have hb : f^[n] y ∈ ball x ε0 := by + rw [h8] + exact h5.2 + exact ⟨h7, hb, h2⟩ + done + + +theorem arbitrary_large_time (N : ℕ) (ε : ℝ) (hε : 0 < ε) (x : α) (hx : x ∈ nonWanderingSet f) : +∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε ∧ f^[n] y ∈ ball x ε ∧ N + 1 < n := +by + by_cases hfx : IsNotPeriodicPt f x + -- hard case: if x is non-periodic, we use continuity of f + · exact non_periodic_arbitrary_large_time f hf N ε hε x hfx hx + -- easy case: if x is periodic, then y = x is a good candidate + · unfold IsNotPeriodicPt at hfx + push_neg at hfx + obtain ⟨n, hn, hn2⟩ := hfx + -- rcases hfx with ⟨n, hn⟩ also works + use x + use n * (N+2) + refine' ⟨_,_,_⟩ + · exact mem_ball_self hε + · have h4 : IsPeriodicPt f n x := by + unfold IsPeriodicPt + unfold IsFixedPt + exact hn2 + rw [IsPeriodicPt.mul_const h4 (N+2)] + exact mem_ball_self hε + · have h5 := Nat.le_mul_of_pos_left (N + 1) hn + linarith + done + + +/- Show that the non-wandering set of `f` is closed. -/ +theorem is_closed : IsClosed (nonWanderingSet f : Set α) := by + rw [← isSeqClosed_iff_isClosed] + unfold IsSeqClosed + intro u x hu ulim + rw [tendsto_atTop_nhds] at ulim + intro ε hepos + have e2pos : 0 < ε / 2 := by linarith + have h1 : IsOpen (ball x (ε / 2)) := isOpen_ball + have h2 : ∃ (z : α), z ∈ ball x (ε/ 2) ∧ z ∈ nonWanderingSet f := by + have k1 := ulim (ball x (ε / 2)) + have k2 : x ∈ (ball x (ε / 2)) := by + exact mem_ball_self e2pos + obtain ⟨N, k3⟩ := k1 k2 h1 + have k4 : u N ∈ ball x (ε / 2) := by + have k5 : N ≤ N := by + exact Nat.le_refl N + exact k3 N k5 + exact ⟨u N, k4, hu N⟩ + rcases h2 with ⟨z, h3, h4⟩ + have h5 : ∃ (y : α), ∃ (n : ℕ), y ∈ ball z (ε / 2) ∧ f^[n] y ∈ ball z (ε / 2) ∧ n ≠ 0 := by + simp [nonWanderingSet] at h4 + -- let l1 := h4 (ε / 2) e2pos + -- rcases l1 with ⟨y, l1, ⟨n, l2, l3⟩⟩ + -- obtain below is equivalent to the above two lines + obtain ⟨y, l1, ⟨n, l2, l3⟩⟩ := h4 (ε / 2) e2pos + use y, n -- note `use y, n` which is the same as `use y` and `use n` + -- simp -- was repeatedly doing `mem_ball.mp: y ∈ ball x ε -> dist y x < ε ` + exact ⟨l1, l2, l3⟩ + rcases h5 with ⟨y, n, h6, h7, h8⟩ + have h9 : y ∈ ball x ε := by + -- simp -- was doing `mem_ball.mp: y ∈ ball x ε -> dist y x < ε ` + have m1 : dist y z + dist z x < ε := by + rw [mem_ball] at h3 h6 + linarith + have : dist y x ≤ dist y z + dist z x := by + exact dist_triangle _ _ _ -- why can I omit argument, but I can't in the line below? + exact lt_of_le_of_lt this m1 + have h10 : f^[n] y ∈ ball x ε := by + -- simp -- was doing `mem_ball.mp: y ∈ ball x ε -> dist y x < ε ` + have p1 : dist (f^[n] y) z + dist z x < ε := by + rw [mem_ball] at h7 h3 + linarith + have : dist (f^[n] y) x ≤ dist (f^[n] y) z + dist z x := by + exact dist_triangle _ _ _ -- why can I omit argument, but I can't in the line below? + exact lt_of_le_of_lt this p1 + exact ⟨y, n, h9, h10, h8⟩ + done + + +/-- The non-wandering set of `f` is compact. -/ +theorem is_cpt : IsCompact (nonWanderingSet f : Set α) := by + apply isCompact_of_isClosed_isBounded + . exact is_closed f + . exact isBounded_of_compactSpace + done + +/-- The omega-limit set of any point is nonempty. -/ +theorem omegaLimit_nonempty (x : α) : Set.Nonempty (ω⁺ (fun n ↦ f^[n]) ({x})) := by + apply nonempty_omegaLimit atTop (fun n ↦ f^[n]) {x} + exact Set.singleton_nonempty x + done + +/-- The omega-limit set of any point is contained in the non-wandering set. -/ +theorem omegaLimit_nonwandering (x : α) : + (ω⁺ (fun n ↦ f^[n]) ({x})) ⊆ (nonWanderingSet f) := by + intro z hz + rewrite [mem_omegaLimit_iff_frequently] at hz + simp at hz + have subsequence : ∀ U ∈ nhds z, ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), f^[φ n] x ∈ U := by + intro U hU + apply Filter.extraction_of_frequently_atTop (hz U hU) + done + -- unfold nonWanderingSet + intro ε hε + have ball_in_nbd : ball z ε ∈ nhds z := by + exact ball_mem_nhds z hε + -- same as `let ⟨φ, hφ, hf⟩ := subsequence (ball z ε) ball_in_nbd` but nicer + obtain ⟨φ, hφ, hf⟩ : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), f^[φ n] x ∈ ball z ε := + subsequence (ball z ε) ball_in_nbd + use f^[φ 1] x, φ 2 - φ 1 + refine' ⟨_, _, _⟩ + . exact (hf 1) + . have : f^[φ 2 - φ 1] (f^[φ 1] x) = f^[φ 2] x := by + rw [ <-Function.iterate_add_apply, Nat.sub_add_cancel ] + apply le_of_lt; + apply hφ + linarith + rw [this] + apply (hf 2) + . simp + exact Nat.sub_ne_zero_of_lt (hφ Nat.le.refl) + done + +/-- The non-wandering set is non-empty -/ +theorem nonWandering_nonempty [hα : Nonempty α] : Set.Nonempty (nonWanderingSet f) := by + have (x : α) : Set.Nonempty (ω⁺ (fun n ↦ f^[n]) ({x})) -> Set.Nonempty (nonWanderingSet f) := by + apply Set.Nonempty.mono + apply omegaLimit_nonwandering + apply this + apply omegaLimit_nonempty f + apply Nonempty.some hα + done + + +/-- The recurrent set is the set of points that are recurrent, i.e. that belong to their omega-limit set. -/ +def recurrentSet {α : Type _} [TopologicalSpace α] (f : α → α) : Set α := + { x | x ∈ ω⁺ (fun n ↦ f^[n]) ({x}) } + +theorem recurrentSet_iff_accumulation_point (x : α) : + x ∈ recurrentSet f ↔ ∀ (ε : ℝ) (N : ℕ), 0 < ε + -> ∃ m : ℕ, N ≤ m ∧ f^[m] x ∈ ball x ε := by + constructor + . intro recur_x + unfold recurrentSet at recur_x + -- simp is fine as well, but we only need + -- `x ∈ { y | p y } = p x` here + -- I hope that being explicit makes compilation faster + simp only [mem_setOf_eq] at recur_x + rw [mem_omegaLimit_iff_frequently] at recur_x + intro ε N hε + have recur_x_in_ball := recur_x (ball x ε) (ball_mem_nhds x hε) + simp [frequently_atTop] at recur_x_in_ball + exact recur_x_in_ball N + . intro hf + unfold recurrentSet + simp only [mem_setOf_eq] -- `x ∈ { y | p y } = p x` + rw [mem_omegaLimit_iff_frequently] + intro U hU + simp [frequently_atTop] -- reduces the goal to `∀ (a : ℕ), ∃ b, a ≤ b ∧ f^[b] x ∈ U` + -- same as `rcases Metric.mem_nhds_iff.mp hU with ⟨ε, hε, rest⟩` but nicer + obtain ⟨ε, hε, ball_in_U⟩ : ∃ ε, ε > 0 ∧ ball x ε ⊆ U := Metric.mem_nhds_iff.mp hU + intro a + obtain ⟨m, hm, fm_in_ball⟩ := (hf ε a hε) + exact ⟨m, hm, mem_of_subset_of_mem ball_in_U fm_in_ball⟩ + done + +/-- Periodic points belong to the recurrent set. -/ +theorem periodicpts_mem_recurrentSet + (x : α) (n : ℕ) (nnz: n ≠ 0) (hx: IsPeriodicPt f n x) : + x ∈ recurrentSet f := by + -- unfold IsPeriodicPt at hx + -- unfold IsFixedPt at hx + -- unfold recurrentSet + have x_in_omegaLimit : x ∈ ω⁺ (fun n ↦ f^[n]) ({x} : Set α) := by + rw [mem_omegaLimit_iff_frequently] + intro U hU + simp [frequently_atTop] + intro a + have hb : ∃ b, a ≤ b ∧ f^[b] x ∈ U := by + use a * n + constructor + . exact Nat.le_mul_of_pos_right a (Nat.pos_of_ne_zero nnz) + . -- have : f^[a * n] x = x := by + -- exact Function.IsPeriodicPt.const_mul hx a + -- rw [this] + rw [Function.IsPeriodicPt.const_mul hx a] + exact mem_of_mem_nhds hU + done + exact hb + done + apply x_in_omegaLimit + done + +/-- The recurrent set is included in the non-wandering set -/ +theorem recurrentSet_nonwandering : recurrentSet f ⊆ (nonWanderingSet f) := by + intro z hz + unfold recurrentSet at hz + simp only [mem_setOf_eq] at hz -- `x ∈ { y | p y } = p x` + apply omegaLimit_nonwandering + exact hz + done + +/-- The minimal subsets are the closed invariant subsets in which all orbits are dense. -/ +structure IsMinimalSubset (f : α → α) (U : Set α) : Prop := + (closed : IsClosed U) + (invariant: IsInvariant (fun n x => f^[n] x) U) + (minimal: ∀ (x y : α) (_: x ∈ U) (_: y ∈ U) (ε : ℝ), ε > 0 -> ∃ n : ℕ, f^[n] y ∈ ball x ε) + +/-- A dynamical system (α,f) is minimal if α is a minimal subset. -/ +def IsMinimal (f : α → α) : Prop := IsMinimalSubset f univ + +/-- In a minimal dynamics, the recurrent set is all the space. -/ +theorem recurrentSet_of_minimal_is_all_space (hf: IsMinimal f) : + ∀ x : α, x ∈ recurrentSet f := by + intro z + have : ∀ (x : α) (ε : ℝ) (N : ℕ), ε > 0 + -> ∃ m : ℕ, m ≥ N ∧ f^[m] x ∈ ball x ε := by + intro x ε N hε + obtain ⟨n, hball⟩ : ∃ n, f^[n] (f^[N] x) ∈ ball x ε := + hf.minimal x (f^[N] x) (mem_univ _) (mem_univ _) ε hε + refine' ⟨n + N, _, _⟩ + . linarith + . rw [ <-Function.iterate_add_apply ] at hball + exact hball + done + apply (recurrentSet_iff_accumulation_point f z).mpr + exact this z + done + +/-- The doubling map is the classic interval map -/ +noncomputable def doubling_map (x : unitInterval) : unitInterval := + ⟨Int.fract (2 * x), by exact unitInterval.fract_mem (2 * x)⟩ + +/-- An example of a continuous dynamics on a compact space in which the recurrent set is all +the space, but the dynamics is not minimal -/ +example : ¬IsMinimal (id : unitInterval -> unitInterval) := by + intro H + have minimality := H.minimal + contrapose minimality + -- `push_neg` pushes negations as deep as possible into the conclusion of a hypothesis + push_neg + use 0, 1, (mem_univ 0), (mem_univ 1), (dist (1 : unitInterval) (0 : unitInterval))/2 + -- we need this helper twice below + have dist_pos : 0 < dist (1 : unitInterval) 0 := by + apply dist_pos.mpr + apply unitInterval.coe_ne_zero.mp; norm_num -- 1 ≠ 0 + constructor + . apply div_pos dist_pos + linarith -- 0 < 2 + . intro n + -- `simp` is necessary to go from `¬id^[n] 1 ∈ ball 0 (dist 1 0 / 2)` + -- to `0 ≤ dist 1 0` + simp + exact le_of_lt dist_pos + done + +example (x : unitInterval) : + x ∈ recurrentSet (id : unitInterval -> unitInterval) := by + -- unfold recurrentSet + apply periodicpts_mem_recurrentSet _ _ 1 + . linarith + . exact is_periodic_id 1 x + done + + +/-- Every point in a minimal subset is recurrent. -/ +theorem minimalSubset_mem_recurrentSet (U : Set α) (hU: IsMinimalSubset f U) : + U ⊆ recurrentSet f := by + intro x hx + obtain ⟨_, hInv, hMin⟩ := hU + apply (recurrentSet_iff_accumulation_point f x).mpr + intro ε N hε + have iterates_in_U : ∀ n : ℕ, f^[n] x ∈ U := by + -- unfold IsInvariant at hInv + intro n + -- let f' := hInv n; simp at f' + -- apply Set.mapsTo'.mp at f' + -- leads us to `f^[n] x ∈ (fun n x ↦ f^[n] x) n '' U` + -- which simplifies to `∃ x', x' ∈ U ∧ f^[n] x' = f^[n] x` + -- as one can check with `simp` + apply Set.mapsTo'.mp (hInv n) + -- once we `use x` + -- we get the statement from `exact ⟨hx, rfl⟩` + -- this can be summarized to + exact ⟨x, hx, rfl⟩ + obtain ⟨n, hball⟩ : ∃ n, f^[n] (f^[N] x) ∈ ball x ε := by + apply hMin x (f^[N] x) hx (iterates_in_U N) ε hε + refine' ⟨n + N, _, _⟩ + . exact le_add_self -- N ≤ n + N + . rw [ <-Function.iterate_add_apply ] at hball + exact hball + done + +/-- Every invariant nonempty closed subset contains at least a minimal invariant subset. -/ +theorem nonempty_invariant_closed_subset_has_minimalSubset + (U : Set α) (hne: Nonempty U) (hC: IsClosed U) (hI: IsInvariant (fun n x => f^[n] x) U) : + ∃ V : Set α, V ⊆ U -> (hinv: MapsTo f U U) -> IsMinimalSubset f U := by + -- This follows from Zorn's lemma + sorry + + + +/-- The recurrent set of `f` is nonempty -/ +theorem recurrentSet_nonempty [Nonempty α]: Set.Nonempty (recurrentSet f) := by + sorry + +end Topological_Dynamics diff --git a/lakefile.lean b/lakefile.lean index 192a6db..f721a91 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,9 +1,13 @@ import Lake open Lake DSL -package «Birkhoff» { - -- add any package configuration options here -} +package «Birkhoff» where + -- Settings applied to both builds and interactive editing + leanOptions := #[ + ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` + ⟨`pp.proofs.withType, false⟩ + ] + -- add any additional package configuration options here require mathlib from git "https://github.com/leanprover-community/mathlib4.git" From 276ac902dcd3fb4feb77b6fd3ebc8947c04f1c35 Mon Sep 17 00:00:00 2001 From: Oliver Butterley Date: Tue, 20 Feb 2024 09:02:46 +0100 Subject: [PATCH 8/8] =?UTF-8?q?=F0=9F=A7=B9=20Birkhoff=20->=20BET?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Birkhoff.lean => BET.lean | 4 ++-- {Birkhoff => BET}/Birkhoff.lean | 0 {Birkhoff => BET}/Topological.lean | 0 lakefile.lean | 4 ++-- 4 files changed, 4 insertions(+), 4 deletions(-) rename Birkhoff.lean => BET.lean (67%) rename {Birkhoff => BET}/Birkhoff.lean (100%) rename {Birkhoff => BET}/Topological.lean (100%) diff --git a/Birkhoff.lean b/BET.lean similarity index 67% rename from Birkhoff.lean rename to BET.lean index d8a4b34..d834994 100644 --- a/Birkhoff.lean +++ b/BET.lean @@ -1,4 +1,4 @@ -- This module serves as the root of the `BET` library. -- Import modules here that should be built as part of the library. -import «Birkhoff».Birkhoff -import «Birkhoff».Topological +import «BET».Birkhoff +import «BET».Topological diff --git a/Birkhoff/Birkhoff.lean b/BET/Birkhoff.lean similarity index 100% rename from Birkhoff/Birkhoff.lean rename to BET/Birkhoff.lean diff --git a/Birkhoff/Topological.lean b/BET/Topological.lean similarity index 100% rename from Birkhoff/Topological.lean rename to BET/Topological.lean diff --git a/lakefile.lean b/lakefile.lean index f721a91..e1f614c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,7 +1,7 @@ import Lake open Lake DSL -package «Birkhoff» where +package «BET» where -- Settings applied to both builds and interactive editing leanOptions := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` @@ -13,6 +13,6 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @[default_target] -lean_lib «Birkhoff» { +lean_lib «BET» { -- add any library configuration options here }