Add product image bound theorems

Author: Fieldnote-Echo

OrdvecFormalization/FiniteProductQuotient.lean

@@ -254,6 +254,113 @@ theorem card_productQuotientRules {Z₁ Z₂ A : Type}
       Fintype.card A ^ (Fintype.card Z₁ * Fintype.card Z₂) := by
   rw [Fintype.card_fun, Fintype.card_prod]
 
+/--
+The reachable image of a product map is contained in the product of the two
+reachable component images.
+-/
+theorem productMap_image_subset_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (productMap Q₁ Q₂) ⊆
+      (QuotientImageFinset Q₁).product (QuotientImageFinset Q₂) := by
+  intro z hz
+  rcases Finset.mem_image.mp hz with ⟨p, _hp, hp⟩
+  rw [← hp]
+  exact Finset.mem_product.mpr
+    ⟨Finset.mem_image.mpr ⟨p.1, Finset.mem_univ p.1, rfl⟩,
+      Finset.mem_image.mpr ⟨p.2, Finset.mem_univ p.2, rfl⟩⟩
+
+/--
+The reachable image of a product map is exactly the product of the reachable
+component images.
+-/
+theorem productMap_image_eq_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (productMap Q₁ Q₂) =
+      (QuotientImageFinset Q₁).product (QuotientImageFinset Q₂) := by
+  apply Finset.Subset.antisymm
+  · exact productMap_image_subset_product_images Q₁ Q₂
+  · intro z hz
+    rcases Finset.mem_product.mp hz with ⟨hz₁, hz₂⟩
+    rcases Finset.mem_image.mp hz₁ with ⟨x, _hx, hx⟩
+    rcases Finset.mem_image.mp hz₂ with ⟨y, _hy, hy⟩
+    exact Finset.mem_image.mpr
+      ⟨(x, y), Finset.mem_univ (x, y), Prod.ext hx hy⟩
+
+/--
+The number of reachable product codes is exactly the product of the numbers of
+reachable component codes.
+-/
+theorem productMap_image_card_eq_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (productMap Q₁ Q₂)).card =
+      (QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card := by
+  rw [productMap_image_eq_product_images Q₁ Q₂]
+  simp
+
+/--
+The number of reachable product codes is bounded by the product of the numbers
+of reachable component codes.
+-/
+theorem productMap_image_card_le_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (productMap Q₁ Q₂)).card ≤
+      (QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card := by
+  rw [productMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Rules on the reachable product image have search-space size
+`|A| ^ |image(productMap Q₁ Q₂)|`.
+-/
+theorem card_productImageQuotientRules
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (productMap Q₁ Q₂) → A) =
+      Fintype.card A ^ (QuotientImageFinset (productMap Q₁ Q₂)).card := by
+  classical
+  letI : Fintype (QuotientImageBucket (productMap Q₁ Q₂)) :=
+    Fintype.ofFinset (QuotientImageFinset (productMap Q₁ Q₂)) (by
+      intro z
+      constructor <;> intro hz <;> exact hz)
+  rw [Fintype.card_fun]
+  congr
+  simp [QuotientImageBucket]
+
+/--
+Rules on the reachable product image have search-space size
+`|A| ^ (|image Q₁| * |image Q₂|)`.
+-/
+theorem card_productImageQuotientRules_eq_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (productMap Q₁ Q₂) → A) =
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_productImageQuotientRules Q₁ Q₂,
+    productMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Product-image quotient rules are bounded by assigning labels to every
+component-image pair.
+-/
+theorem card_productImageQuotientRules_le_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (productMap Q₁ Q₂) → A) ≤
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_productImageQuotientRules_eq_product_images Q₁ Q₂]
+
 namespace RuleFactorsThrough
 
 /-- Pairing two product-factorized targets is equivalent to factoring both components. -/
@@ -301,6 +408,26 @@ structure ComparisonObs (Ω₁ Ω₂ : Type) where
   second : Ω₂
 deriving DecidableEq
 
