Strong supports

Signed-off-by: zeramorphic <[email protected]>

ConNF.lean

@@ -35,3 +35,4 @@ import ConNF.Setup.StrSet
 import ConNF.Setup.Support
 import ConNF.Setup.Tree
 import ConNF.Setup.TypeIndex
+import ConNF.Support.Strong

ConNF/Aux/Set.lean

@@ -50,10 +50,28 @@ theorem Set.inter_symmDiff_left {α : Type _} {s t : Set α} :
   simp only [Set.mem_symmDiff, Set.mem_inter_iff, Set.mem_diff]
   tauto
 
-theorem Set.smulSet_def {α β : Type _} {x : α} {s : Set β} [SMul α β] :
+theorem Set.smul_set_def {α β : Type _} {x : α} {s : Set β} [SMul α β] :
     x • s = (x • ·) '' s :=
   rfl
 
+theorem Set.subset_smul_set {α β : Type _} {x : α} {s t : Set β} [Group α] [MulAction α β] :
+    t ⊆ x • s ↔ x⁻¹ • t ⊆ s := by
+  constructor
+  · rintro h _ ⟨a, ha, rfl⟩
+    simp only [← mem_smul_set_iff_inv_smul_mem]
+    exact h ha
+  · intro h a ha
+    refine ⟨x⁻¹ • a, ?_, ?_⟩
+    · apply h
+      rwa [smul_mem_smul_set_iff]
+    · simp only [smul_inv_smul]
+
+theorem Set.symmDiff_smul_set {α β : Type _} {x : α} {s t : Set β} [Group α] [MulAction α β] :
+    x • s ∆ t = (x • s) ∆ (x • t) := by
+  ext a
+  simp only [Set.mem_smul_set, Set.mem_symmDiff]
+  aesop
+
 theorem Set.bounded_lt_union {α : Type _} [LinearOrder α] {s t : Set α}
     (hs : s.Bounded (· < ·)) (ht : t.Bounded (· < ·)) :
     (s ∪ t).Bounded (· < ·) := by

ConNF/Setup/BasePerm.lean

@@ -95,7 +95,7 @@ theorem one_litter :
 instance : Mul BasePerm where
   mul π₁ π₂ := ⟨π₁ᴬ * π₂ᴬ, π₁ᴸ * π₂ᴸ, λ s L h ↦ by
     have := π₁.smul_near_smul _ _ <| π₂.smul_near_smul s L h
-    simpa only [Set.smulSet_def, Set.image_image] using this⟩
+    simpa only [Set.smul_set_def, Set.image_image] using this⟩
 
 @[simp]
 theorem mul_atom (π₁ π₂ : BasePerm) :
@@ -113,7 +113,7 @@ theorem inv_smul_near_inv_smul (π : BasePerm) (s : Set Atom) (L : Litter) :
   apply near_trans (near_image h ↑πᴬ⁻¹)
   have := π.smul_near_smul (πᴸ⁻¹ L)ᴬ (πᴸ⁻¹ L) near_rfl
   have := near_image this ↑πᴬ⁻¹
