Markov-Kakutani fixed point theorem

Stream: mathlib4

[Michael Lane]

Hi!

I have finished leaning a proof of the Markov-Kakutani fixed point theorem, found here: https://en.wikipedia.org/wiki/Markov%E2%80%93Kakutani_fixed-point_theorem

My eventual goal is to write a theory of amenable groups for locally compact groups. (A google search reveals this has already been done in Lean 3 for discrete countable groups.) I already have a bit of work done in this direction, but the Markov-Kakutani code is much more PR-able.

There are a few things that I could not find in mathlib that I suspect do exist, I just can't find them. For example, this function and theorem:

variable {V : Type _}

def finInter {n : ℕ} (f : Fin n → Set V)
: Fin n → Set V
  | ⟨0, isLt⟩ => f ⟨0, isLt⟩
  | ⟨k + 1, isLt⟩ => f ⟨k + 1, isLt⟩ ∩ finInter f ⟨k, by omega⟩

theorem finInter_eq_iInter_forall {n : ℕ} (f : Fin n → Set V)
: ∀ k, finInter f k = ⋂ i : Fin (k + 1), f (i.castLT (by omega))

The proof of the theorem is a very annoying 21 lines long...

So my two questions are:

1. Does the finInter function exist already in mathlib?
2. Is there anything I should do towards making a PR that isn't already found on this list: https://leanprover-community.github.io/contribute/index.html?

Thanks a lot
Michael

[Aaron Liu]

Why do you need finInter?

[Aaron Liu]

You can also write it as ⋂ i ∈ Finset.Iic k, f i

[Michael Lane]

Aaron Liu said:

Why do you need finInter?

This line of the proof, from the Wikipedia page, bold mine: "Applying the result for a single mapping successively, it follows that any finite subset..." I can experiment with the Finset.Iic suggestion to see if it suits my needs.

[Yakov Pechersky]

Applying the result for a single mapping successively, it follows that any finite subset of S has a non-empty fixed point set given as the intersection of the compact convex sets K^{T} as T ranges over the subset.

I would imagine the proof discusses as Finset and uses finset induction

[Aaron Liu]

docs#Finset.induction

[Michael Lane]

Any comments on this instance and theorem?

variable {V : Type _}
variable [AddCommGroup V] [Module ℝ V] [TopologicalSpace V]

instance : Monoid (V →ᴬ[ℝ] V) where
  mul T₁ T₂ := T₁.comp T₂
  one := {AffineMap.id ℝ V with cont := by continuity}
  mul_assoc _ _ _ := rfl
  one_mul _ := rfl
  mul_one _ := rfl

theorem comm_comp_of_comm_action
{action : Submonoid (V →ᴬ[ℝ] V)} [IsMulCommutative action]
: ∀ T₁ T₂ : action, T₁.1 ∘ T₂.1 = T₂.1 ∘ T₁.1 := by
  intro T₁ T₂
  calc T₁.1 ∘ T₂.1
    _ = T₁ * T₂ := rfl
    _ = T₂ * T₁ := by rw[CommMonoid.mul_comm T₁ T₂]

The monoid structure is just composition of continuous affine maps. Since this is a fairly standard construction, is there a shorter way of creating the instance, other than listing all its fields?

The theorem to me just feels "tortured". Is there a better way of doing it?

[Aaron Liu]

Usually these are put under a type synonym, since multiplication is pointwise multiplication. For example, we have docs#Module.End, docs#Monoid.End, docs#Function.End, etc.

[Michael Lane]

Could you clarify "multiplication is pointwise multiplication"?

[Aaron Liu]

When multiplying two functions ℕ → ℝ, for example, the default instance is pointwise multiplication. Same for monoid homomorphisms, and for continuous maps and for a lot of other map too probably