GeneralNormedPackets.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiVerification.MathlibImports
7 
8 /-!
9 # Finite packet maps over any normed field
10 
11 The continuous coordinate identities do not require a nontrivial valuation.
12 The separate GeneralPacketBounds module uses actual projector norm bounds,
13 since continuity alone need not imply boundedness over a trivially valued field.
14 -/
15 
16 set_option autoImplicit false
17 noncomputable section
18 
19 open scoped BigOperators InnerProduct lp
20 open Set Function UniformSpace
21 
22 namespace Komorebi.PaperIRelease.GeneralNormedPackets
23 
24 /-! ## Finite bounded packet systems -/
25 
26 /-- A finite family of continuous projectors which is pairwise annihilating and
27 sums pointwise to the identity. -/
28 structure ContinuousProjectorFamily
29     (𝕜 : Type*) (X : Type*) (ι : Type*)
30     [NormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
31     [Fintype ι] where
32   proj : ι → X →L[𝕜] X
33   idempotent : ∀ i x, proj i (proj i x) = proj i x
34   annihilate : ∀ {i j}, i ≠ j → ∀ x, proj i (proj j x) = 0
35   complete : ∀ x, (∑ i, proj i x) = x
36 
37 namespace ContinuousProjectorFamily
38 
39 variable {𝕜 X ι : Type*}
40 variable [NormedField 𝕜]
41 variable [NormedAddCommGroup X] [NormedSpace 𝕜 X]
42 variable [Fintype ι]
43 
44 /-- The `i`th packet is the range of its continuous projector. -/
45 def packet (P : ContinuousProjectorFamily 𝕜 X ι) (i : ι) : Submodule 𝕜 X :=
46   (P.proj i).range
47 
48 /-- Every packet range is closed. -/
49 theorem isClosed_packet (P : ContinuousProjectorFamily 𝕜 X ι) (i : ι) :
50     IsClosed (P.packet i : Set X) := by
51   apply ContinuousLinearMap.IsIdempotentElem.isClosed_range
52   apply ContinuousLinearMap.ext
53   intro x
54   exact P.idempotent i x
55 
56 /-- Analysis into the finite product of packet ranges. -/
57 def analysis (P : ContinuousProjectorFamily 𝕜 X ι) :
58     X →L[𝕜] ∀ i, P.packet i :=
59   ContinuousLinearMap.pi fun i ↦
60     (P.proj i).codRestrict (P.packet i) fun x ↦ by
61       change P.proj i x ∈ (P.proj i).range
62       exact ⟨x, rfl⟩
63 
64 @[simp]
65 theorem analysis_apply_coe (P : ContinuousProjectorFamily 𝕜 X ι) (x : X) (i : ι) :
66     ((P.analysis x i : P.packet i) : X) = P.proj i x :=
67   by simp [analysis]
68 
69 /-- Synthesis is the finite sum of the packet inclusions. -/
70 def synthesis (P : ContinuousProjectorFamily 𝕜 X ι) :
71     (∀ i, P.packet i) →L[𝕜] X :=
72   ∑ i, (P.packet i).subtypeL.comp (ContinuousLinearMap.proj i)
73 
74 @[simp]
75 theorem synthesis_apply (P : ContinuousProjectorFamily 𝕜 X ι)
76     (x : ∀ i, P.packet i) :
77     P.synthesis x = ∑ i, (x i : X) := by
78   simp [synthesis]
79 
80 @[simp]
81 theorem synthesis_analysis (P : ContinuousProjectorFamily 𝕜 X ι) (x : X) :
82     P.synthesis (P.analysis x) = x := by
83   simpa [synthesis] using P.complete x
84 
85 @[simp]
86 theorem analysis_synthesis (P : ContinuousProjectorFamily 𝕜 X ι)
87     (x : ∀ i, P.packet i) :
88     P.analysis (P.synthesis x) = x := by
89   classical
90   ext i
91   rw [analysis_apply_coe, synthesis_apply]
92   change P.proj i (∑ j, (x j : X)) = (x i : X)
93   rw [map_sum, Finset.sum_eq_single i]
94   · rcases (x i).property with ⟨y, hy⟩
95     rw [← hy]
96     exact P.idempotent i y
97   · intro j _ hji
98     rcases (x j).property with ⟨y, hy⟩
99     rw [← hy]
100     exact P.annihilate hji.symm y
101   · simp
102 
103 /-- The topological packet isomorphism: continuous analysis and synthesis are
104 mutually inverse.  A finite product is the finite direct sum as a vector
105 space, and carries one of its equivalent finite-product norms. -/
106 def packetEquiv (P : ContinuousProjectorFamily 𝕜 X ι) :
107     X ≃L[𝕜] ∀ i, P.packet i :=
108   ContinuousLinearEquiv.equivOfInverse P.analysis P.synthesis
109     P.synthesis_analysis P.analysis_synthesis
110 
111 @[simp]
112 theorem packetEquiv_apply (P : ContinuousProjectorFamily 𝕜 X ι) (x : X) :
113     P.packetEquiv x = P.analysis x :=
114   rfl
115 
116 /-- Literal Banach-space wrapper for the topological packet theorem.  It
117 packages both manuscript conclusions: every packet is closed and analysis is
118 a continuous linear isomorphism whose forward and inverse maps are the declared
119 analysis and synthesis operators. -/
120 theorem topological_packet_isomorphism [CompleteSpace X]
121     (P : ContinuousProjectorFamily 𝕜 X ι) :
122     (∀ i, IsClosed (P.packet i : Set X)) ∧
123       ∃ e : X ≃L[𝕜] ∀ i, P.packet i,
124         e.toContinuousLinearMap = P.analysis ∧
125           e.symm.toContinuousLinearMap = P.synthesis := by
126   refine ⟨P.isClosed_packet, P.packetEquiv, rfl, ?_⟩
127   rfl
128 
129 /-! ## Completion preserves finite packet extraction -/
130 
131 /-- The image of a dense submodule under an arbitrary bounded idempotent is
132 dense in the full range.  This is the literal manuscript completion lemma;
133 it does not require the projector to belong to a finite packet family. -/
134 theorem idempotentRange_eq_closure_map
135     (Q : X →L[𝕜] X) (hQ : ∀ x, Q (Q x) = Q x)
136     (M : Submodule 𝕜 X) (hM : M.topologicalClosure = ⊤) :
137     (M.map Q.toLinearMap).topologicalClosure = Q.range := by
138   have hclosed : IsClosed (Q.range : Set X) := by
139     apply ContinuousLinearMap.IsIdempotentElem.isClosed_range
140     apply ContinuousLinearMap.ext
141     intro x
142     exact hQ x
143   apply le_antisymm
144   · apply Submodule.topologicalClosure_minimal
145     · exact LinearMap.map_le_range
146     · exact hclosed
147   · have h := Submodule.topologicalClosure_map Q M
148     rw [hM] at h
149     simpa using h
150 
151 /-- For a dense submodule `M`, the image of `M` under any bounded idempotent
152 projector is dense in the full packet range.  This is the exact completion
153 claim `P_i X = closure (P_i M)`, stated as equality of submodules.  The result
154 is slightly stronger than the manuscript statement because invariance
155 `P_i M ⊆ M` is not needed for this equality. -/
156 theorem packetRange_eq_closure_map
157     (P : ContinuousProjectorFamily 𝕜 X ι) (M : Submodule 𝕜 X)
158     (hM : M.topologicalClosure = ⊤) (i : ι) :
159     (M.map (P.proj i).toLinearMap).topologicalClosure = P.packet i := by
160   simpa [packet] using
161     idempotentRange_eq_closure_map (P.proj i) (P.idempotent i) M hM
162 
163 
164 end ContinuousProjectorFamily
165 end Komorebi.PaperIRelease.GeneralNormedPackets

Back to source controls