+/-- Finite comparison observations are equivalent to left/right/right triples. -/
+def comparisonObsEquivProd (Ω₁ Ω₂ : Type) :
+    ComparisonObs Ω₁ Ω₂ ≃ Ω₁ × Ω₂ × Ω₂ where
+  toFun c := (c.left, c.first, c.second)
+  invFun x := {
+    left := x.1
+    first := x.2.1
+    second := x.2.2
+  }
+  left_inv c := by
+    cases c
+    rfl
+  right_inv x := by
+    cases x
+    rfl
+
+noncomputable instance comparisonObsFintype {Ω₁ Ω₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] : Fintype (ComparisonObs Ω₁ Ω₂) :=
+  Fintype.ofEquiv (Ω₁ × Ω₂ × Ω₂) (comparisonObsEquivProd Ω₁ Ω₂).symm
+
 /-- Product quotient for a left item and two right items. -/
 def comparisonMap {Ω₁ Ω₂ Z₁ Z₂ : Type}
     (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
@@ -396,4 +523,149 @@ theorem rankByScore_factorsThrough_of_score_factorsThrough
   cases c
   simp [rankByScore, comparisonMap, hscoreQ]
 
+/-! ## Comparison image bounds -/
+
+/--
+The ambient box of reachable comparison codes induced by one left image and two
+right images.
+-/
+def ComparisonImageBox {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) : Finset (ComparisonObs Z₁ Z₂) :=
+  ((QuotientImageFinset Q₁).product
+      ((QuotientImageFinset Q₂).product (QuotientImageFinset Q₂))).image
+    (fun z => {
+      left := z.1
+      first := z.2.1
+      second := z.2.2
+    })
+
+/--
+The reachable image of a comparison map is contained in the box of reachable
+left/right/right component codes.
+-/
+theorem comparisonMap_image_subset_imageBox
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (comparisonMap Q₁ Q₂) ⊆
+      ComparisonImageBox Q₁ Q₂ := by
+  intro z hz
+  rcases Finset.mem_image.mp hz with ⟨c, _hc, hc⟩
+  rw [← hc]
+  unfold ComparisonImageBox
+  apply Finset.mem_image.mpr
+  refine ⟨(Q₁ c.left, (Q₂ c.first, Q₂ c.second)), ?_, rfl⟩
+  exact Finset.mem_product.mpr
+    ⟨Finset.mem_image.mpr ⟨c.left, Finset.mem_univ c.left, rfl⟩,
+      Finset.mem_product.mpr
+        ⟨Finset.mem_image.mpr ⟨c.first, Finset.mem_univ c.first, rfl⟩,
+          Finset.mem_image.mpr ⟨c.second, Finset.mem_univ c.second, rfl⟩⟩⟩
+
+/--
+The reachable image of a comparison map is exactly the box of reachable
+left/right/right component codes.
+-/
+theorem comparisonMap_image_eq_imageBox
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (comparisonMap Q₁ Q₂) =
+      ComparisonImageBox Q₁ Q₂ := by
+  apply Finset.Subset.antisymm
+  · exact comparisonMap_image_subset_imageBox Q₁ Q₂
+  · intro z hz
+    unfold ComparisonImageBox at hz
+    rcases Finset.mem_image.mp hz with ⟨p, hp, hpz⟩
+    rcases Finset.mem_product.mp hp with ⟨hzleft, hzrights⟩
+    rcases Finset.mem_product.mp hzrights with ⟨hzfirst, hzsecond⟩
+    rcases Finset.mem_image.mp hzleft with ⟨x, _hxmem, hx⟩
+    rcases Finset.mem_image.mp hzfirst with ⟨y₁, _hy₁mem, hy₁⟩
+    rcases Finset.mem_image.mp hzsecond with ⟨y₂, _hy₂mem, hy₂⟩
+    apply Finset.mem_image.mpr
+    refine ⟨{ left := x, first := y₁, second := y₂ }, Finset.mem_univ _, ?_⟩
+    rw [← hpz]
+    simp [comparisonMap, hx, hy₁, hy₂]
+
+/--
+The number of reachable comparison codes is exactly
+`|image Q₁| * |image Q₂| * |image Q₂|`.
+-/
+theorem comparisonMap_image_card_eq_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (comparisonMap Q₁ Q₂)).card =
+      (QuotientImageFinset Q₁).card *
+        (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card := by
+  rw [comparisonMap_image_eq_imageBox Q₁ Q₂]
+  unfold ComparisonImageBox
+  rw [Finset.card_image_of_injective]
+  · simp [mul_assoc]
+  · intro p₁ p₂ h
+    exact Prod.ext (congrArg ComparisonObs.left h)
+      (Prod.ext (congrArg ComparisonObs.first h)
+        (congrArg ComparisonObs.second h))
+
+/--
+The number of reachable comparison codes is bounded by
+`|image Q₁| * |image Q₂| * |image Q₂|`.
+-/
+theorem comparisonMap_image_card_le_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (comparisonMap Q₁ Q₂)).card ≤
+      (QuotientImageFinset Q₁).card *
+        (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card := by
+  rw [comparisonMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Rules on the reachable comparison image have search-space size
+`|A| ^ |image(comparisonMap Q₁ Q₂)|`.
+-/
+theorem card_comparisonImageQuotientRules
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (comparisonMap Q₁ Q₂) → A) =
+      Fintype.card A ^ (QuotientImageFinset (comparisonMap Q₁ Q₂)).card := by
+  classical
+  letI : Fintype (QuotientImageBucket (comparisonMap Q₁ Q₂)) :=
+    Fintype.ofFinset (QuotientImageFinset (comparisonMap Q₁ Q₂)) (by
+      intro z
+      constructor <;> intro hz <;> exact hz)
+  rw [Fintype.card_fun]
+  congr
+  simp [QuotientImageBucket]
+
+/--
+Rules on the reachable comparison image have search-space size
+`|A| ^ (|image Q₁| * |image Q₂| * |image Q₂|)`.
+-/
+theorem card_comparisonImageQuotientRules_eq_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (comparisonMap Q₁ Q₂) → A) =
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card *
+          (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_comparisonImageQuotientRules Q₁ Q₂,
+    comparisonMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Comparison-image quotient rules are bounded by assigning labels to every
+left/right/right component-image triple.
+-/
+theorem card_comparisonImageQuotientRules_le_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (comparisonMap Q₁ Q₂) → A) ≤
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card *
+          (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_comparisonImageQuotientRules_eq_product_images Q₁ Q₂]
+
 end OrdvecFormalization

