ResidualSampling.lean

1 import KomorebiSpace.BanachBlocks
2 import KomorebiSpace.Profiles
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Bounded-gap resampling as a continuous linear cochain map
8 
9 Contractive bonds and a uniform gap bound give a bounded map on all residual
10 families. No converse estimate is asserted. Candidate sampling itself is
11 contractive and does not require a gap bound.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace BanachTower
17 open scoped NNReal ENNReal
18 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
19 variable (X Y : BanachTower.{u,v} 𝕜)
20 variable (hX : ∀ n, ‖X.down n‖ ≤ 1) (hY : ∀ n, ‖Y.down n‖ ≤ 1)
21 variable (φ : ℕ → ℕ) (hφ : Monotone φ)
22 
23 /-- The sampled tower retains the actual composite bonding maps. -/
24 abbrev resample : BanachTower.{u,v} 𝕜 where
25   Obj n := X.Obj (φ n)
26   down n := restriction X (hφ (Nat.le_succ n))
27   bound := 1
28   down_bound n := restriction_contractive X hX (hφ (Nat.le_succ n))
29 
30 @[simp] theorem resample_down (n : ℕ) :
31     (resample X hX φ hφ).down n = restriction X (hφ (Nat.le_succ n)) := rfl
32 
33 def sampleLinear : Candidates X Y →ₗ[𝕜]
34     Candidates (resample X hX φ hφ) (resample Y hY φ hφ) where
35   toFun f := ⟨fun n => f (φ n), memℓp_infty ⟨‖f‖, by
36     rintro _ ⟨n, rfl⟩
37     exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (φ n)⟩⟩
38   map_add' f g := by apply lp.ext; rfl
39   map_smul' c f := by apply lp.ext; rfl
40 
41 theorem sampleLinear_bound (f : Candidates X Y) :
42     ‖sampleLinear X Y hX hY φ hφ f‖ ≤ ‖f‖ := by
43   apply lp.norm_le_of_forall_le (norm_nonneg f)
44   intro n
45   exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (φ n)
46 
47 def sampleCLM : Candidates X Y →L[𝕜]
48     Candidates (resample X hX φ hφ) (resample Y hY φ hφ) :=
49   (sampleLinear X Y hX hY φ hφ).mkContinuous 1
50     (fun f => by simpa using sampleLinear_bound X Y hX hY φ hφ f)
51 
52 @[simp] theorem sampleCLM_apply (f : Candidates X Y) (n : ℕ) :
53     sampleCLM X Y hX hY φ hφ f n = f (φ n) := rfl
54 
55 theorem sampleCLM_bound (f : Candidates X Y) :
56     ‖sampleCLM X Y hX hY φ hφ f‖ ≤ ‖f‖ := sampleLinear_bound X Y hX hY φ hφ f
57 
58 theorem sampleCLM_opNorm : ‖sampleCLM X Y hX hY φ hφ‖ ≤ 1 := by
59   apply ContinuousLinearMap.opNorm_le_bound _ (by norm_num)
60   intro f
61   simpa using sampleCLM_bound X Y hX hY φ hφ f
62 
63 /-- This identity is available even without bounded gaps. -/
64 theorem sampled_differential_coordinate (f : Candidates X Y) (n : ℕ) :
65     differential (resample X hX φ hφ) (resample Y hY φ hφ)
66       (sampleCLM X Y hX hY φ hφ f) n =
67       blockDefect X Y f (hφ (Nat.le_succ n)) := rfl
68 
69 variable (M : ℕ) (hgap : ∀ n, φ (n+1) - φ n ≤ M)
70 
71 def residualSampleLinear : Residuals X Y →ₗ[𝕜]
72     Residuals (resample X hX φ hφ) (resample Y hY φ hφ) where
73   toFun r := ⟨fun n => blockSum X Y r (hφ (Nat.le_succ n)), memℓp_infty ⟨(M : ℝ)*‖r‖, by
74     rintro _ ⟨n, rfl⟩
75     exact (blockSum_uniform_bound X Y hX hY r (hφ (Nat.le_succ n))).trans
76       (mul_le_mul_of_nonneg_right (by exact_mod_cast hgap n) (norm_nonneg r))⟩⟩
77   map_add' r s := by
78     apply lp.ext
79     funext n
80     exact blockSum_add X Y r s (hφ (Nat.le_succ n))
81   map_smul' c r := by
82     apply lp.ext
83     funext n
84     exact blockSum_smul X Y c r (hφ (Nat.le_succ n))
85 
86 theorem residualSampleLinear_bound (r : Residuals X Y) :
87     ‖residualSampleLinear X Y hX hY φ hφ M hgap r‖ ≤ (M : ℝ)*‖r‖ := by
88   apply lp.norm_le_of_forall_le (by positivity)
89   intro n
90   exact (blockSum_uniform_bound X Y hX hY r (hφ (Nat.le_succ n))).trans
91     (mul_le_mul_of_nonneg_right (by exact_mod_cast hgap n) (norm_nonneg r))
92 
93 /-- Actual bounded block-accumulation operator, not a sampled scalar error profile. -/
94 def residualSampleCLM : Residuals X Y →L[𝕜]
95     Residuals (resample X hX φ hφ) (resample Y hY φ hφ) :=
96   (residualSampleLinear X Y hX hY φ hφ M hgap).mkContinuous (M : ℝ)
97     (residualSampleLinear_bound X Y hX hY φ hφ M hgap)
98 
99 @[simp] theorem residualSampleCLM_apply (r : Residuals X Y) (n : ℕ) :
100     residualSampleCLM X Y hX hY φ hφ M hgap r n =
101       blockSum X Y r (hφ (Nat.le_succ n)) := rfl
102 
103 theorem residualSampleCLM_bound (r : Residuals X Y) :
104     ‖residualSampleCLM X Y hX hY φ hφ M hgap r‖ ≤ (M : ℝ)*‖r‖ :=
105   residualSampleLinear_bound X Y hX hY φ hφ M hgap r
106 
107 theorem residualSampleCLM_opNorm :
108     ‖residualSampleCLM X Y hX hY φ hφ M hgap‖ ≤ (M : ℝ) :=
109   ContinuousLinearMap.opNorm_le_bound _ (by positivity)
110     (residualSampleCLM_bound X Y hX hY φ hφ M hgap)
111 
112 /-- The central commuting square, with both operators already constructed. -/
113 theorem resampling_chain (f : Candidates X Y) :
114     differential (resample X hX φ hφ) (resample Y hY φ hφ)
115       (sampleCLM X Y hX hY φ hφ f) =
116       residualSampleCLM X Y hX hY φ hφ M hgap (differential X Y f) := by
117   apply lp.ext
118   funext n
119   exact (blockSum_differential X Y f (hφ (Nat.le_succ n))).symm
120 
121 include hgap in
122 theorem sampled_residual_bound (f : Candidates X Y) :
123     ‖differential (resample X hX φ hφ) (resample Y hY φ hφ)
124       (sampleCLM X Y hX hY φ hφ f)‖ ≤ (M : ℝ)*‖differential X Y f‖ := by
125   rw [resampling_chain X Y hX hY φ hφ M hgap]
126   exact residualSampleCLM_bound X Y hX hY φ hφ M hgap _
127 
128 /-- Exactness is preserved by any monotone common resampling, even with unbounded gaps. -/
129 theorem sample_exact (f : Candidates X Y) (hf : Exact X Y f) :
130     Exact (resample X hX φ hφ) (resample Y hY φ hφ) (sampleCLM X Y hX hY φ hφ f) := by
131   intro n
132   apply ContinuousLinearMap.ext
133   intro x
134   change restriction Y (hφ (Nat.le_succ n)) (f (φ (n+1)) x) =
135     f (φ n) (restriction X (hφ (Nat.le_succ n)) x)
136   rw [restriction_underlying Y, restriction_underlying X]
137   exact Resolution.Adjacent.map_all (fun n => f n)
138     (fun k y => congrArg (fun T : X.Obj (k+1) →L[𝕜] Y.Obj k => T y) (hf k))
139     (hφ (Nat.le_succ n)) x
140 
141 include hgap in
142 /-- Vanishing residual in candidate-sequence norm survives bounded-gap resampling. -/
143 theorem sampled_residual_tendsto_zero (f : ℕ → Candidates X Y)
144     (hf : Filter.Tendsto (fun k => differential X Y (f k)) Filter.atTop (nhds 0)) :
145     Filter.Tendsto (fun k => differential (resample X hX φ hφ) (resample Y hY φ hφ)
146       (sampleCLM X Y hX hY φ hφ (f k))) Filter.atTop (nhds 0) := by
147   have h := (residualSampleCLM X Y hX hY φ hφ M hgap).continuous.tendsto (0 : Residuals X Y)
148   have hc := h.comp hf
149   simpa only [map_zero, Function.comp_def, ← resampling_chain X Y hX hY φ hφ M hgap] using hc
150 
151 end BanachTower
152 end KomorebiSpace
153 end

Back to source controls