ContinuousHolonomyResidual.lean

1 import PaperXI.HolonomyResidual
2 import Mathlib.Analysis.Normed.Operator.Basic
3 
4 /-! Continuous forms of the exact residual identity and its conditioning bound.
5 The maps are actual continuous linear equivalences. No isometry is assumed. -/
6 set_option autoImplicit false
7 
8 namespace PaperXI.ContinuousHolonomyResidual
9 
10 variable {K Vr Vu Vv Wr Wu Wv : Type*} [NontriviallyNormedField K]
11 variable [NormedAddCommGroup Vr] [NormedSpace K Vr]
12 variable [NormedAddCommGroup Vu] [NormedSpace K Vu]
13 variable [NormedAddCommGroup Vv] [NormedSpace K Vv]
14 variable [NormedAddCommGroup Wr] [NormedSpace K Wr]
15 variable [NormedAddCommGroup Wu] [NormedSpace K Wu]
16 variable [NormedAddCommGroup Wv] [NormedSpace K Wv]
17 
18 def transported (U : Vr ≃L[K] Wr) (A : Vr ≃L[K] Vu) (B : Wr ≃L[K] Wu) :
19     Vu ≃L[K] Wu := (A.symm.trans U).trans B
20 
21 @[simp] theorem transported_apply (U : Vr ≃L[K] Wr) (A : Vr ≃L[K] Vu)
22     (B : Wr ≃L[K] Wu) (x : Vu) : transported U A B x = B (U (A.symm x)) := rfl
23 
24 @[simp] theorem transported_toLinearEquiv (U : Vr ≃L[K] Wr) (A : Vr ≃L[K] Vu)
25     (B : Wr ≃L[K] Wu) : (transported U A B).toLinearEquiv =
26       HolonomyResidual.transported U.toLinearEquiv A.toLinearEquiv B.toLinearEquiv := rfl
27 
28 def cycleDefect (U : Vr ≃L[K] Wr)
29     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
30     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
31     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv) : Vr →L[K] Wr :=
32   U.toContinuousLinearMap.comp
33       (Av.symm.toContinuousLinearMap.comp (A.toContinuousLinearMap.comp Au.toContinuousLinearMap)) -
34     Bv.symm.toContinuousLinearMap.comp
35       (B.toContinuousLinearMap.comp (Bu.toContinuousLinearMap.comp U.toContinuousLinearMap))
36 
37 def edgeResidual (U : Vr ≃L[K] Wr)
38     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
39     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
40     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv) : Vu →L[K] Wv :=
41   (transported U Av Bv).toContinuousLinearMap.comp A.toContinuousLinearMap -
42     B.toContinuousLinearMap.comp (transported U Au Bu).toContinuousLinearMap
43 
44 @[simp] theorem cycleDefect_toLinearMap (U : Vr ≃L[K] Wr)
45     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
46     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
47     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv) :
48     (cycleDefect U Au Av Bu Bv A B).toLinearMap =
49       HolonomyResidual.cycleDefect U.toLinearEquiv Au.toLinearEquiv Av.toLinearEquiv
50         Bu.toLinearEquiv Bv.toLinearEquiv A.toLinearEquiv B.toLinearEquiv := rfl
51 
52 @[simp] theorem edgeResidual_toLinearMap (U : Vr ≃L[K] Wr)
53     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
54     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
55     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv) :
56     (edgeResidual U Au Av Bu Bv A B).toLinearMap =
57       HolonomyResidual.edgeResidual U.toLinearEquiv Au.toLinearEquiv Av.toLinearEquiv
58         Bu.toLinearEquiv Bv.toLinearEquiv A.toLinearEquiv B.toLinearEquiv := rfl
59 
60 theorem residual_factorization (U : Vr ≃L[K] Wr)
61     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
62     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
63     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv) :
64     edgeResidual U Au Av Bu Bv A B =
65       Bv.toContinuousLinearMap.comp
66         ((cycleDefect U Au Av Bu Bv A B).comp Au.symm.toContinuousLinearMap) := by
67   ext x
68   exact LinearMap.congr_fun (HolonomyResidual.residual_factorization
69     U.toLinearEquiv Au.toLinearEquiv Av.toLinearEquiv Bu.toLinearEquiv
70     Bv.toLinearEquiv A.toLinearEquiv B.toLinearEquiv) x
71 
72 theorem residual_zero_iff (U : Vr ≃L[K] Wr)
73     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
74     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
75     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv) :
76     edgeResidual U Au Av Bu Bv A B = 0 ↔ cycleDefect U Au Av Bu Bv A B = 0 := by
77   rw [residual_factorization]
78   constructor
79   · intro h
80     ext x
81     have hx := congrArg (fun f : Vu →L[K] Wv => f (Au x)) h
82     simpa using hx
83   · intro h
84     simp [h]
85 
86 theorem residual_norm_bound (U : Vr ≃L[K] Wr)
87     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
88     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
89     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv) :
90     ‖edgeResidual U Au Av Bu Bv A B‖ ≤
91       ‖Bv.toContinuousLinearMap‖ * ‖cycleDefect U Au Av Bu Bv A B‖ *
92         ‖Au.symm.toContinuousLinearMap‖ := by
93   rw [residual_factorization]
94   calc
95     _ ≤ ‖Bv.toContinuousLinearMap‖ *
96         ‖(cycleDefect U Au Av Bu Bv A B).comp Au.symm.toContinuousLinearMap‖ :=
97       ContinuousLinearMap.opNorm_comp_le _ _
98     _ ≤ ‖Bv.toContinuousLinearMap‖ *
99         (‖cycleDefect U Au Av Bu Bv A B‖ * ‖Au.symm.toContinuousLinearMap‖) :=
100       mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _)
101     _ = _ := (mul_assoc _ _ _).symm
102 
103 theorem uniform_bound (U : Vr ≃L[K] Wr)
104     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
105     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
106     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv)
107     (C_B ε C_A : ℝ) (hB : ‖Bv.toContinuousLinearMap‖ ≤ C_B)
108     (hD : ‖cycleDefect U Au Av Bu Bv A B‖ ≤ ε)
109     (hA : ‖Au.symm.toContinuousLinearMap‖ ≤ C_A) :
110     ‖edgeResidual U Au Av Bu Bv A B‖ ≤ C_B * ε * C_A := by
111   apply (residual_norm_bound U Au Av Bu Bv A B).trans
112   have hB0 : 0 ≤ C_B := (norm_nonneg _).trans hB
113   have hD0 : 0 ≤ ε := (norm_nonneg _).trans hD
114   exact mul_le_mul (mul_le_mul hB hD (norm_nonneg _) hB0) hA
115     (norm_nonneg _) (mul_nonneg hB0 hD0)
116 
117 /-- A bound on the actual mixed path factor suffices. This factor is not the
118 condition number of either individual transport. -/
119 theorem product_conditioning_bound (U : Vr ≃L[K] Wr)
120     (Au : Vr ≃L[K] Vu) (Av : Vr ≃L[K] Vv)
121     (Bu : Wr ≃L[K] Wu) (Bv : Wr ≃L[K] Wv)
122     (A : Vu ≃L[K] Vv) (B : Wu ≃L[K] Wv)
123     (C ε : ℝ)
124     (hC : ‖Bv.toContinuousLinearMap‖ * ‖Au.symm.toContinuousLinearMap‖ ≤ C)
125     (hD : ‖cycleDefect U Au Av Bu Bv A B‖ ≤ ε) :
126     ‖edgeResidual U Au Av Bu Bv A B‖ ≤ C * ε := by
127   apply (residual_norm_bound U Au Av Bu Bv A B).trans
128   rw [mul_right_comm]
129   exact mul_le_mul hC hD (norm_nonneg _)
130     ((mul_nonneg (norm_nonneg _) (norm_nonneg _)).trans hC)
131 
132 end PaperXI.ContinuousHolonomyResidual

Back to source controls