ConditionedCoordinates.lean

1 import KomorebiVerification.TopologicalCompletion
2 import Mathlib.Analysis.Normed.Operator.NormedSpace
3 
4 /-!
5 # Conditioned packet coordinates
6 
7 This constructs the condition-number definition and proves the two-sided
8 operator norm comparison.  The general statement applies to any chosen
9 bounded coordinate isomorphism, so it is not restricted to a particular
10 finite product norm.  Only the lower bound by one requires a nonzero space.
11 -/
12 
13 set_option autoImplicit false
14 noncomputable section
15 
16 namespace Komorebi.PaperICompletion.ConditionedCoordinates
17 
18 universe u v w
19 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
20 variable {X : Type v} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
21 variable {Y : Type w} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
22 
23 /-- Product of the genuine operator norms of a coordinate map and its inverse. -/
24 def conditionNumber (e : X ≃L[𝕜] Y) : ℝ :=
25   ‖e.toContinuousLinearMap‖ * ‖e.symm.toContinuousLinearMap‖
26 
27 theorem conditionNumber_nonneg (e : X ≃L[𝕜] Y) : 0 ≤ conditionNumber e :=
28   mul_nonneg (norm_nonneg _) (norm_nonneg _)
29 
30 theorem conditionNumber_symm (e : X ≃L[𝕜] Y) :
31     conditionNumber e.symm = conditionNumber e := by
32   simp only [conditionNumber, ContinuousLinearEquiv.symm_symm, mul_comm]
33 
34 /-- A coordinate condition number is at least one on a nonzero space. -/
35 theorem one_le_conditionNumber [Nontrivial X] (e : X ≃L[𝕜] Y) :
36     1 ≤ conditionNumber e := e.one_le_norm_mul_norm_symm
37 
38 /-- Bounded coordinate conjugation of the actual operator. -/
39 def coordinateOperator (e : X ≃L[𝕜] Y) (T : X →L[𝕜] X) : Y →L[𝕜] Y :=
40   e.toContinuousLinearMap.comp (T.comp e.symm.toContinuousLinearMap)
41 
42 theorem coordinateOperator_inverse (e : X ≃L[𝕜] Y) (T : X →L[𝕜] X) :
43     coordinateOperator e.symm (coordinateOperator e T) = T := by
44   ext x
45   simp [coordinateOperator]
46 
47 /-- Forward condition-number bound. -/
48 theorem norm_coordinateOperator_le (e : X ≃L[𝕜] Y) (T : X →L[𝕜] X) :
49     ‖coordinateOperator e T‖ ≤ conditionNumber e * ‖T‖ := by
50   calc
51     ‖coordinateOperator e T‖ ≤ ‖e.toContinuousLinearMap‖ *
52         ‖T.comp e.symm.toContinuousLinearMap‖ :=
53       ContinuousLinearMap.opNorm_comp_le _ _
54     _ ≤ ‖e.toContinuousLinearMap‖ * (‖T‖ * ‖e.symm.toContinuousLinearMap‖) :=
55       mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _)
56     _ = conditionNumber e * ‖T‖ := by unfold conditionNumber; ring
57 
58 /-- Reverse condition-number bound. -/
59 theorem norm_le_conditionNumber_mul_coordinateOperator
60     (e : X ≃L[𝕜] Y) (T : X →L[𝕜] X) :
61     ‖T‖ ≤ conditionNumber e * ‖coordinateOperator e T‖ := by
62   simpa only [coordinateOperator_inverse, conditionNumber_symm] using
63     norm_coordinateOperator_le e.symm (coordinateOperator e T)
64 
65 /-- On the zero space the condition number is zero, not at least one. -/
66 theorem conditionNumber_eq_zero_of_subsingleton [Subsingleton X]
67     (e : X ≃L[𝕜] Y) : conditionNumber e = 0 := by
68   have he : e.toContinuousLinearMap = 0 := by
69     ext x
70     rw [Subsingleton.elim x 0, map_zero]
71     rfl
72   simp [conditionNumber, he]
73 
74 section Packets
75 open KomorebiVerification.TopologicalCompletion
76 variable {ι : Type*} [Fintype ι]
77 
78 /-- Packet-coordinate condition number in the canonical product norm. -/
79 def packetConditionNumber (P : BoundedProjectorFamily 𝕜 X ι) : ℝ :=
80   conditionNumber P.packetEquiv
81 
82 theorem packetConditionNumber_eq (P : BoundedProjectorFamily 𝕜 X ι) :
83     packetConditionNumber P = ‖P.analysis‖ * ‖P.synthesis‖ := rfl
84 
85 /-- Both bounds of the publication proposition, with literal packet analysis and synthesis. -/
86 theorem packet_conditioned_coordinate_bounds
87     (P : BoundedProjectorFamily 𝕜 X ι) (T : X →L[𝕜] X) :
88     ‖P.analysis.comp (T.comp P.synthesis)‖ ≤ packetConditionNumber P * ‖T‖ ∧
89       ‖T‖ ≤ packetConditionNumber P * ‖P.analysis.comp (T.comp P.synthesis)‖ :=
90   ⟨norm_coordinateOperator_le P.packetEquiv T,
91     norm_le_conditionNumber_mul_coordinateOperator P.packetEquiv T⟩
92 
93 end Packets
94 end Komorebi.PaperICompletion.ConditionedCoordinates

Back to source controls