GeneralConditionedCoordinates.lean

1 import PaperIRelease.GeneralPacketBounds
2 
3 set_option autoImplicit false
4 noncomputable section
5 
6 namespace Komorebi.PaperIRelease.GeneralConditionedCoordinates
7 
8 variable {X Y : Type*} [NormedAddCommGroup X] [NormedAddCommGroup Y]
9 
10 /-- The usual infimum-of-bounds operator norm is available for bounded
11 additive maps without a nontriviality assumption on a scalar valuation. -/
12 def ofBoundedLinear {𝕜 : Type*} [Semiring 𝕜] [Module 𝕜 X] [Module 𝕜 Y]
13     (f : X →ₗ[𝕜] Y) (h : IsBoundedLinearMap 𝕜 f) : NormedAddGroupHom X Y where
14   toFun := f
15   map_add' := f.map_add
16   bound' := by obtain ⟨C, _, hC⟩ := h.bound; exact ⟨C, hC⟩
17 
18 def conditionNumber (A : NormedAddGroupHom X Y) (S : NormedAddGroupHom Y X) : ℝ :=
19   ‖A‖ * ‖S‖
20 
21 def coordinateOperator (A : NormedAddGroupHom X Y) (S : NormedAddGroupHom Y X)
22     (T : NormedAddGroupHom X X) : NormedAddGroupHom Y Y := A.comp (T.comp S)
23 
24 theorem one_le_conditionNumber [Nontrivial X]
25     (A : NormedAddGroupHom X Y) (S : NormedAddGroupHom Y X)
26     (hSA : ∀ x, S (A x) = x) : 1 ≤ conditionNumber A S := by
27   have h : S.comp A = NormedAddGroupHom.id X := by ext x; exact hSA x
28   calc
29     1 = ‖NormedAddGroupHom.id X‖ := (NormedAddGroupHom.norm_id X).symm
30     _ = ‖S.comp A‖ := congrArg norm h.symm
31     _ ≤ ‖S‖ * ‖A‖ := NormedAddGroupHom.norm_comp_le S A
32     _ = conditionNumber A S := by unfold conditionNumber; ring
33 
34 theorem norm_coordinateOperator_le (A : NormedAddGroupHom X Y)
35     (S : NormedAddGroupHom Y X) (T : NormedAddGroupHom X X) :
36     ‖coordinateOperator A S T‖ ≤ conditionNumber A S * ‖T‖ := by
37   calc
38     ‖coordinateOperator A S T‖ ≤ ‖A‖ * ‖T.comp S‖ := NormedAddGroupHom.norm_comp_le _ _
39     _ ≤ ‖A‖ * (‖T‖ * ‖S‖) :=
40       mul_le_mul_of_nonneg_left (NormedAddGroupHom.norm_comp_le _ _) (norm_nonneg _)
41     _ = conditionNumber A S * ‖T‖ := by unfold conditionNumber; ring
42 
43 theorem coordinateOperator_inverse (A : NormedAddGroupHom X Y)
44     (S : NormedAddGroupHom Y X) (hSA : ∀ x, S (A x) = x)
45     (T : NormedAddGroupHom X X) : coordinateOperator S A (coordinateOperator A S T) = T := by
46   ext x
47   change S (A (T (S (A x)))) = T x
48   rw [hSA, hSA]
49 
50 theorem conditioned_coordinate_bounds (A : NormedAddGroupHom X Y)
51     (S : NormedAddGroupHom Y X) (hSA : ∀ x, S (A x) = x)
52     (T : NormedAddGroupHom X X) :
53     ‖coordinateOperator A S T‖ ≤ conditionNumber A S * ‖T‖ ∧
54       ‖T‖ ≤ conditionNumber A S * ‖coordinateOperator A S T‖ := by
55   refine ⟨norm_coordinateOperator_le A S T, ?_⟩
56   have h := norm_coordinateOperator_le S A (coordinateOperator A S T)
57   rw [coordinateOperator_inverse A S hSA T] at h
58   simpa only [conditionNumber, mul_comm ‖S‖ ‖A‖] using h
59 
60 open GeneralNormedPackets
61 
62 variable {𝕜 I : Type*} [NormedField 𝕜] [NormedSpace 𝕜 X] [Fintype I]
63 
64 def packetAnalysis (P : ContinuousProjectorFamily 𝕜 X I)
65     (hb : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i)) :
66     NormedAddGroupHom X (∀ i, P.packet i) :=
67   ofBoundedLinear P.analysis.toLinearMap (P.analysis_isBounded hb)
68 
69 def packetSynthesis (P : ContinuousProjectorFamily 𝕜 X I) :
70     NormedAddGroupHom (∀ i, P.packet i) X :=
71   ofBoundedLinear P.synthesis.toLinearMap P.synthesis_isBounded
72 
73 /-- The abstract norm argument applies to the actual finite-packet maps
74 over every normed field, including a trivially valued one. -/
75 theorem packet_conditioned_coordinate_bounds (P : ContinuousProjectorFamily 𝕜 X I)
76     (hb : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i)) (T : X →ₗ[𝕜] X)
77     (hT : IsBoundedLinearMap 𝕜 T) :
78     ‖coordinateOperator (packetAnalysis P hb) (packetSynthesis P) (ofBoundedLinear T hT)‖ ≤
79         conditionNumber (packetAnalysis P hb) (packetSynthesis P) * ‖ofBoundedLinear T hT‖ ∧
80       ‖ofBoundedLinear T hT‖ ≤ conditionNumber (packetAnalysis P hb) (packetSynthesis P) *
81         ‖coordinateOperator (packetAnalysis P hb) (packetSynthesis P) (ofBoundedLinear T hT)‖ :=
82   conditioned_coordinate_bounds _ _ P.synthesis_analysis _
83 
84 theorem one_le_packet_conditionNumber [Nontrivial X]
85     (P : ContinuousProjectorFamily 𝕜 X I)
86     (hb : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i)) :
87     1 ≤ conditionNumber (packetAnalysis P hb) (packetSynthesis P) :=
88   one_le_conditionNumber _ _ P.synthesis_analysis
89 
90 /-- The same condition number estimates hold in each equivalent finite
91 product norm, with the actual coordinate maps and their usual operator norms. -/
92 theorem equivalent_norm_conditioned_coordinates [NormedSpace 𝕜 Y] [Nontrivial X]
93     (P : ContinuousProjectorFamily 𝕜 X I)
94     (hb : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i))
95     (e : (∀ i, P.packet i) ≃ₗ[𝕜] Y)
96     (C D : ℝ) (hC : ∀ z, ‖e z‖ ≤ C * ‖z‖)
97     (hD : ∀ y, ‖e.symm y‖ ≤ D * ‖y‖) :
98     ∃ (A : NormedAddGroupHom X Y) (S : NormedAddGroupHom Y X),
99       (∀ x, A x = e (P.analysis x)) ∧
100       (∀ y, S y = P.synthesis (e.symm y)) ∧
101       1 ≤ conditionNumber A S ∧
102       ∀ (T : X →ₗ[𝕜] X) (hT : IsBoundedLinearMap 𝕜 T),
103         ‖coordinateOperator A S (ofBoundedLinear T hT)‖ ≤
104           conditionNumber A S * ‖ofBoundedLinear T hT‖ ∧
105         ‖ofBoundedLinear T hT‖ ≤ conditionNumber A S *
106           ‖coordinateOperator A S (ofBoundedLinear T hT)‖ := by
107   obtain ⟨_, hA, hS, hSA, _⟩ := P.equivalent_norm_packet_bounds hb e C D hC hD
108   let A := ofBoundedLinear (e.toLinearMap.comp P.analysis.toLinearMap) hA
109   let S := ofBoundedLinear (P.synthesis.toLinearMap.comp e.symm.toLinearMap) hS
110   exact ⟨A, S, fun _ => rfl, fun _ => rfl, one_le_conditionNumber A S hSA,
111     fun T hT => conditioned_coordinate_bounds A S hSA (ofBoundedLinear T hT)⟩
112 
113 end Komorebi.PaperIRelease.GeneralConditionedCoordinates

Back to source controls