CayleyHolonomyConditioning.lean

1 import Mathlib.Analysis.Complex.Basic
2 import Mathlib.Analysis.Normed.Operator.LinearIsometry
3 import Mathlib.Tactic.FieldSimp
4 import Mathlib.Tactic.Ring
5 import Mathlib.Tactic.Linarith
6 import Mathlib.Tactic.Positivity
7 
8 set_option autoImplicit false
9 
10 /-!
11 # A two-real-dimensional family with unbounded holonomy correction gains
12 
13 Multiplication by (t+i)/(t-i) is a real linear isometry of C with no nonzero
14 fixed vector, for every real t. Its exact correction gain is |t-i|/2. Thus
15 finite dimensionality supplies a finite gain for each system, not a common
16 gain for all isometric loop operators. All statements are universal in t.
17 -/
18 noncomputable section
19 namespace KomorebiSpace
20 namespace CayleyHolonomy
21 
22 @[simp] theorem denominator_ne_zero (t : ℝ) : (t : ℂ)-Complex.I ≠ 0 := by
23   intro h
24   have hi := congrArg Complex.im h
25   norm_num at hi
26 
27 @[simp] theorem numerator_ne_zero (t : ℝ) : (t : ℂ)+Complex.I ≠ 0 := by
28   intro h
29   have hi := congrArg Complex.im h
30   norm_num at hi
31 
32 def phase (t : ℝ) : ℂ := ((t : ℂ)+Complex.I)/((t : ℂ)-Complex.I)
33 
34 theorem phase_ne_zero (t : ℝ) : phase t ≠ 0 :=
35   div_ne_zero (numerator_ne_zero t) (denominator_ne_zero t)
36 
37 theorem phase_norm (t : ℝ) : ‖phase t‖ = 1 := by
38   have hc : (t : ℂ)+Complex.I = star ((t : ℂ)-Complex.I) := by
39     apply Complex.ext <;> simp
40   unfold phase
41   rw [norm_div, hc, norm_star, div_self (norm_ne_zero_iff.mpr (denominator_ne_zero t))]
42 
43 theorem phase_ne_one (t : ℝ) : phase t ≠ 1 := by
44   intro h
45   have he : (t : ℂ)+Complex.I = (t : ℂ)-Complex.I :=
46     (div_eq_one_iff_eq (denominator_ne_zero t)).mp h
47   have hi := congrArg Complex.im he
48   norm_num at hi
49 
50 /-- A genuine real linear isometry, not an arbitrary small residual operator. -/
51 def rotation (t : ℝ) : ℂ ≃ₗᵢ[ℝ] ℂ where
52   toFun z := phase t * z
53   invFun z := (phase t)⁻¹ * z
54   left_inv z := by dsimp only; rw [← mul_assoc, inv_mul_cancel₀ (phase_ne_zero t), one_mul]
55   right_inv z := by dsimp only; rw [← mul_assoc, mul_inv_cancel₀ (phase_ne_zero t), one_mul]
56   map_add' z w := mul_add _ _ _
57   map_smul' c z := by
58     change phase t * ((c : ℂ)*z) = (c : ℂ)*(phase t*z)
59     ring
60   norm_map' z := by
61     change ‖phase t * z‖ = ‖z‖
62     rw [norm_mul, phase_norm, one_mul]
63 
64 @[simp] theorem rotation_apply (t : ℝ) (z : ℂ) : rotation t z = phase t * z := rfl
65 
66 theorem fixed_iff_zero (t : ℝ) (z : ℂ) : rotation t z = z ↔ z = 0 := by
67   rw [rotation_apply]
68   constructor
69   · intro h
70     have hp : (phase t-1)*z = 0 := by rw [sub_mul, one_mul, h, sub_self]
71     exact (mul_eq_zero.mp hp).resolve_left (sub_ne_zero.mpr (phase_ne_one t))
72   · intro h; simp [h]
73 
74 theorem phase_sub_one (t : ℝ) :
75     phase t-1 = (2:ℂ)*Complex.I/((t:ℂ)-Complex.I) := by
76   unfold phase
77   field_simp
78   ring
79 
80 theorem phase_displacement_norm (t : ℝ) :
81     ‖phase t-1‖ = 2/‖(t:ℂ)-Complex.I‖ := by
82   rw [phase_sub_one, norm_div, norm_mul]
83   norm_num
84 
85 def sharpGain (t : ℝ) : ℝ := ‖(t:ℂ)-Complex.I‖/2
86 
87 theorem sharpGain_pos (t : ℝ) : 0 < sharpGain t := by
88   unfold sharpGain
89   exact div_pos (norm_pos_iff.mpr (denominator_ne_zero t)) (by norm_num)
90 
91 /-- Equality for all inputs gives the exact, rather than only sufficient, gain. -/
92 theorem sharp_gain_identity (t : ℝ) (z : ℂ) :
93     sharpGain t * ‖rotation t z-z‖ = ‖z‖ := by
94   have hf : rotation t z-z = (phase t-1)*z := by rw [rotation_apply]; ring
95   rw [hf, norm_mul, phase_displacement_norm]
96   unfold sharpGain
97   field_simp [norm_ne_zero_iff.mpr (denominator_ne_zero t)]
98 
99 /-- Any claimed stability bound must be at least the displayed gain. -/
100 theorem necessary_gain (t C : ℝ)
101     (h : ∀ z : ℂ, ‖z‖ ≤ C * ‖rotation t z-z‖) : sharpGain t ≤ C := by
102   have he := sharp_gain_identity t (1:ℂ)
103   have hb := mul_le_mul_of_nonneg_left (h 1) (le_of_lt (sharpGain_pos t))
104   norm_num only [norm_one] at he hb
105   calc
106     sharpGain t = sharpGain t * 1 := by ring
107     _ ≤ sharpGain t * (C * ‖rotation t 1-1‖) := hb
108     _ = C * (sharpGain t * ‖rotation t 1-1‖) := by ring
109     _ = C := by rw [he, mul_one]
110 
111 theorem gain_unbounded (C : ℝ) : ∃ t : ℝ, C < sharpGain t := by
112   let t := 2*|C|+1
113   have ht : 0 ≤ t := by dsimp [t]; positivity
114   have hn := Complex.abs_re_le_norm ((t:ℂ)-Complex.I)
115   have hn' : t ≤ ‖(t:ℂ)-Complex.I‖ := by
116     simpa only [Complex.sub_re, Complex.ofReal_re, Complex.I_re,
117       sub_zero, abs_of_nonneg ht] using hn
118   refine ⟨t, ?_⟩
119   unfold sharpGain
120   have hc := le_abs_self C
121   dsimp [t] at hn' ⊢
122   linarith
123 
124 theorem no_uniform_holonomy_gain :
125     ¬ ∃ C : ℝ, ∀ t : ℝ, ∀ z : ℂ, ‖z‖ ≤ C * ‖rotation t z-z‖ := by
126   rintro ⟨C,hC⟩
127   obtain ⟨t,ht⟩ := gain_unbounded C
128   exact (not_le_of_gt ht) (necessary_gain t C (hC t))
129 
130 end CayleyHolonomy
131 end KomorebiSpace
132 end

Back to source controls