ResidualAliasing.lean

1 import KomorebiSpace.ResidualSampling
2 import Mathlib.Tactic.NormNum
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Residual aliasing and the sharp dependence on block length
8 
9 Even sampling hides a nonzero alternating fine defect in an actual bounded
10 candidate. Separately, the block-accumulation operator has norm exactly M on
11 identity real towers sampled every M stages. These are all-level Lean proofs.
12 -/
13 noncomputable section
14 namespace KomorebiSpace
15 namespace ResidualAliasing
16 open BanachTower
17 open scoped NNReal ENNReal
18 
19 abbrev scalar : BanachTower ℝ where
20   Obj _ := ℝ
21   down _ := ContinuousLinearMap.id ℝ ℝ
22   bound := 1
23   down_bound _ := ContinuousLinearMap.norm_id_le
24 
25 theorem scalar_contractive (n : ℕ) : ‖scalar.down n‖ ≤ 1 :=
26   ContinuousLinearMap.norm_id_le
27 
28 @[simp] theorem scalar_restriction {i j : ℕ} (h : i ≤ j) :
29     restriction scalar h = ContinuousLinearMap.id ℝ ℝ := by
30   induction j, h using Nat.le_induction with
31   | base => simp
32   | succ j hj ih =>
33     rw [restriction_succ scalar hj, ih]
34     apply ContinuousLinearMap.ext
35     intro x
36     rfl
37 
38 def stride (m n : ℕ) : ℕ := m*n
39 
40 theorem stride_monotone (m : ℕ) : Monotone (stride m) :=
41   fun _ _ h => Nat.mul_le_mul_left m h
42 
43 @[simp] theorem stride_gap (m n : ℕ) : stride m (n+1) - stride m n = m := by
44   simp [stride, Nat.mul_add]
45 
46 theorem stride_cofinal (m : ℕ) (hm : 0 < m) : Resolution.UnboundedSchedule (stride m) := by
47   intro n
48   refine ⟨n, ?_⟩
49   change n ≤ m*n
50   nlinarith
51 
52 abbrev sampled (m : ℕ) := resample scalar scalar_contractive (stride m) (stride_monotone m)
53 
54 abbrev sample (m : ℕ) := sampleCLM scalar scalar scalar_contractive scalar_contractive
55   (stride m) (stride_monotone m)
56 
57 abbrev coarsen (m : ℕ) := residualSampleCLM scalar scalar scalar_contractive scalar_contractive
58   (stride m) (stride_monotone m) m (fun n => (stride_gap m n).le)
59 
60 @[simp] theorem sampled_down (m n : ℕ) :
61     (sampled m).down n = ContinuousLinearMap.id ℝ ℝ := scalar_restriction _
62 
63 /-- The candidate alternates between the identity and twice the identity. -/
64 def level (n : ℕ) : ℝ →L[ℝ] ℝ :=
65   (1 + Profiles.alternating n) • ContinuousLinearMap.id ℝ ℝ
66 
67 theorem level_bound (n : ℕ) : ‖level n‖ ≤ 2 := by
68   unfold level Profiles.alternating
69   split_ifs <;> norm_num [norm_smul, ContinuousLinearMap.norm_id]
70 
71 def candidate : Candidates scalar scalar :=
72   ⟨level, memℓp_infty ⟨2, by rintro _ ⟨n, rfl⟩; exact level_bound n⟩⟩
73 
74 @[simp] theorem candidate_even (n : ℕ) : candidate (2*n) = ContinuousLinearMap.id ℝ ℝ := by
75   change level (2*n) = _
76   simp [level]
77 
78 @[simp] theorem candidate_odd (n : ℕ) : candidate (2*n+1) = (2 : ℝ) • ContinuousLinearMap.id ℝ ℝ := by
79   change level (2*n+1) = _
80   norm_num [level]
81 
82 @[simp] theorem fine_defect_even (n : ℕ) :
83     differential scalar scalar candidate (2*n) = ContinuousLinearMap.id ℝ ℝ := by
84   rw [differential_apply, candidate_even, candidate_odd]
85   apply ContinuousLinearMap.ext
86   intro x
87   change 2*x-x=x
88   ring
89 
90 @[simp] theorem fine_defect_odd (n : ℕ) :
91     differential scalar scalar candidate (2*n+1) = -ContinuousLinearMap.id ℝ ℝ := by
92   rw [differential_apply, show 2*n+1+1=2*(n+1) by omega, candidate_even, candidate_odd]
93   apply ContinuousLinearMap.ext
94   intro x
95   change x-2*x = -x
96   ring
97 
98 theorem fine_residual_norm : ‖differential scalar scalar candidate‖ = 1 := by
99   apply le_antisymm
100   · apply lp.norm_le_of_forall_le (by norm_num)
101     intro n
102     have hn : n = 2*(n/2) ∨ n = 2*(n/2)+1 := by omega
103     rcases hn with h | h
104     · rw [h, fine_defect_even]
105       exact ContinuousLinearMap.norm_id_le
106     · rw [h, fine_defect_odd, norm_neg]
107       exact ContinuousLinearMap.norm_id_le
108   · have h := lp.norm_apply_le_norm ENNReal.top_ne_zero (differential scalar scalar candidate) (2*0)
109     rw [fine_defect_even, ContinuousLinearMap.norm_id] at h
110     exact h
111 
112 @[simp] theorem sampled_candidate (n : ℕ) :
113     sample 2 candidate n = ContinuousLinearMap.id ℝ ℝ := candidate_even n
114 
115 theorem sampled_candidate_exact : Exact (sampled 2) (sampled 2) (sample 2 candidate) := by
116   intro n
117   simp [stride]
118 
119 theorem sampled_residual_zero :
120     differential (sampled 2) (sampled 2) (sample 2 candidate) = 0 :=
121   (exact_iff_differential_zero _ _ _).mp sampled_candidate_exact
122 
123 theorem candidate_not_exact : ¬ Exact scalar scalar candidate := by
124   intro h
125   have hz := (exact_iff_differential_zero _ _ _).mp h
126   have hn := fine_residual_norm
127   rw [hz, norm_zero] at hn
128   norm_num at hn
129 
130 /-- A coarse exact candidate with nonzero seed hides fine incompatibility. -/
131 theorem coarsening_hides_nonzero_residual :
132     ¬ Exact scalar scalar candidate ∧
133     Exact (sampled 2) (sampled 2) (sample 2 candidate) ∧
134     sample 2 candidate 0 1 = 1 :=
135   ⟨candidate_not_exact, sampled_candidate_exact, by rw [sampled_candidate]; rfl⟩
136 
137 theorem coarsen_not_injective : ¬ Function.Injective (coarsen 2) := by
138   intro hi
139   have hc : coarsen 2 (differential scalar scalar candidate) = coarsen 2 0 := by
140     rw [map_zero]
141     exact (resampling_chain scalar scalar scalar_contractive scalar_contractive
142       (stride 2) (stride_monotone 2) 2 (fun n => (stride_gap 2 n).le) candidate).symm.trans
143       sampled_residual_zero
144   have hz := hi hc
145   have hn := fine_residual_norm
146   rw [hz, norm_zero] at hn
147   norm_num at hn
148 
149 /-- No positive lower comparison bound is possible, even on residuals of actual candidates. -/
150 theorem no_positive_reverse_bound (c : ℝ) (hc : 0 < c) :
151     ¬ (∀ f : Candidates scalar scalar, c*‖differential scalar scalar f‖ ≤
152       ‖differential (sampled 2) (sampled 2) (sample 2 f)‖) := by
153   intro h
154   have he := h candidate
155   rw [fine_residual_norm, sampled_residual_zero, norm_zero, mul_one] at he
156   exact (not_le_of_gt hc) he
157 
158 /-- Test input for the norm of the block map; it is not claimed to be a fine defect. -/
159 def unitResidual : Residuals scalar scalar :=
160   ⟨fun _ => ContinuousLinearMap.id ℝ ℝ, memℓp_infty ⟨1, by
161     rintro _ ⟨n, rfl⟩
162     exact ContinuousLinearMap.norm_id_le⟩⟩
163 
164 theorem unitResidual_norm : ‖unitResidual‖ = 1 := by
165   apply le_antisymm
166   · apply lp.norm_le_of_forall_le (by norm_num)
167     intro n
168     exact ContinuousLinearMap.norm_id_le
169   · have h := lp.norm_apply_le_norm ENNReal.top_ne_zero unitResidual 0
170     change ‖ContinuousLinearMap.id ℝ ℝ‖ ≤ ‖unitResidual‖ at h
171     simpa using h
172 
173 theorem blockSum_unit {i j : ℕ} (h : i ≤ j) :
174     blockSum scalar scalar unitResidual h = ((j-i : ℕ) : ℝ) • ContinuousLinearMap.id ℝ ℝ := by
175   induction j, h using Nat.le_induction with
176   | base => simp
177   | succ j hj ih =>
178     rw [blockSum_succ scalar scalar unitResidual hj, scalar_restriction, ih]
179     have hs : j+1-i = (j-i)+1 := by omega
180     rw [hs, Nat.cast_add, Nat.cast_one]
181     apply ContinuousLinearMap.ext
182     intro x
183     change x + (↑(j-i) * x) = (↑(j-i)+1)*x
184     ring
185 
186 @[simp] theorem coarsen_unit_coordinate (m n : ℕ) :
187     coarsen m unitResidual n = (m : ℝ) • ContinuousLinearMap.id ℝ ℝ := by
188   change blockSum scalar scalar unitResidual (stride_monotone m (Nat.le_succ n)) = _
189   rw [blockSum_unit, stride_gap]
190 
191 theorem coarsen_unit_norm (m : ℕ) : ‖coarsen m unitResidual‖ = (m : ℝ) := by
192   apply le_antisymm
193   · have h := residualSampleCLM_bound scalar scalar scalar_contractive scalar_contractive
194       (stride m) (stride_monotone m) m (fun n => (stride_gap m n).le) unitResidual
195     simpa [unitResidual_norm] using h
196   · have h := lp.norm_apply_le_norm ENNReal.top_ne_zero (coarsen m unitResidual) 0
197     rw [coarsen_unit_coordinate] at h
198     simpa [norm_smul, ContinuousLinearMap.norm_id, Real.norm_of_nonneg (Nat.cast_nonneg m)] using h
199 
200 /-- The M factor is sharp for maps on all residual families. -/
201 theorem coarsen_opNorm (m : ℕ) : ‖coarsen m‖ = (m : ℝ) := by
202   apply le_antisymm
203   · exact residualSampleCLM_opNorm scalar scalar scalar_contractive scalar_contractive
204       (stride m) (stride_monotone m) m (fun n => (stride_gap m n).le)
205   · have h := (coarsen m).le_opNorm unitResidual
206     simpa [unitResidual_norm, coarsen_unit_norm] using h
207 
208 end ResidualAliasing
209 end KomorebiSpace
210 end

Back to source controls