-  simp only [smul_litter_def, smul_atom_def, Perm.apply_inv_self, Set.smulSet_def,
+  simp only [smul_litter_def, smul_atom_def, Perm.apply_inv_self, Set.smul_set_def,
     Perm.image_inv, preimage_image] at this
   rw [Perm.image_inv]
   exact near_symm this

ConNF/Setup/Enumeration.lean

@@ -191,6 +191,32 @@ theorem smul_rel {G X : Type _} [Group G] [MulAction G X]
     (π • E).rel i x ↔ E.rel i (π⁻¹ • x) :=
   Iff.rfl
 
+@[simp]
+theorem mem_smul {G X : Type _} [Group G] [MulAction G X]
+    (π : G) (E : Enumeration X) (x : X) :
+    x ∈ π • E ↔ π⁻¹ • x ∈ E :=
+  Iff.rfl
+
+open scoped Pointwise in
+@[simp]
+theorem smul_rel_codom {G X : Type _} [Group G] [MulAction G X]
+    (π : G) (E : Enumeration X) :
+    (π • E).rel.codom = π • E.rel.codom := by
+  ext x
+  constructor
+  · rintro ⟨i, h⟩
+    exact ⟨π⁻¹ • x, ⟨i, h⟩, smul_inv_smul π x⟩
+  · rintro ⟨x, ⟨i, h⟩, rfl⟩
+    use i
+    rwa [smul_rel, inv_smul_smul]
+
+open scoped Pointwise in
+@[simp]
+theorem smul_coe {G X : Type _} [Group G] [MulAction G X]
+    (π : G) (E : Enumeration X) :
+    ((π • E : Enumeration X) : Set X) = π • (E : Set X) :=
+  smul_rel_codom π E
+
 instance {G X : Type _} [Group G] [MulAction G X] :
     MulAction G (Enumeration X) where
   one_smul E := by

ConNF/Setup/Tree.lean

@@ -99,6 +99,16 @@ theorem zpow_apply [Group X] (T : Tree X α) (A : α ↝ ⊥) (n : ℤ) :
     (T ^ n) A = (T A) ^ n :=
   rfl
 
+@[simp]
+theorem inv_deriv [Group X] (T : Tree X α) (A : α ↝ β) :
+    T⁻¹ ⇘ A = (T ⇘ A)⁻¹ :=
+  rfl
+
+@[simp]
+theorem inv_sderiv [Group X] (T : Tree X α) (h : β < α) :
+    T⁻¹ ↘ h = (T ↘ h)⁻¹ :=
+  rfl
+
 /-- The partial order on the type of `α`-trees of `X` is given by "branchwise" comparison. -/
 instance partialOrder [PartialOrder X] : PartialOrder (Tree X α) :=
   Pi.partialOrder

ConNF/Support/Strong.lean

@@ -0,0 +1,83 @@
+import ConNF.FOA.Inflexible
+
+/-!
+# Strong supports
+
+In this file, we define strong supports.
+
+## Main declarations
+
+* `ConNF.Support.Strong`: The property that a support is strong.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal
+open scoped symmDiff
+
+namespace ConNF
+
+variable [Params.{u}] {β : TypeIndex}
+
+instance : LE BaseSupport where
+  le S T := (Sᴬ : Set Atom) ⊆ Tᴬ ∧ (Sᴺ : Set NearLitter) ⊆ Tᴺ
+
+instance : Preorder BaseSupport where
+  le_refl S := ⟨subset_rfl, subset_rfl⟩
+  le_trans S T U h₁ h₂ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩
+
+theorem BaseSupport.smul_le_smul {S T : BaseSupport} (h : S ≤ T) (π : BasePerm) :
+    π • S ≤ π • T := by
+  constructor
+  · simp only [smul_atoms, Enumeration.smul_rel_codom, Set.set_smul_subset_set_smul_iff]
+    exact h.1
+  · simp only [smul_nearLitters, Enumeration.smul_rel_codom, Set.set_smul_subset_set_smul_iff]
+    exact h.2
+
+instance : LE (Support β) where
+  le S T := ∀ A, S ⇘. A ≤ T ⇘. A
+
+instance : Preorder (Support β) where
+  le_refl S := λ A ↦ le_rfl
+  le_trans S T U h₁ h₂ := λ A ↦ (h₁ A).trans (h₂ A)
+
+theorem Support.smul_le_smul {S T : Support β} (h : S ≤ T) (π : StrPerm β) :
+    π • S ≤ π • T :=
+  λ A ↦ BaseSupport.smul_le_smul (h A) (π A)
+
+namespace Support
+
+variable [Level] [CoherentData] [LeLevel β]
+
+structure Strong (S : Support β) : Prop where
+  interference_subset {A : β ↝ ⊥} {N₁ N₂ : NearLitter} :
+    N₁ ∈ (S ⇘. A)ᴺ → N₂ ∈ (S ⇘. A)ᴺ → N₁ᴬ ∆ N₂ᴬ ⊆ (S ⇘. A)ᴬ
+  support_le {A : β ↝ ⊥} {N : NearLitter} (h : N ∈ (S ⇘. A)ᴺ)
+    (P : InflexiblePath β) (t : Tangle P.δ)
+    (hA : A = P.A ↘ P.hε ↘.) (ht : Nᴸ = fuzz P.hδε t) :
+    t.support ≤ S ⇘ (P.A ↘ P.hδ)
+
+theorem Strong.smul {S : Support β} (hS : S.Strong) (ρ : AllPerm β) : (ρᵁ • S).Strong := by
+  constructor
+  · intro A N₁ N₂ h₁ h₂
+    rw [smul_derivBot, BaseSupport.smul_nearLitters, Enumeration.mem_smul] at h₁ h₂
+    rw [smul_derivBot, BaseSupport.smul_atoms, Enumeration.smul_rel_codom, Set.subset_smul_set,
+      Set.symmDiff_smul_set]
+    exact hS.interference_subset h₁ h₂
+  · intro A N hN P t hA ht
+    rw [smul_derivBot, BaseSupport.smul_nearLitters, Enumeration.mem_smul] at hN
+    have := hS.support_le hN P (ρ⁻¹ ⇘ P.A ↘ P.hδ • t) hA ?_
+    · convert smul_le_smul this (ρᵁ ⇘ P.A ↘ P.hδ) using 1
+      · rw [Tangle.smul_support, smul_smul,
+          allPermSderiv_forget, allPermDeriv_forget, allPermForget_inv,
+          Tree.inv_deriv, Tree.inv_sderiv, mul_inv_cancel, one_smul]
+      · ext B : 1
+        rw [smul_derivBot, Tree.sderiv_apply, Tree.deriv_apply, Path.deriv_scoderiv]
+        rfl
+    · rw [← smul_fuzz P.hδ P.hε P.hδε, allPermDeriv_forget, allPermForget_inv,
+        BasePerm.smul_nearLitter_litter, ← Tree.inv_apply, hA, ht]
+      rfl
+
+end Support
+end ConNF

blueprint/src/chapters/counting.tex

@@ -2,12 +2,16 @@ \section{Strong supports}
 \begin{definition}
   \uses{def:StrSupport}
   \label{def:StrSupport.Occurs}
-  We define a partial order \( \preceq \) on base supports by \( S \preceq T \) if and only if \( \im S^\Atom \subseteq \im T^\Atom \) and \( \im S^\NearLitter \subseteq \im T^\NearLitter \).
+  \lean{ConNF.instPreorderSupport}
+  \leanok
+  We define a preorder \( \preceq \) on base supports by \( S \preceq T \) if and only if \( \im S^\Atom \subseteq \im T^\Atom \) and \( \im S^\NearLitter \subseteq \im T^\NearLitter \).
   For \( \beta \)-supports, we define \( S \preceq T \) if and only if \( S_A \preceq T_A \) for each \( A \).
 \end{definition}
 \begin{definition}
   \uses{def:StrSupport,def:InflexiblePath,def:Interference}
   \label{def:Strong}
+  \lean{ConNF.Support.Strong}
+  \leanok
   A \( \beta \)-support \( S \) is \emph{strong} if:
   \begin{itemize}
     \item for every pair of near-litters \( N_1, N_2 \in \im S_A^\NearLitter \), we have \( \interf(N_1, N_2) \subseteq \im S_A^\Atom \); and
@@ -17,9 +21,12 @@ \section{Strong supports}
 \begin{proposition}
   \uses{def:Strong}
   \label{prop:Strong.smul}
+  \lean{ConNF.Support.Strong.smul}
+  \leanok
   If \( S \) is a strong \( \beta \)-support and \( \rho \) is \( \beta \)-allowable, then \( \rho(S) \) is strong.
 \end{proposition}
 \begin{proof}
+  \leanok
   Interference is stable under application of allowable permutations, and the required supports are also preserved under action of allowable permutations.
 \end{proof}
 \begin{proposition}