OrdvecFormalization/Verify.lean

@@ -198,9 +198,17 @@ namespace OrdvecFormalization
 #check @ObservedProductQuotients
 #check @UnobservedReachableProductQuotients
 #check @card_productQuotientRules
+#check @productMap_image_subset_product_images
+#check @productMap_image_eq_product_images
+#check @productMap_image_card_eq_product_images_card
+#check @productMap_image_card_le_product_images_card
+#check @card_productImageQuotientRules
+#check @card_productImageQuotientRules_eq_product_images
+#check @card_productImageQuotientRules_le_product_images
 #check @RuleFactorsThrough.product_pair_iff
 #check @ProductSampleConsistent.prod_iff
 #check @ComparisonObs
+#check @comparisonObsEquivProd
 #check @comparisonMap
 #check @comparisonMap_left
 #check @comparisonMap_first
@@ -210,6 +218,14 @@ namespace OrdvecFormalization
 #check @ruleFactorsThrough_comparison_fiberInvariant
 #check @rankByScore
 #check @rankByScore_factorsThrough_of_score_factorsThrough
+#check @ComparisonImageBox
+#check @comparisonMap_image_subset_imageBox
+#check @comparisonMap_image_eq_imageBox
+#check @comparisonMap_image_card_eq_product_images_card
+#check @comparisonMap_image_card_le_product_images_card
+#check @card_comparisonImageQuotientRules
+#check @card_comparisonImageQuotientRules_eq_product_images
+#check @card_comparisonImageQuotientRules_le_product_images
 #check @pairQuotient
 #check @pairQuotient_apply
 #check @pairQuotient_eq_iff
@@ -482,11 +498,25 @@ namespace OrdvecFormalization
 #print axioms productSampleConsistent_iff_exists_productRuleFitsSample
 #print axioms no_productQuotientTarget_of_sample_collision
 #print axioms card_productQuotientRules
+#print axioms productMap_image_subset_product_images
+#print axioms productMap_image_eq_product_images
+#print axioms productMap_image_card_eq_product_images_card
+#print axioms productMap_image_card_le_product_images_card
+#print axioms card_productImageQuotientRules
+#print axioms card_productImageQuotientRules_eq_product_images
+#print axioms card_productImageQuotientRules_le_product_images
 #print axioms RuleFactorsThrough.product_pair_iff
 #print axioms ProductSampleConsistent.prod_iff
 #print axioms comparisonMap_eq_iff
 #print axioms ruleFactorsThrough_comparison_fiberInvariant
 #print axioms rankByScore_factorsThrough_of_score_factorsThrough
+#print axioms comparisonMap_image_subset_imageBox
+#print axioms comparisonMap_image_eq_imageBox
+#print axioms comparisonMap_image_card_eq_product_images_card
+#print axioms comparisonMap_image_card_le_product_images_card
+#print axioms card_comparisonImageQuotientRules
+#print axioms card_comparisonImageQuotientRules_eq_product_images
+#print axioms card_comparisonImageQuotientRules_le_product_images
 #print axioms pairQuotient_eq_iff
 #print axioms pairRuleFactorsThrough_same_on_quotient_fibers
 #print axioms no_pair_compatible_target_of_sample_collision