FinitePartitions.lean

1 import KomorebiLSM.FiniteBayes
2 import Mathlib.Data.Setoid.Partition
3 import Mathlib.Data.Fintype.Card
4 
5 /-! Finite partitions with block aggregation and strict-refinement cardinality. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.FinitePartitions
8 open scoped BigOperators
9 open FiniteBayes
10 universe u v
11 variable {I : Type u} [Fintype I]
12 
13 noncomputable instance quotientEnumeration (r : Setoid I) : Fintype (Quotient r) :=
14   Fintype.ofFinite _
15 
16 noncomputable def blockCount (r : Setoid I) : ℕ := Fintype.card (Quotient r)
17 
18 def coarsenMap {r s : Setoid I} (h : r ≤ s) : Quotient r → Quotient s :=
19   Quotient.map' id (fun _ _ hxy => h hxy)
20 
21 omit [Fintype I] in
22 @[simp] theorem coarsenMap_mk {r s : Setoid I} (h : r ≤ s) (i : I) :
23     coarsenMap h (Quotient.mk r i) = Quotient.mk s i := rfl
24 
25 omit [Fintype I] in
26 theorem coarsenMap_surjective {r s : Setoid I} (h : r ≤ s) :
27     Function.Surjective (coarsenMap h) := by
28   intro q
29   induction q using Quotient.inductionOn with
30   | h i => exact ⟨Quotient.mk r i, rfl⟩
31 
32 theorem blockCount_le (r : Setoid I) : blockCount r ≤ Fintype.card I :=
33   Fintype.card_le_of_surjective (Quotient.mk r) Quotient.mk_surjective
34 
35 theorem blockCount_refines {r s : Setoid I} (h : r ≤ s) : blockCount s ≤ blockCount r :=
36   Fintype.card_le_of_surjective (coarsenMap h) (coarsenMap_surjective h)
37 
38 theorem equal_of_refines_card {r s : Setoid I} (h : r ≤ s)
39     (hc : blockCount r = blockCount s) : r = s := by
40   have hinj : Function.Injective (coarsenMap h) :=
41     ((Fintype.bijective_iff_surjective_and_card (coarsenMap h)).mpr
42       ⟨coarsenMap_surjective h, hc⟩).1
43   apply le_antisymm h
44   intro i j hij
45   exact Quotient.exact (hinj (show coarsenMap h (Quotient.mk r i) =
46     coarsenMap h (Quotient.mk r j) from Quotient.sound hij))
47 
48 theorem strict_refinement_count {r s : Setoid I} (h : r ≤ s) (hne : r ≠ s) :
49     blockCount s < blockCount r := by
50   have hle := blockCount_refines h
51   have hneq : blockCount r ≠ blockCount s := fun hc => hne (equal_of_refines_card h hc)
52   omega
53 
54 noncomputable def blockAggregate (r : Setoid I) (p : I → ℝ) : Quotient r → ℝ := by
55   classical
56   exact aggregate (Quotient.mk r) p
57 
58 noncomputable def blockMass (r : Setoid I) (p : I → ℝ) (j : I) : ℝ := by
59   classical
60   exact ∑ i, if r i j then p i else 0
61 
62 @[simp] theorem blockAggregate_mk (r : Setoid I) (p : I → ℝ) (j : I) :
63     blockAggregate r p (Quotient.mk r j) = blockMass r p j := by
64   classical
65   simp only [blockAggregate, aggregate, blockMass, Quotient.eq_iff_equiv]
66 
67 theorem blockAggregate_comp {r s : Setoid I} (h : r ≤ s) (p : I → ℝ) :
68     blockAggregate s p = by classical exact aggregate (coarsenMap h) (blockAggregate r p) := by
69   classical
70   simp only [blockAggregate, aggregate_comp]
71   rfl
72 
73 theorem same_fine_implies_same_coarse {r s : Setoid I} (h : r ≤ s) (p q : I → ℝ)
74     (he : blockAggregate r p = blockAggregate r q) :
75     blockAggregate s p = blockAggregate s q := by
76   classical
77   rw [blockAggregate_comp h p, blockAggregate_comp h q, he]
78 
79 theorem blockCount_kernel {A : Type v} [Fintype A] (c : I → A)
80     (hc : Function.Surjective c) : blockCount (Setoid.ker c) = Fintype.card A := by
81   let f : Quotient (Setoid.ker c) → A := Quotient.lift c (fun _ _ h => h)
82   have hfi : Function.Injective f := by
83     intro p q
84     induction p using Quotient.inductionOn with
85     | h i =>
86       induction q using Quotient.inductionOn with
87       | h j => intro h; exact Quotient.sound h
88   have hfs : Function.Surjective f := by
89     intro a
90     obtain ⟨i, hi⟩ := hc a
91     exact ⟨Quotient.mk (Setoid.ker c) i, hi⟩
92   exact Fintype.card_of_bijective ⟨hfi, hfs⟩
93 
94 end Komorebi.LSM.FinitePartitions

Back to source controls