OverlapExamples.lean

1 import KomorebiSpace.OverlapViewBridge
2 import Mathlib.Combinatorics.SimpleGraph.Walk.Operations
3 import Mathlib.Tactic.FinCases
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Uniform star control, sharp chain growth, and a nontrivial chart example
9 
10 All graph families are defined for arbitrary finite sizes. No finite numerical
11 check supplies the universal statements or their asymptotic failure boundary.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace OverlapTransport
17 namespace Examples
18 variable {V : Type u} {H : Type v}
19 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
20 
21 def star (o : V) : SimpleGraph V := SimpleGraph.fromRel (fun i _ => i = o)
22 
23 def starPath (o i : V) : (star o).Walk o i := by
24   classical
25   by_cases h : o = i
26   · subst i; exact .nil
27   · exact (show (star o).Adj o i from ⟨h, Or.inl rfl⟩).toWalk
28 
29 @[simp] theorem starPath_anchor (o : V) : starPath o o = .nil := by
30   classical
31   simp [starPath]
32 
33 theorem starPath_length_le_one (o i : V) : (starPath o i).length ≤ 1 := by
34   classical
35   by_cases h : o = i
36   · subst i; simp
37   · simp [starPath, h]
38 
39 def starRouting (o : V) : Routing (star o) o where
40   path := starPath o
41   at_anchor := starPath_anchor o
42 
43 variable [Fintype V]
44 
45 theorem star_radius_le_one (o : V) : (starRouting o).radius ≤ 1 := by
46   apply Finset.sup_le
47   intro i _
48   exact starPath_length_le_one o i
49 
50 /-- The constant is independent of how many vertices the star has. -/
51 theorem star_error (e : Frames (V := V) (H := H)) (o : V) (x : V → H) :
52     ‖x - repair e o x‖ ≤ ‖edgeDifferential e (star o) x‖ := by
53   calc
54     _ ≤ ((starRouting o).radius : ℝ) * ‖edgeDifferential e (star o) x‖ :=
55       (starRouting o).repair_error e x
56     _ ≤ 1 * ‖edgeDifferential e (star o) x‖ :=
57       mul_le_mul_of_nonneg_right (by exact_mod_cast star_radius_le_one o) (norm_nonneg _)
58     _ = _ := one_mul _
59 
60 /-- Actual finite paths with n edges and n+1 views. -/
61 def chain (n : ℕ) : SimpleGraph (Fin (n+1)) where
62   Adj i j := i.val + 1 = j.val ∨ j.val + 1 = i.val
63   symm := ⟨by intro i j h; exact h.symm⟩
64   loopless := ⟨by intro i h; omega⟩
65 
66 def chainWalk (n : ℕ) : (k : ℕ) → (hk : k ≤ n) →
67     (chain n).Walk (⟨0, by omega⟩ : Fin (n+1)) ⟨k, by omega⟩
68   | 0, _ => .nil
69   | k+1, hk => (chainWalk n k (by omega)).append
70       (show (chain n).Adj (⟨k, by omega⟩ : Fin (n+1)) ⟨k+1, by omega⟩ from
71         Or.inl rfl).toWalk
72 
73 theorem chainWalk_length (n : ℕ) : ∀ (k : ℕ) (hk : k ≤ n),
74     (chainWalk n k hk).length = k
75   | 0, _ => rfl
76   | k+1, hk => by
77     simp only [chainWalk, SimpleGraph.Walk.length_append, SimpleGraph.Adj.length_toWalk]
78     rw [chainWalk_length n k]
79 
80 def chainRouting (n : ℕ) : Routing (chain n) (0 : Fin (n+1)) where
81   path i := chainWalk n i.val (by omega)
82   at_anchor := rfl
83 
84 theorem chain_radius (n : ℕ) : (chainRouting n).radius = n := by
85   apply le_antisymm
86   · apply Finset.sup_le
87     intro i _
88     change (chainWalk n i.val _).length ≤ n
89     rw [chainWalk_length]
90     omega
91   · have h := (chainRouting n).length_le_radius (Fin.last n)
92     change (chainWalk n n _).length ≤ (chainRouting n).radius at h
93     rw [chainWalk_length] at h
94     exact h
95 
96 def identityFrames (n : ℕ) : Frames (V := Fin (n+1)) (H := ℝ) :=
97   fun _ => LinearIsometryEquiv.refl ℝ ℝ
98 
99 def ramp (n : ℕ) (i : Fin (n+1)) : ℝ := i.val
100 
101 theorem ramp_repair_zero (n : ℕ) : repair (identityFrames n) 0 (ramp n) = 0 := by
102   funext i
103   simp [repair, transport_apply, identityFrames, ramp]
104 
105 theorem ramp_norm (n : ℕ) : ‖ramp n‖ = (n : ℝ) := by
106   apply le_antisymm
107   · apply (pi_norm_le_iff_of_nonneg (Nat.cast_nonneg n)).mpr
108     intro i
109     change ‖(i.val : ℝ)‖ ≤ (n : ℝ)
110     rw [Real.norm_natCast]
111     exact_mod_cast Nat.le_of_lt_succ i.isLt
112   · have h := norm_le_pi_norm (ramp n) (Fin.last n)
113     simpa [ramp] using h
114 
115 theorem chain_residual_le_one (n : ℕ) :
116     ‖edgeDifferential (identityFrames n) (chain n) (ramp n)‖ ≤ 1 := by
117   apply (pi_norm_le_iff_of_nonneg zero_le_one).mpr
118   intro a
119   change ‖(a.val.2.val : ℝ) - (a.val.1.val : ℝ)‖ ≤ 1
120   rcases a.property with h | h
121   · rw [← h, Nat.cast_add, Nat.cast_one]
122     norm_num
123   · rw [← h, Nat.cast_add, Nat.cast_one]
124     norm_num
125 
126 theorem chain_residual_norm (n : ℕ) (hn : 0 < n) :
127     ‖edgeDifferential (identityFrames n) (chain n) (ramp n)‖ = 1 := by
128   apply le_antisymm (chain_residual_le_one n)
129   let a : Edges (chain n) := ⟨(⟨0, by omega⟩,⟨1,by omega⟩),Or.inl rfl⟩
130   have h := norm_le_pi_norm (edgeDifferential (identityFrames n) (chain n) (ramp n)) a
131   simpa [edgeDifferential_apply, defect, transport_apply, identityFrames, ramp, a] using h
132 
133 theorem chain_error (n : ℕ) :
134     ‖ramp n - repair (identityFrames n) 0 (ramp n)‖ = (n : ℝ) := by
135   rw [ramp_repair_zero, sub_zero, ramp_norm]
136 
137 /-- A derived upper estimate and an input attaining it at every positive chain length. -/
138 theorem chain_bound_sharp (n : ℕ) (hn : 0 < n) :
139     (∀ x : Fin (n+1) → ℝ,
140       ‖x - repair (identityFrames n) 0 x‖ ≤ (n : ℝ) *
141         ‖edgeDifferential (identityFrames n) (chain n) x‖) ∧
142     ‖ramp n - repair (identityFrames n) 0 (ramp n)‖ =
143       (n : ℝ) * ‖edgeDifferential (identityFrames n) (chain n) (ramp n)‖ := by
144   constructor
145   · intro x
146     simpa only [chain_radius] using (chainRouting n).repair_error (identityFrames n) x
147   · rw [chain_error, chain_residual_norm n hn, mul_one]
148 
149 /-- No one finite constant works for every length of this explicit overlap family. -/
150 theorem no_uniform_chain_constant :
151     ¬ ∃ C : ℝ, 0 ≤ C ∧ ∀ n (x : Fin (n+1) → ℝ),
152       ‖x - repair (identityFrames n) 0 x‖ ≤ C *
153         ‖edgeDifferential (identityFrames n) (chain n) x‖ := by
154   rintro ⟨C,hC,hbound⟩
155   obtain ⟨n,hn⟩ := exists_nat_gt C
156   have hb := hbound n (ramp n)
157   rw [chain_error] at hb
158   have he := mul_le_mul_of_nonneg_left (chain_residual_le_one n) hC
159   rw [mul_one] at he
160   exact (not_le_of_gt hn) (hb.trans he)
161 
162 /-- A nonidentity local chart on the real line. -/
163 def reflection : ℝ ≃ₗᵢ[ℝ] ℝ where
164   toFun x := -x
165   invFun x := -x
166   left_inv := neg_neg
167   right_inv := neg_neg
168   map_add' := neg_add
169   map_smul' := by intro c x; simp
170   norm_map' := norm_neg
171 
172 def signedFrames : Frames (V := Bool) (H := ℝ) :=
173   fun b => if b then reflection else LinearIsometryEquiv.refl ℝ ℝ
174 
175 def signedData : Bool → ℝ := fun b => if b then -9 else 7
176 
177 theorem signed_repair_formula :
178     repair signedFrames false signedData false = 7 ∧
179     repair signedFrames false signedData true = -7 := by
180   constructor <;> rfl
181 
182 theorem signed_residual_nonzero :
183     edgeDifferential signedFrames (star false) signedData ≠ 0 := by
184   intro h
185   let a : Edges (star false) := ⟨(false,true), ⟨by decide, Or.inl rfl⟩⟩
186   have he := congrFun h a
187   change -(-9 : ℝ) - 7 = 0 at he
188   norm_num at he
189 
190 end Examples
191 end OverlapTransport
192 end KomorebiSpace
193 end

Back to source controls