[Merged by Bors] - feat: define ergodic actions#14952
Conversation
PR summary 6f94d50389
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.GroupTheory.GroupAction.IterateAct | 207 | 179 | -28 (-13.53%) |
| Mathlib.MeasureTheory.MeasurableSpace.Instances | 605 | 607 | +2 (+0.33%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 367 files with changed transitive imports: this is too many to display! |
Declarations diff
+ ErgodicSMul
+ ErgodicVAdd
+ IterateMulAct.instDiscreteMeasurableSpace
+ IterateMulAct.instMeasurableSpace
+ Measurable.measurableSMul₂_iterateMulAct
+ MeasurePreserving.smulInvariantMeasure_iterateMulAct
+ _root_.ErgodicSMul.of_aestabilizer
+ _root_.MulAction.aeconst_of_aestabilizer_eq_top
+ aeconst_of_forall_preimage_smul_ae_eq
+ aeconst_of_forall_smul_ae_eq
+ ergodicSMul_iterateMulAct
+ instCountable
+ instance (priority := 100) Subsingleton.measurableSingletonClass
+ measurableSMul_iterateMulAct
+ measurableSMul₂_iterateMulAct
+ smulInvariantMeasure_iterateMulAct
- Subsingleton.measurableSingletonClass
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
|
This PR/issue depends on: |
| instance IterateMulAct.instDiscreteMeasurableSpace {α : Type*} {f : α → α} : | ||
| DiscreteMeasurableSpace (IterateMulAct f) := inferInstance | ||
|
|
||
| instance (priority := 100) Subsingleton.measurableSingletonClass |
There was a problem hiding this comment.
| instance (priority := 100) Subsingleton.measurableSingletonClass | |
| instance (priority := 100) Subsingleton.instMeasurableSingletonClass |
There was a problem hiding this comment.
This is a pre-existing instance. I would prefer not to rename it in an unrelated PR.
| simp only [ergodicSMul_iff, smulInvariantMeasure_iterateMulAct, hf] | ||
| refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩ | ||
| · intro s hm hs | ||
| rw [← eventuallyConst_set'] |
There was a problem hiding this comment.
I think the ideal would be to refactor PreErgodic to use the language of EventuallyConst s (ae μ).
I think almost as good would be to add lemmas similar to :
lemma Ergodic.eventuallyConst_ae (hf : Ergodic f μ) (hs : MeasurableSet s) (hs' : f ⁻¹' s = s) :
EventuallyConst s (ae μ) := by
simpa only [eventuallyConst_set'] using hf.ae_empty_or_univ hs hs'and use them here instead of eventuallyConst_set'.
However this is all just "nice to have". This is clearly fine as it stands.
There was a problem hiding this comment.
This refactor is on my TODO list but I don't want to make this series of PRs depend on a refactor.
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
|
bors merge |
Also prove that a function is ergodic iff the corresponding `IterateMulAct` action is ergodic.
|
Pull request successfully merged into master. Build succeeded: |
Also prove that a function is ergodic iff the corresponding `IterateMulAct` action is ergodic.
Also prove that a function is ergodic iff the corresponding `IterateMulAct` action is ergodic.
Also prove that a function is ergodic iff the corresponding `IterateMulAct` action is ergodic.
Also prove that a function is ergodic iff the corresponding
IterateMulActactionis ergodic.