BandedCount.lean

1 module
2 public import Mathlib.Order.Interval.Finset.Fin
3 public import Mathlib.Algebra.BigOperators.Fin
4 public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
5 public import Mathlib.Tactic
6 
7 /-!
8 Author: Komorebi P. Paper VIII item 4.1.
9 Counts actual finite addresses, not a recurrence assumed to describe them.
10 One scalar multiplication and one accumulation are two modeled operations.
11 -/
12 public section
13 set_option autoImplicit false
14 namespace KomorebiPaperVIII
15 open scoped BigOperators Classical
16 
17 abbrev BandedAddress (p w : ℕ) :=
18   {e : Fin p × Fin p // e.1.val ≤ e.2.val+w ∧ e.2.val ≤ e.1.val+w}
19 
20 noncomputable def bandCount (p w : ℕ) : ℕ :=
21   ∑ i : Fin p, ∑ j : Fin p,
22     if i.val ≤ j.val+w ∧ j.val ≤ i.val+w then 1 else 0
23 
24 theorem bandCount_card (p w : ℕ) : Fintype.card (BandedAddress p w) = bandCount p w := by
25   simp only [BandedAddress,Fintype.card_subtype,Finset.card_filter,Fintype.sum_prod_type,bandCount]
26 
27 theorem finite_prefix_count (p w : ℕ) (hw : w ≤ p) :
28     (∑ i : Fin p, if i.val < w then 1 else 0) = w := by
29   by_cases he : w = p
30   · subst w
31     simp
32   · let a : Fin p := ⟨w,by omega⟩
33     have hf : Finset.univ.filter (fun i : Fin p => i.val < w) = Finset.Iio a := by
34       ext i
35       simp [a,Fin.lt_def]
36     rw [←Finset.card_filter,hf,Fin.card_Iio]
37 
38 theorem bandCount_succ (p w : ℕ) (hw : w ≤ p) :
39     bandCount (p+1) w = bandCount p w + 2*w+1 := by
40   have hc : (∑ i : Fin p, if i.val+1 ≤ w then 1 else 0) = w := by
41     simpa only [Nat.succ_le_iff] using finite_prefix_count p w hw
42   have hpred (i j : Fin p) :
43       (i.val+1 ≤ j.val+1+w ∧ j.val+1 ≤ i.val+1+w) ↔
44       (i.val ≤ j.val+w ∧ j.val ≤ i.val+w) := by omega
45   simp only [bandCount,Fin.sum_univ_succ,Fin.val_zero,Fin.val_succ,
46     Nat.zero_add,Nat.zero_le,true_and,and_true,hpred,Finset.sum_add_distrib]
47   simp only [hc,ite_true]
48   omega
49 
50 theorem bandCount_full (p : ℕ) : bandCount (p+1) p = (p+1)^2 := by
51   have hpred (i j : Fin (p+1)) : i.val ≤ j.val+p ∧ j.val ≤ i.val+p := by
52     have hi := i.isLt
53     have hj := j.isLt
54     omega
55   simp [bandCount,hpred,pow_two]
56 
57 /-- Subtraction-free count identity, avoiding truncated-natural ambiguity. -/
58 theorem bandCount_balance (p w : ℕ) (hw : w < p) :
59     bandCount p w + w*(w+1) = p*(2*w+1) := by
60   induction p with
61   | zero => omega
62   | succ p ih =>
63     by_cases he : w = p
64     · subst w
65       rw [bandCount_full]
66       ring
67     · have hwp : w < p := by omega
68       have hi := ih hwp
69       rw [bandCount_succ p w (by omega)]
70       nlinarith
71 
72 /-- Item 4.1: exact cardinality of the active block address set. -/
73 theorem banded_block_count (p w : ℕ) (hw : w < p) :
74     Fintype.card (BandedAddress p w) = p*(2*w+1)-w*(w+1) := by
75   rw [bandCount_card]
76   have he := bandCount_balance p w hw
77   omega
78 
79 /-- Scalar entries in an explicitly stored banded block representation. -/
80 abbrev BandedStorage (p w b : ℕ) := BandedAddress p w × Fin b × Fin b
81 
82 /-- One event for each multiply or accumulation, RHS, address and local scalar. -/
83 abbrev BandedOperation (p w b q : ℕ) := Fin 2 × Fin q × BandedStorage p w b
84 
85 theorem banded_storage_count (p w b : ℕ) (hw : w < p) :
86     Fintype.card (BandedStorage p w b) = b^2*(p*(2*w+1)-w*(w+1)) := by
87   simp only [BandedStorage,Fintype.card_prod,Fintype.card_fin,banded_block_count p w hw]
88   ring
89 
90 theorem banded_operation_count (p w b q : ℕ) (hw : w < p) :
91     Fintype.card (BandedOperation p w b q) = 2*q*b^2*(p*(2*w+1)-w*(w+1)) := by
92   simp only [BandedOperation,Fintype.card_prod,Fintype.card_fin,
93     banded_storage_count p w b hw]
94   ring
95 
96 theorem banded_diagonal_case (p : ℕ) (hp : 0 < p) :
97     Fintype.card (BandedAddress p 0) = p := by
98   simpa using banded_block_count p 0 hp
99 
100 end KomorebiPaperVIII
101 
102 -- FIFTH BLOCK AXIOM AUDIT
103 #print axioms KomorebiPaperVIII.bandCount_card
104 #print axioms KomorebiPaperVIII.finite_prefix_count
105 #print axioms KomorebiPaperVIII.bandCount_succ
106 #print axioms KomorebiPaperVIII.bandCount_full
107 #print axioms KomorebiPaperVIII.bandCount_balance
108 #print axioms KomorebiPaperVIII.banded_block_count
109 #print axioms KomorebiPaperVIII.banded_storage_count
110 #print axioms KomorebiPaperVIII.banded_operation_count
111 #print axioms KomorebiPaperVIII.banded_diagonal_case
112 #print axioms KomorebiPaperVIII.BandedAddress
113 #print axioms KomorebiPaperVIII.BandedStorage
114 #print axioms KomorebiPaperVIII.BandedOperation
115 #print axioms KomorebiPaperVIII.bandCount

Back to source controls