Minimal.lean to be polished and harmonized with mathlib

[mseri]

See https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Dynamics/Minimal.lean

Our minimal sets need to be extended to action and topological spaces

[oliver-butterley]

Just a note to explain that in a recent PR to this repo, more results related to minimal sets were added. Currently the file contains some definitions and results which are not in mathlib but the definitions are not as general as those for minimal in mathlib. In summary there is stuff that is very much worthwhile adding to mathlib but there is quite a gap to make it match up with what is already there.

[oliver-butterley]

Soon we'll figure out a full and precise action plan... At the moment it seems the key things related to Minimal.lean are:

• Update the remaining parts from metric to topological spaces.
• Decide a strategy for making this content compatible with Mathlib/Dynamics/Minimal and perhaps adjusting what is already in mathlib to achieve this. - Adjust the way the equivalent definitions are written.
• Refine everything to mathlib stlye.

Currently in mathlib:

/-- An action of an additive monoid `M` on a topological space is called *minimal* if the `M`-orbit
of every point `x : α` is dense. -/
class AddAction.IsMinimal (M α : Type*) [AddMonoid M] [TopologicalSpace α] [AddAction M α] :
    Prop where
  dense_orbit : ∀ x : α, Dense (AddAction.orbit M x)

[mseri]

Ping @sgouezel to give you an idea of what we had in mind at least for minimal

[sgouezel]

I think the mathlib notion is pretty bad (the existence of the dense orbit should require completness of the space or something like that), and will in in time need to be refactored in terms of your notion. The steps would be:

• First clean up everything you have, and get it into mathlib
• Then refactor the existing mathlib definition.

Don't try to do both at the same time, it would just make things more completed to review.

[sgouezel]

I'd advise to write down a definition of minimal that makes sense for the action of any monoid, although then it makes sense to prove results specific to actions of N or Z as you wish.

[sgouezel]

variable {α : Type*}[TopologicalSpace α]

/- A subset is minimal if it is nonempty, closed, and every orbit is dense.
To do: remove invariant, add nonempty. -/
structure AddAction.IsMinimalSubset (M : Type*) [VAdd M α] (U : Set α) : Prop :=
  (isClosed : IsClosed U)
  (isInvariant : IsInvariant (fun (n : M) (x : α) ↦ n +ᵥ x) U)
  (isMinimal : ∀ V W, IsOpen V → (U ∩ V).Nonempty → IsOpen W → (U ∩ W).Nonempty → ∃ (n : M),
    ((fun (x : α) ↦ n +ᵥ x) ⁻¹' (V ∩ U)) ∩ (W ∩ U) |>.Nonempty)

/- A subset is minimal if it is nonempty, closed, and every orbit is dense.
To do: remove invariant, add nonempty. -/
@[to_additive]
structure MulAction.IsMinimalSubset (M : Type*) [SMul M α] (U : Set α) : Prop :=
  (isClosed : IsClosed U)
  (isInvariant : IsInvariant (fun (n : M) (x : α) ↦ n • x) U)
  (isMinimal : ∀ V W, IsOpen V → (U ∩ V).Nonempty → IsOpen W → (U ∩ W).Nonempty → ∃ (n : M),
    ((fun (x : α) ↦ n • x) ⁻¹' (V ∩ U)) ∩ (W ∩ U) |>.Nonempty)

namespace MulAction

variable (M : Type*) [Monoid M] [MulAction M α]

-- Any theorem here should have a @[to_additive]...

end MulAction

[mseri]

Topological.lean needs to be updated to use TopologicalSpace instead of MetricSpace before we can update minimal. This appears immediately when trying to generalize

theorem recurrentSet_of_minimal_is_all_space (M : Type*) [AddMonoid ℕ] [AddAction ℕ α]
  (hM : AddAction.IsMinimal ℕ α) (x : α) :
    x ∈ recurrentSet (fun x ↦ AddAction.toFun ℕ α x 1) := by
  -- explicitly, we are now proving
  -- ∀ (ε : ℝ) (N : ℕ), ε > 0 → ∃ m : ℕ, m ≥ N ∧ f^[m] x ∈ ball x ε
  let f := fun x ↦ AddAction.toFun ℕ α x 1
  apply (recurrentSet_iff_accumulation_point f x).mpr
  intro ε N hε
  obtain ⟨n, hball⟩ : ∃ n, f^[n] (f^[N] x) ∈ ball x ε :=
    hf.minimal x (f^[N] x) (mem_univ _) (mem_univ _) ε hε
  exact ⟨n + N, by linarith, (Function.iterate_add_apply _ _ _ _).symm ▸ hball⟩

Here as soon as we call Topological.recurrentSet_iff_accumulation_point we get the error failed to synthesize MetricSpace α

[sgouezel]

Yury's comment on Zulip that there is Flow in the file Mathlib.Dynamics.Flow is excellent. It's probably a good idea to rephrase everything in terms of this notion, because there is already a canonical way to go from a map to the flow constructed from its iterations. And since you're doing topological dynamics, assuming continuity for all of this is definitely natural.

As flows are only with additive notation currently, it means you won't need to to_additiveize everything. Just start from ϕ : Flow τ α.

[sgouezel]

(An issue with the SMul point of view is that the naturasl already act on the real line, by multiplication, so if you want to look at a dynamics on the real line using the SMul point of view there will be two different typeclasses for [SMul ℕ ℝ], which will be a nightmare).

[mseri]

It is being a nightmare in a number of different ways haivng to deal with topological space & filters :) I think it could be a good idea if we sit down for a while and streamline what we should do