PacketEquivalentNorm.lean

1 import KomorebiVerification.TopologicalCompletion
2 
3 set_option autoImplicit false
4 noncomputable section
5 
6 namespace Komorebi.PaperIRelease.PacketEquivalentNorm
7 
8 open KomorebiVerification.TopologicalCompletion
9 
10 variable {𝕜 X Y I : Type*} [NontriviallyNormedField 𝕜]
11 variable [NormedAddCommGroup X] [NormedSpace 𝕜 X]
12 variable [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [Fintype I]
13 
14 /-- A linear identification carrying a norm equivalent to the canonical
15 finite product norm gives the same bounded inverse packet maps. The two
16 inequalities are exactly the declared norm equivalence, not bounds assumed
17 for the packet analysis or synthesis maps. -/
18 def packetEquivOfEquivalentNorm (P : BoundedProjectorFamily 𝕜 X I)
19     (e : (∀ i, P.packet i) ≃ₗ[𝕜] Y) (C D : ℝ)
20     (hC : ∀ z, ‖e z‖ ≤ C * ‖z‖)
21     (hD : ∀ y, ‖e.symm y‖ ≤ D * ‖y‖) : X ≃L[𝕜] Y :=
22   P.packetEquiv.trans
23     (ContinuousLinearEquiv.equivOfInverse
24       (e.toLinearMap.mkContinuous C hC)
25       (e.symm.toLinearMap.mkContinuous D hD)
26       e.symm_apply_apply e.apply_symm_apply)
27 
28 /-- Closed packet ranges and bounded, mutually inverse analysis/synthesis
29 for every finite product norm equivalent to the maximum norm. -/
30 theorem finite_packet_equivalent_norm (P : BoundedProjectorFamily 𝕜 X I)
31     (e : (∀ i, P.packet i) ≃ₗ[𝕜] Y) (C D : ℝ)
32     (hC : ∀ z, ‖e z‖ ≤ C * ‖z‖)
33     (hD : ∀ y, ‖e.symm y‖ ≤ D * ‖y‖) :
34     (∀ i, IsClosed (P.packet i : Set X)) ∧
35       ∃ f : X ≃L[𝕜] Y,
36         (∀ x, f x = e (P.analysis x)) ∧
37         (∀ y, f.symm y = P.synthesis (e.symm y)) := by
38   exact ⟨P.isClosed_packet, packetEquivOfEquivalentNorm P e C D hC hD,
39     fun _ => rfl, fun _ => rfl⟩
40 
41 end Komorebi.PaperIRelease.PacketEquivalentNorm

Back to source controls