AmplifiedExamples.lean

1 import KomorebiSpace.AmplifiedViews
2 import KomorebiSpace.OverlapExamples
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Nonisometric chains with exact exponential amplification
8 
9 The graph has n edges. Each forward bond contracts by 1/2 and each reverse
10 bond expands by 2. The nonzero anchor 7 is protected. A candidate has directed
11 edge residual norm 1 but exact anchored repair error 2^n-1.
12 -/
13 noncomputable section
14 namespace KomorebiSpace
15 namespace AmplifiedTransport
16 namespace Examples
17 
18 /-- A real scalar continuous linear equivalence, with inverse explicitly given. -/
19 def scale (a : ℝ) (ha : a ≠ 0) : ℝ ≃L[ℝ] ℝ :=
20   (show ℝ ≃ₗ[ℝ] ℝ from
21     { toFun := fun x => a*x
22       invFun := fun x => a⁻¹*x
23       left_inv := by intro x; change a⁻¹*(a*x)=x; rw [← mul_assoc, inv_mul_cancel₀ ha, one_mul]
24       right_inv := by intro x; change a*(a⁻¹*x)=x; rw [← mul_assoc, mul_inv_cancel₀ ha, one_mul]
25       map_add' := mul_add a
26       map_smul' := by intro c x; change a*(c*x)=c*(a*x); ring }).toContinuousLinearEquiv
27 
28 @[simp] theorem scale_apply (a : ℝ) (ha : a ≠ 0) (x : ℝ) : scale a ha x = a*x := rfl
29 
30 @[simp] theorem scale_symm_apply (a : ℝ) (ha : a ≠ 0) (x : ℝ) :
31     (scale a ha).symm x = a⁻¹*x := rfl
32 
33 def chainFrames (n : ℕ) (i : Fin (n+1)) : ℝ ≃L[ℝ] ℝ :=
34   scale ((2 : ℝ)^i.val) (pow_ne_zero _ (by norm_num))
35 
36 def chainConnection (n : ℕ) : Connection (Fin (n+1)) ℝ :=
37   Connection.ofFrames (chainFrames n)
38 
39 @[simp] theorem chain_transport (n : ℕ) (i j : Fin (n+1)) (z : ℝ) :
40     (chainConnection n).transport i j z =
41       (2 : ℝ)^i.val * (((2 : ℝ)^j.val)⁻¹*z) := rfl
42 
43 theorem chain_transport_forward (n : ℕ) (i j : Fin (n+1))
44     (h : i.val+1=j.val) (z : ℝ) : (chainConnection n).transport i j z = z/2 := by
45   rw [chain_transport, ← h, pow_succ]
46   have hn : (2 : ℝ)^i.val ≠ 0 := pow_ne_zero _ (by norm_num)
47   field_simp
48 
49 theorem chain_transport_backward (n : ℕ) (i j : Fin (n+1))
50     (h : i.val+1=j.val) (z : ℝ) : (chainConnection n).transport j i z = 2*z := by
51   rw [chain_transport, ← h, pow_succ]
52   have hn : (2 : ℝ)^i.val ≠ 0 := pow_ne_zero _ (by norm_num)
53   field_simp
54 
55 def chainRepair (n : ℕ) (x : Fin (n+1) → ℝ) (i : Fin (n+1)) : ℝ :=
56   (2 : ℝ)^i.val * x 0
57 
58 @[simp] theorem chainRepair_anchor (n : ℕ) (x : Fin (n+1) → ℝ) :
59     chainRepair n x 0 = x 0 := by simp [chainRepair]
60 
61 theorem chainRepair_parallel (n : ℕ) (x : Fin (n+1) → ℝ) :
62     (chainConnection n).Parallel (OverlapTransport.Examples.chain n) (chainRepair n x) := by
63   intro i j _
64   rw [chain_transport]
65   unfold chainRepair
66   have hj : (2 : ℝ)^j.val ≠ 0 := pow_ne_zero _ (by norm_num)
67   field_simp
68 
69 /-- Equality with the general holonomy-based projector, not a second repair definition. -/
70 theorem chainRepair_is_constructed (n : ℕ) (x : Fin (n+1) → ℝ) :
71     Rooted.orthogonalRepair (chainConnection n) (OverlapTransport.Examples.chainRouting n) x =
72       chainRepair n x := by
73   apply Rooted.parallel_unique (chainConnection n) (OverlapTransport.Examples.chainRouting n)
74     (Rooted.orthogonalRepair_parallel _ _ x) (chainRepair_parallel n x)
75   rw [Rooted.orthogonalRepair_anchor, chainRepair_anchor]
76   apply Rooted.anchorProjection_fixes
77   have he := Rooted.parallel_anchor_fixed (chainConnection n)
78     (OverlapTransport.Examples.chainRouting n) (chainRepair n x) (chainRepair_parallel n x)
79   simpa only [chainRepair_anchor] using he
80 
81 def candidate (n : ℕ) (i : Fin (n+1)) : ℝ := 8*(2 : ℝ)^i.val-1
82 
83 @[simp] theorem candidate_anchor (n : ℕ) : candidate n 0 = 7 := by norm_num [candidate]
84 
85 theorem candidate_forward_defect (n : ℕ) (i j : Fin (n+1)) (h : i.val+1=j.val) :
86     (chainConnection n).defect (candidate n) i j = 1/2 := by
87   rw [Connection.defect, chain_transport_forward n i j h]
88   simp only [candidate, ← h, pow_succ]
89   ring
90 
91 theorem candidate_backward_defect (n : ℕ) (i j : Fin (n+1)) (h : i.val+1=j.val) :
92     (chainConnection n).defect (candidate n) j i = -1 := by
93   rw [Connection.defect, chain_transport_backward n i j h]
94   simp only [candidate, ← h, pow_succ]
95   ring
96 
97 theorem candidate_residual_le_one (n : ℕ) :
98     ‖(chainConnection n).differential (OverlapTransport.Examples.chain n) (candidate n)‖ ≤ 1 := by
99   apply (pi_norm_le_iff_of_nonneg zero_le_one).mpr
100   intro a
101   rw [Connection.differential_apply]
102   rcases a.property with h | h
103   · rw [candidate_forward_defect n _ _ h]; norm_num
104   · rw [candidate_backward_defect n _ _ h]; norm_num
105 
106 theorem candidate_residual_norm (n : ℕ) (hn : 0 < n) :
107     ‖(chainConnection n).differential (OverlapTransport.Examples.chain n) (candidate n)‖ = 1 := by
108   apply le_antisymm (candidate_residual_le_one n)
109   let a : OverlapTransport.Edges (OverlapTransport.Examples.chain n) :=
110     ⟨(⟨1,by omega⟩,⟨0,by omega⟩),Or.inr rfl⟩
111   have he := norm_le_pi_norm
112     ((chainConnection n).differential (OverlapTransport.Examples.chain n) (candidate n)) a
113   change ‖(chainConnection n).defect (candidate n) ⟨1,by omega⟩ ⟨0,by omega⟩‖ ≤ _ at he
114   rw [candidate_backward_defect n _ _ rfl] at he
115   simpa using he
116 
117 theorem candidate_error_coordinate (n : ℕ) (i : Fin (n+1)) :
118     (candidate n-chainRepair n (candidate n)) i = (2 : ℝ)^i.val-1 := by
119   change (8*(2 : ℝ)^i.val-1) - (2 : ℝ)^i.val * candidate n 0 = _
120   rw [candidate_anchor]
121   ring
122 
123 theorem candidate_error_norm (n : ℕ) :
124     ‖candidate n-chainRepair n (candidate n)‖ = (2 : ℝ)^n-1 := by
125   have hp : ∀ k : ℕ, 1 ≤ (2 : ℝ)^k := fun k => one_le_pow₀ (by norm_num)
126   apply le_antisymm
127   · apply (pi_norm_le_iff_of_nonneg (sub_nonneg.mpr (hp n))).mpr
128     intro i
129     rw [candidate_error_coordinate, Real.norm_eq_abs, abs_of_nonneg (sub_nonneg.mpr (hp i.val))]
130     apply sub_le_sub_right
131     exact pow_le_pow_right₀ (by norm_num) (Nat.le_of_lt_succ i.isLt)
132   · have h := norm_le_pi_norm (candidate n-chainRepair n (candidate n)) (Fin.last n)
133     rw [candidate_error_coordinate] at h
134     change ‖(2 : ℝ)^n-1‖ ≤ _ at h
135     rw [Real.norm_eq_abs, abs_of_nonneg (sub_nonneg.mpr (hp n))] at h
136     exact h
137 
138 /-- Actual all-depth candidate and general-repair discrepancy. -/
139 theorem exponential_amplification (n : ℕ) (hn : 0 < n) :
140     candidate n 0 = 7 ∧
141     ‖(chainConnection n).differential (OverlapTransport.Examples.chain n) (candidate n)‖ = 1 ∧
142     ‖candidate n-Rooted.orthogonalRepair (chainConnection n)
143       (OverlapTransport.Examples.chainRouting n) (candidate n)‖ = (2 : ℝ)^n-1 := by
144   rw [chainRepair_is_constructed]
145   exact ⟨candidate_anchor n,candidate_residual_norm n hn,candidate_error_norm n⟩
146 
147 /-- The old route-length-only bound fails on a three-edge nonisometric chain. -/
148 theorem length_only_bound_false :
149     ¬ ‖candidate 3-Rooted.orthogonalRepair (chainConnection 3)
150       (OverlapTransport.Examples.chainRouting 3) (candidate 3)‖ ≤
151       (3 : ℝ)*‖(chainConnection 3).differential (OverlapTransport.Examples.chain 3) (candidate 3)‖ := by
152   rw [chainRepair_is_constructed, candidate_error_norm, candidate_residual_norm 3 (by norm_num)]
153   norm_num
154 
155 /-- A fixed anchor can be amplified: global nonexpansiveness no longer follows. -/
156 theorem repair_not_nonexpansive :
157     ¬ ∀ x : Fin 2 → ℝ,
158       ‖Rooted.orthogonalRepair (chainConnection 1)
159         (OverlapTransport.Examples.chainRouting 1) x‖ ≤ ‖x‖ := by
160   intro h
161   have hb := h (fun _ => 7)
162   rw [chainRepair_is_constructed] at hb
163   have hl := norm_le_pi_norm (chainRepair 1 (fun _ => (7 : ℝ))) (1 : Fin 2)
164   have hx : ‖(fun _ : Fin 2 => (7 : ℝ))‖ = 7 := by simp
165   rw [hx] at hb
166   norm_num [chainRepair] at hl
167   linarith
168 
169 end Examples
170 end AmplifiedTransport
171 end KomorebiSpace
172 end

Back to source controls