HolonomyConditioningExample.lean

1 import KomorebiSpace.HolonomyProjection
2 import KomorebiSpace.CayleyHolonomyConditioning
3 import Mathlib.Analysis.InnerProductSpace.Basic
4 import Mathlib.Tactic.FinCases
5 
6 set_option autoImplicit false
7 
8 /-!
9 # The nonuniform gain family on an actual fixed three-view graph
10 
11 All connections are inverse-consistent real linear isometries of C. Only one
12 edge carries the varying Cayley rotation. The graph and real fiber dimension
13 stay fixed. Thus no graph-size or dimension growth explains the diverging
14 correction gain.
15 -/
16 noncomputable section
17 namespace KomorebiSpace
18 namespace HolonomyTransport
19 namespace ConditioningTriangle
20 
21 abbrev graph : SimpleGraph (Fin 3) := ⊤
22 
23 def edgeTransport (t : ℝ) (i j : Fin 3) : ℂ ≃ₗᵢ[ℝ] ℂ :=
24   if i=0 ∧ j=2 then CayleyHolonomy.rotation t
25   else if i=2 ∧ j=0 then (CayleyHolonomy.rotation t).symm
26   else LinearIsometryEquiv.refl ℝ ℂ
27 
28 def connection (t : ℝ) : Connection (Fin 3) ℂ where
29   transport := edgeTransport t
30   self_apply := by intro i z; fin_cases i <;> rfl
31   reverse_apply := by
32     intro i j z
33     fin_cases i <;> fin_cases j
34     all_goals first
35       | rfl
36       | exact (CayleyHolonomy.rotation t).symm_apply_apply z
37       | exact (CayleyHolonomy.rotation t).apply_symm_apply z
38 
39 def routing : OverlapTransport.Routing graph (0 : Fin 3) where
40   path i := by
41     by_cases h : (0 : Fin 3)=i
42     · subst i; exact .nil
43     · exact (show graph.Adj 0 i from h).toWalk
44   at_anchor := rfl
45 
46 theorem parallel_iff_zero (t : ℝ) (x : Fin 3 → ℂ) :
47     (connection t).Parallel graph x ↔ x=0 := by
48   constructor
49   · intro hx
50     have h10 : x 1=x 0 := hx 0 1 (by decide)
51     have h21 : x 2=x 1 := hx 1 2 (by decide)
52     have hr : CayleyHolonomy.rotation t (x 2)=x 0 := hx 0 2 (by decide)
53     rw [h21,h10] at hr
54     have hz := (CayleyHolonomy.fixed_iff_zero t (x 0)).mp hr
55     funext i
56     fin_cases i
57     · exact hz
58     · exact h10.trans hz
59     · exact h21.trans (h10.trans hz)
60   · intro hx
61     subst x
62     intro i j _hij
63     exact map_zero _
64 
65 theorem fixed_iff_zero (t : ℝ) (z : ℂ) :
66     z ∈ Rooted.fixedSpace (connection t) routing ↔ z=0 := by
67   rw [← Rooted.anchor_extendable_iff]
68   constructor
69   · rintro ⟨x,hx,ho⟩
70     have hz := (parallel_iff_zero t x).mp hx
71     rw [hz] at ho
72     exact ho.symm
73   · intro hz
74     subst z
75     exact ⟨0,(parallel_iff_zero t 0).mpr rfl,rfl⟩
76 
77 theorem orthogonalRepair_zero (t : ℝ) (x : Fin 3 → ℂ) :
78     Rooted.orthogonalRepair (connection t) routing x=0 :=
79   (parallel_iff_zero t _).mp (Rooted.orthogonalRepair_parallel (connection t) routing x)
80 
81 theorem inverse_displacement_norm (t : ℝ) (z : ℂ) :
82     ‖(CayleyHolonomy.rotation t).symm z-z‖ = ‖CayleyHolonomy.rotation t z-z‖ := by
83   rw [← (CayleyHolonomy.rotation t).norm_map, map_sub,
84     LinearIsometryEquiv.apply_symm_apply, norm_sub_rev]
85 
86 theorem constant_residual_norm (t : ℝ) (z : ℂ) :
87     ‖(connection t).differential graph (fun _ => z)‖ = ‖CayleyHolonomy.rotation t z-z‖ := by
88   apply le_antisymm
89   · apply (pi_norm_le_iff_of_nonneg (norm_nonneg _)).mpr
90     intro a
91     change ‖edgeTransport t a.val.1 a.val.2 z-z‖ ≤ _
92     unfold edgeTransport
93     split
94     · exact le_rfl
95     · split
96       · exact le_of_eq (inverse_displacement_norm t z)
97       · change ‖z-z‖ ≤ _
98         rw [sub_self,norm_zero]
99         exact norm_nonneg (CayleyHolonomy.rotation t z-z)
100   · have hb := norm_le_pi_norm ((connection t).differential graph (fun _ => z))
101         (⟨(0,2),by decide⟩ : OverlapTransport.Edges graph)
102     exact hb
103 
104 /-- Every global repair gain on this fixed graph must be at least |t-i|/2. -/
105 theorem necessary_global_gain (t C : ℝ)
106     (hb : ∀ x : Fin 3 → ℂ,
107       ‖x-Rooted.orthogonalRepair (connection t) routing x‖ ≤
108         C * ‖(connection t).differential graph x‖) : CayleyHolonomy.sharpGain t ≤ C := by
109   apply CayleyHolonomy.necessary_gain t C
110   intro z
111   have hx := hb (fun _ => z)
112   rw [orthogonalRepair_zero, sub_zero, constant_residual_norm] at hx
113   simpa only [pi_norm_const] using hx
114 
115 /-- Failure of a universal constant already occurs with three vertices and real dimension two. -/
116 theorem no_uniform_global_gain :
117     ¬ ∃ C : ℝ, ∀ t : ℝ, ∀ x : Fin 3 → ℂ,
118       ‖x-Rooted.orthogonalRepair (connection t) routing x‖ ≤
119         C * ‖(connection t).differential graph x‖ := by
120   rintro ⟨C,hC⟩
121   obtain ⟨t,ht⟩ := CayleyHolonomy.gain_unbounded C
122   exact (not_le_of_gt ht) (necessary_global_gain t C (hC t))
123 
124 end ConditioningTriangle
125 end HolonomyTransport
126 end KomorebiSpace
127 end

Back to source controls