Packets.lean

1 import Mathlib.Data.ZMod.Basic
2 import Mathlib.Tactic
3 
4 /-!
5 Author: Komorebi P.
6 Paper V, first block. Checked source; see the bundled build and axiom audit.
7 Pointwise partition identities are not by themselves the l2 bounded-operator bridge.
8 -/
9 
10 open scoped BigOperators
11 
12 namespace KomorebiPaperV
13 
14 section Packets
15 variable {I R V : Type*} [DecidableEq R] [Zero V]
16 
17 def packet (phase : I → R) (r : R) (x : I → V) : I → V :=
18   fun i => if phase i = r then x i else 0
19 
20 theorem packet_idempotent (phase : I → R) (r : R) (x : I → V) :
21     packet phase r (packet phase r x) = packet phase r x := by
22   funext i
23   by_cases h : phase i = r <;> simp [packet, h]
24 
25 theorem packet_annihilate (phase : I → R) (r s : R) (hne : r ≠ s)
26     (x : I → V) : packet phase r (packet phase s x) = 0 := by
27   funext i
28   by_cases hr : phase i = r
29   · simp [packet, hr, hne]
30   · simp [packet, hr]
31 end Packets
32 
33 section FinitePackets
34 variable {I R S V : Type*} [Fintype R] [DecidableEq R] [AddCommMonoid V]
35 
36 theorem packet_complete (phase : I → R) (x : I → V) (i : I) :
37     (∑ r : R, packet phase r x i) = x i := by
38   classical
39   calc
40     (∑ r : R, packet phase r x i) = packet phase (phase i) x i := by
41       apply Finset.sum_eq_single (phase i)
42       · intro b _ hb
43         simp [packet, Ne.symm hb]
44       · simp
45     _ = x i := by simp [packet]
46 
47 omit [Fintype R] in
48 theorem packet_refinement [Fintype S] [DecidableEq S]
49     (fine : I → S) (coarsen : S → R) (r : R) (x : I → V) (i : I) :
50     packet (coarsen ∘ fine) r x i =
51       ∑ s : S, if coarsen s = r then packet fine s x i else 0 := by
52   classical
53   symm
54   calc
55     (∑ s : S, if coarsen s = r then packet fine s x i else 0) =
56         (if coarsen (fine i) = r then packet fine (fine i) x i else 0) := by
57       apply Finset.sum_eq_single (fine i)
58       · intro b _ hb
59         simp [packet, Ne.symm hb]
60       · simp
61     _ = packet (coarsen ∘ fine) r x i := by
62       simp [packet]
63 end FinitePackets
64 
65 section AddressEquivalence
66 variable {I R Q V : Type*}
67 
68 def analyzeAddress (e : I ≃ R × Q) (x : I → V) : R → Q → V :=
69   fun r q => x (e.symm (r, q))
70 
71 def synthesizeAddress (e : I ≃ R × Q) (c : R → Q → V) : I → V :=
72   fun i => c (e i).1 (e i).2
73 
74 theorem address_synthesize_analyze (e : I ≃ R × Q) (x : I → V) :
75     synthesizeAddress e (analyzeAddress e x) = x := by
76   funext i
77   simp [synthesizeAddress, analyzeAddress]
78 
79 theorem address_analyze_synthesize (e : I ≃ R × Q) (c : R → Q → V) :
80     analyzeAddress e (synthesizeAddress e c) = c := by
81   funext r q
82   simp [synthesizeAddress, analyzeAddress]
83 end AddressEquivalence
84 
85 section IntegerResidues
86 variable {V : Type*} [AddCommMonoid V]
87 
88 def residuePacket (N : ℕ) (r : ZMod N) (x : ℤ → V) : ℤ → V :=
89   packet (fun n : ℤ => (n : ZMod N)) r x
90 
91 theorem residuePacket_idempotent (N : ℕ) (r : ZMod N) (x : ℤ → V) :
92     residuePacket N r (residuePacket N r x) = residuePacket N r x := by
93   exact packet_idempotent (fun n : ℤ => (n : ZMod N)) r x
94 
95 theorem residuePacket_complete (N : ℕ) [NeZero N] (x : ℤ → V) (n : ℤ) :
96     (∑ r : ZMod N, residuePacket N r x n) = x n := by
97   exact packet_complete (fun n : ℤ => (n : ZMod N)) x n
98 end IntegerResidues
99 
100 end KomorebiPaperV

Back to source controls