From c86abcc8f6a0f9adb04da0c97808231b80442927 Mon Sep 17 00:00:00 2001
From: zeramorphic <zeramorphic@proton.me>
Date: Sat, 16 Mar 2024 01:29:10 +0000
Subject: [PATCH] Port CountCodingFunction

Signed-off-by: zeramorphic <zeramorphic@proton.me>
---
 ConNF/Counting.lean                     |  1 +
 ConNF/Counting/CountCodingFunction.lean | 49 +++++++++++++++++++++++++
 2 files changed, 50 insertions(+)
 create mode 100644 ConNF/Counting/CountCodingFunction.lean

diff --git a/ConNF/Counting.lean b/ConNF/Counting.lean
index 93d80795f9..9824e72d1a 100644
--- a/ConNF/Counting.lean
+++ b/ConNF/Counting.lean
@@ -8,3 +8,4 @@ import ConNF.Counting.CountSpec
 import ConNF.Counting.CountStrongOrbit
 import ConNF.Counting.Hypotheses
 import ConNF.Counting.Recode
+import ConNF.Counting.CountCodingFunction
diff --git a/ConNF/Counting/CountCodingFunction.lean b/ConNF/Counting/CountCodingFunction.lean
new file mode 100644
index 0000000000..ffab353174
--- /dev/null
+++ b/ConNF/Counting/CountCodingFunction.lean
@@ -0,0 +1,49 @@
+import ConNF.Counting.Recode
+
+/-!
+# Counting coding functions
+-/
+
+open Cardinal Function MulAction Set
+open scoped Cardinal
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
+  (hγ : (γ : TypeIndex) < β)
+
+noncomputable def recodeSurjection
+    (x : { x : Set (RaisedSingleton hγ) × SupportOrbit β //
+      ∃ ho : ∀ U ∈ x.2, AppearsRaised hγ (Subtype.val '' x.1) U,
+      ∀ U, ∀ hU : U ∈ x.2,
+        Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ (Subtype.val '' x.1) U (ho U hU)) }) :
+    CodingFunction β :=
+  raisedCodingFunction hγ (Subtype.val '' x.val.1) x.val.2 x.prop.choose x.prop.choose_spec
+
+theorem recodeSurjection_surjective : Surjective (recodeSurjection hγ) := by
+  rintro χ
+  obtain ⟨S, hS⟩ := χ.dom_nonempty
+  refine ⟨⟨⟨Subtype.val ⁻¹' raiseSingletons hγ S ((χ.decode S).get hS), SupportOrbit.mk S⟩,
+      ?_, ?_⟩, ?_⟩
+  · intro U hU
+    rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
+    exact appearsRaised_of_mem_orbit hγ S ((χ.decode S).get hS) (χ.supports_decode S hS) U hU
+  · intro U hU
+    conv in (Subtype.val '' _) => rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
+    exact supports_decodeRaised_of_mem_orbit hγ S
+      ((χ.decode S).get hS) (χ.supports_decode S hS) U hU
+  · rw [recodeSurjection]
+    conv in (Subtype.val '' _) => rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
+    conv_rhs => rw [CodingFunction.eq_code hS,
+      ← recode_eq hγ S ((χ.decode S).get hS) (χ.supports_decode S hS)]
+
+/-- The main lemma about counting coding functions. -/
+theorem mk_strong_codingFunction_le :
+    #(CodingFunction β) ≤ 2 ^ #(RaisedSingleton hγ) * #(SupportOrbit β) := by
+  refine (mk_le_of_surjective (recodeSurjection_surjective hγ)).trans ?_
+  refine (mk_subtype_le _).trans ?_
+  simp only [mk_prod, mk_set, lift_id, le_refl]
+
+end ConNF