source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 
5 SECTION 17 FINITE MULTILINEAR PACKET IDENTITIES.
6 Compiled with the pinned Lean compiler in the release verification.
7 Imported by PaperIIIContinuation and included in the owned declaration census.
8 -/
9 import KomorebiPaperIII.PacketCoordinates
10 import Mathlib.LinearAlgebra.Multilinear.Basic
11 
12 set_option autoImplicit false
13 noncomputable section
14 open scoped BigOperators
15 
16 namespace Komorebi.PaperIII.PacketCoordinates
17 universe u v w x y z
18 variable {R : Type u} [Semiring R]
19 variable {M : Type v} {N : Type w}
20 variable [AddCommMonoid M] [Module R M]
21 variable [AddCommMonoid N] [Module R N]
22 variable {I : Type x} {J : Type y} [Fintype I] [Fintype J]
23 variable {n : Nat}
24 
25 /-- A finite resolution of the identity is already enough for the full
26     multilinear expansion. Idempotence and pairwise annihilation are NOT used
27     in this identity: they are needed later to make packet coordinates into
28     an actual independent direct-sum representation. -/
29 theorem reconstruction_from_resolutions
30     (Ps : I → M →ₗ[R] M) (Qs : J → N →ₗ[R] N)
31     (hPs : ∑ i : I, Ps i = LinearMap.id)
32     (hQs : ∑ j : J, Qs j = LinearMap.id)
33     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
34     (h : Fin n → M) :
35     B h = ∑ gamma : J, ∑ alpha : Fin n → I,
36       Qs gamma (B (fun k => Ps (alpha k) (h k))) := by
37   classical
38   have hslot (k : Fin n) : (∑ i : I, Ps i (h k)) = h k := by
39     simpa only [LinearMap.sum_apply, LinearMap.id_apply] using
40       LinearMap.congr_fun hPs (h k)
41   have hout : (∑ gamma : J, Qs gamma (B h)) = B h := by
42     simpa only [LinearMap.sum_apply, LinearMap.id_apply] using
43       LinearMap.congr_fun hQs (B h)
44   have hinput : B h = ∑ alpha : Fin n → I,
45       B (fun k => Ps (alpha k) (h k)) := by
46     calc
47       B h = B (fun k => ∑ i : I, Ps i (h k)) := by
48         congr 1
49         funext k
50         exact (hslot k).symm
51       _ = ∑ alpha : Fin n → I,
52           B (fun k => Ps (alpha k) (h k)) := by
53         exact B.map_sum (fun (k : Fin n) (i : I) => Ps i (h k))
54   calc
55     B h = ∑ gamma : J, Qs gamma (B h) := hout.symm
56     _ = ∑ gamma : J,
57           Qs gamma (∑ alpha : Fin n → I,
58             B (fun k => Ps (alpha k) (h k))) := by rw [hinput]
59     _ = ∑ gamma : J, ∑ alpha : Fin n → I,
60           Qs gamma (B (fun k => Ps (alpha k) (h k))) := by
61           simp only [map_sum]
62 
63 /-- A labelled packet jet extended to the ambient slots; no range certificate
64     and no pre-established coordinate equivalence is assumed. -/
65 def ambientJet (P : System R M I) (Q : System R N J)
66     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
67     (gamma : J) (alpha : Fin n → I) :
68     MultilinearMap R (fun (_ : Fin n) => M) N :=
69   (Q.projector gamma).compMultilinearMap
70     (B.compLinearMap (fun k => P.projector (alpha k)))
71 
72 @[simp] theorem ambientJet_apply (P : System R M I) (Q : System R N J)
73     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
74     (gamma : J) (alpha : Fin n → I) (h : Fin n → M) :
75     ambientJet P Q B gamma alpha h =
76       Q.projector gamma (B (fun k => P.projector (alpha k) (h k))) := rfl
77 
78 /-- The manuscript's packet jet is literally defined on the actual input
79     projector ranges and has the actual output projector range as codomain. -/
80 def packetJet (P : System R M I) (Q : System R N J)
81     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
82     (gamma : J) (alpha : Fin n → I) :
83     MultilinearMap R
84       (fun k : Fin n => LinearMap.range (P.projector (alpha k)))
85       (LinearMap.range (Q.projector gamma)) :=
86   ((Q.projector gamma).compMultilinearMap
87     (B.compLinearMap (fun k =>
88       (LinearMap.range (P.projector (alpha k))).subtype))).codRestrict
89     (LinearMap.range (Q.projector gamma))
90     (by
91       intro xs
92       refine ⟨B (fun k => (xs k : M)), ?_⟩
93       rfl)
94 
95 /-- Evaluate a genuine range-to-range block, then coerce its output to N. -/
96 @[simp] theorem packetJet_apply_coe (P : System R M I) (Q : System R N J)
97     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
98     (gamma : J) (alpha : Fin n → I)
99     (xs : (k : Fin n) → LinearMap.range (P.projector (alpha k))) :
100     (packetJet P Q B gamma alpha xs : N) =
101       Q.projector gamma (B (fun k => (xs k : M))) := rfl
102 
103 /-- Input reconstruction by expanding every argument using completeness;
104     this also works when B is not symmetric and n = 0. -/
105 theorem multilinear_input_expansion (P : System R M I)
106     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
107     (h : Fin n → M) :
108     B h = ∑ alpha : Fin n → I,
109       B (fun k => P.projector (alpha k) (h k)) := by
110   classical
111   have hslot (k : Fin n) :
112       (∑ i : I, P.projector i (h k)) = h k := by
113     simpa only [P.synthesis_apply, P.analysis_apply] using
114       P.synthesis_analysis (h k)
115   calc
116     B h = B (fun k => ∑ i : I, P.projector i (h k)) := by
117       congr 1
118       funext k
119       exact (hslot k).symm
120     _ = ∑ alpha : Fin n → I,
121         B (fun k => P.projector (alpha k) (h k)) := by
122       exact B.map_sum (fun (k : Fin n) (i : I) => P.projector i (h k))
123 
124 /-- The input-output packet reconstruction identity, with no independent
125     splitting certificate. In particular it applies to each continuous
126     Frechet derivative, after forgetting continuity. -/
127 theorem multilinear_packet_reconstruction
128     (P : System R M I) (Q : System R N J)
129     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
130     (h : Fin n → M) :
131     B h = ∑ gamma : J, ∑ alpha : Fin n → I,
132       (packetJet P Q B gamma alpha
133         (fun k => P.analysis (h k) (alpha k)) : N) := by
134   classical
135   calc
136     B h = ∑ gamma : J, ∑ alpha : Fin n → I,
137       Q.projector gamma
138         (B (fun k => P.projector (alpha k) (h k))) :=
139       reconstruction_from_resolutions P.projector Q.projector
140         P.complete Q.complete B h
141     _ = ∑ gamma : J, ∑ alpha : Fin n → I,
142       (packetJet P Q B gamma alpha
143         (fun k => P.analysis (h k) (alpha k)) : N) := by
144       simp only [packetJet_apply_coe, P.analysis_apply]
145 
146 /-- On projected ambient vectors, the range jet and the ambient extension
147     agree literally. This guards against accidentally dropping cross slots. -/
148 theorem packetJet_eq_ambientJet_on_analysis
149     (P : System R M I) (Q : System R N J)
150     (B : MultilinearMap R (fun (_ : Fin n) => M) N)
151     (gamma : J) (alpha : Fin n → I) (h : Fin n → M) :
152     (packetJet P Q B gamma alpha
153       (fun k => P.analysis (h k) (alpha k)) : N) =
154       ambientJet P Q B gamma alpha h := by
155   simp only [packetJet_apply_coe, P.analysis_apply, ambientJet_apply]
156 
157 end Komorebi.PaperIII.PacketCoordinates

Back to source controls