From a09187c7fa112f0200051357f3a5ee1bb0adf304 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Sat, 2 Dec 2023 13:43:06 +0100
Subject: [PATCH] :sparkles: Start proving proposition 3.2

---
 Rubin.lean              | 48 ++++++++++++++++++++++++++++++++++
 Rubin/LocallyDense.lean | 57 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 105 insertions(+)

diff --git a/Rubin.lean b/Rubin.lean
index 97610b0..e4c66b3 100644
--- a/Rubin.lean
+++ b/Rubin.lean
@@ -704,6 +704,54 @@ end RegularSupport
 
 section HomeoGroup
 
+open Topology
+
+theorem proposition_3_2 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
+  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
+  [ContinuousMulAction G α]
+  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) :
+  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧ ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g :=
+by
+  have U_in_nhds : U ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use U
+
+  let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds
+
+  -- This feels like black magic, but okay
+  let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U
+  have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed
+
+  have W_in_nhds : W ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use interior W
+    repeat' apply And.intro
+    · exact interior_subset
+    · simp
+    · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  use W
+
+  repeat' apply And.intro
+  exact W_in_nhds
+  {
+    rw [W_cl_eq_W]
+    exact W_ss_U
+  }
+
+  have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G p_in_int_W
+
+  use g
+  constructor
+  · apply rigidStabilizer_mono interior_subset
+    simp
+    exact g_in_rist
+  · rw [<-mem_support] at g_moves_p
+    apply support_subset_regularSupport
+    exact g_moves_p
+
 
 end HomeoGroup
 
diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean
index 97bfb5a..f672f77 100644
--- a/Rubin/LocallyDense.lean
+++ b/Rubin/LocallyDense.lean
@@ -15,6 +15,24 @@ class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G
     p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p))
 #align is_locally_dense Rubin.LocallyDense
 
+theorem LocallyDense.from_rigidStabilizer_in_nhds (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :
+  (∀ U : Set α, IsOpen U → ∀ p ∈ U, closure (MulAction.orbit (RigidStabilizer G U) p) ∈ 𝓝 p) →
+  LocallyDense G α :=
+by
+  intro hyp
+  constructor
+  intro U p p_in_U
+
+  -- TODO: potentially add that requirement to LocallyDense?
+  have U_open : IsOpen U := sorry
+
+  have closure_in_nhds := hyp U U_open p p_in_U
+  rw [mem_nhds_iff] at closure_in_nhds
+
+  rw [mem_interior]
+  exact closure_in_nhds
+
+-- TODO: rename
 lemma LocallyDense.nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]:
   ∀ {U : Set α},
   Set.Nonempty U →
@@ -23,6 +41,45 @@ by
   intros U H_ne
   exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U H_ne.some H_ne.some_mem⟩
 
+/--
+This is a stronger statement than `LocallyMoving.get_nontrivial_rist_elem`,
+as here we are able to prove that the nontrivial element does move `p`.
+
+The condition that `Filer.NeBot (𝓝[≠] p)` is automatically satisfied by the `HasNoIsolatedPoints` class.
+--/
+theorem get_moving_elem_in_rigidStabilizer (G : Type _) {α : Type _}
+  [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]
+  [T1Space α] {p : α} [Filter.NeBot (𝓝[≠] p)]
+  {U : Set α} (p_in_U : p ∈ U) :
+  ∃ g : G, g ∈ RigidStabilizer G U ∧ g • p ≠ p :=
+by
+  by_contra g_not_exist
+  rw [<-Classical.not_forall_not] at g_not_exist
+  simp at g_not_exist
+
+  have orbit_singleton : MulAction.orbit (RigidStabilizer G U) p = {p} := by
+    ext x
+    rw [MulAction.mem_orbit_iff]
+    rw [Set.mem_singleton_iff]
+    simp
+    constructor
+    · intro ⟨g, g_in_rist, g_eq_p⟩
+      rw [g_not_exist g g_in_rist] at g_eq_p
+      exact g_eq_p.symm
+    · intro x_eq_p
+      use 1
+      rw [x_eq_p, one_smul]
+      exact ⟨Subgroup.one_mem _, rfl⟩
+
+  have regular_orbit_empty : interior (closure (MulAction.orbit (RigidStabilizer G U) p)) = ∅ := by
+    rw [orbit_singleton]
+    rw [closure_singleton]
+    rw [interior_singleton]
+
+  have p_in_regular_orbit := LocallyDense.isLocallyDense (G := G) U p p_in_U
+  rw [regular_orbit_empty] at p_in_regular_orbit
+  exact p_in_regular_orbit
+
 class LocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
   locally_moving: ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥
 #align is_locally_moving Rubin.LocallyMoving