ResidualProfiles.lean

1 import KomorebiSpace.ResidualSampling
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Levelwise residual decay under cofinal bounded-gap resampling
7 
8 The hypothesis concerns norms of adjacent operators at growing resolution,
9 not a sequence of entire candidates converging in the sup norm. The conclusion
10 is one-way: cancellation prevents a converse in general.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace
15 namespace BanachTower
16 open Filter
17 open scoped Topology
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 include hX hY
22 
23 /-- A block whose component residual norms are bounded by e has budget length * e. -/
24 theorem blockSum_local_bound (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n)
25     {i j : ℕ} (h : i ≤ j) (e : ℝ) (he : ∀ k, i ≤ k → k < j → ‖r k‖ ≤ e) :
26     ‖blockSum X Y r h‖ ≤ (j-i : ℕ)*e := by
27   apply (blockSum_norm X Y hX hY r h).trans
28   calc
29     (∑ k ∈ Finset.Ico i j, ‖r k‖) ≤ ∑ _k ∈ Finset.Ico i j, e := by
30       apply Finset.sum_le_sum
31       intro k hk
32       exact he k (Finset.mem_Ico.mp hk).1 (Finset.mem_Ico.mp hk).2
33     _ = (j-i : ℕ)*e := by simp
34 
35 /-- Cofinal bounded-gap sampling preserves levelwise decay of actual operator residuals. -/
36 theorem blockSum_cofinal_vanish (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n)
37     (hr : Tendsto (fun n => ‖r n‖) atTop (𝓝 0))
38     (φ : ℕ → ℕ) (hφ : Monotone φ) (hc : Resolution.UnboundedSchedule φ)
39     (M : ℕ) (hgap : ∀ n, φ (n+1)-φ n ≤ M) :
40     Tendsto (fun n => ‖blockSum X Y r (hφ (Nat.le_succ n))‖) atTop (𝓝 0) := by
41   apply Metric.tendsto_atTop.2
42   intro ε hε
43   have hden : 0 < (M : ℝ)+1 := by positivity
44   have he : 0 < ε/((M : ℝ)+1) := div_pos hε hden
45   have ht : ∀ᶠ k in atTop, ‖r k‖ < ε/((M : ℝ)+1) :=
46     (tendsto_order.1 hr).2 _ he
47   obtain ⟨N, hN⟩ := eventually_atTop.1 ht
48   obtain ⟨K, hK⟩ := hc N
49   refine ⟨K, ?_⟩
50   intro n hn
51   have hφN : N ≤ φ n := hK.trans (hφ hn)
52   have hb := blockSum_local_bound X Y hX hY r (hφ (Nat.le_succ n))
53     (ε/((M : ℝ)+1)) (fun k hk _ => (hN k (hφN.trans hk)).le)
54   have hle : ‖blockSum X Y r (hφ (Nat.le_succ n))‖ ≤
55       (M : ℝ)*(ε/((M : ℝ)+1)) :=
56     hb.trans (mul_le_mul_of_nonneg_right (by exact_mod_cast hgap n) he.le)
57   have heq : ε/((M : ℝ)+1)*((M : ℝ)+1)=ε := div_mul_cancel₀ ε (ne_of_gt hden)
58   have hlt : ‖blockSum X Y r (hφ (Nat.le_succ n))‖ < ε := by nlinarith
59   simpa only [Real.dist_eq, sub_zero, abs_of_nonneg (norm_nonneg _)] using hlt
60 
61 /-- Specialization to a single bounded candidate with asymptotically vanishing fine defects. -/
62 theorem sampled_levelwise_residual_vanish (f : Candidates X Y)
63     (hf : Tendsto (fun n => ‖differential X Y f n‖) atTop (𝓝 0))
64     (φ : ℕ → ℕ) (hφ : Monotone φ) (hc : Resolution.UnboundedSchedule φ)
65     (M : ℕ) (hgap : ∀ n, φ (n+1)-φ n ≤ M) :
66     Tendsto (fun n => ‖differential (resample X hX φ hφ) (resample Y hY φ hφ)
67       (sampleCLM X Y hX hY φ hφ f) n‖) atTop (𝓝 0) := by
68   have h := blockSum_cofinal_vanish X Y hX hY (differential X Y f) hf φ hφ hc M hgap
69   simpa only [blockSum_differential, sampled_differential_coordinate] using h
70 
71 end BanachTower
72 end KomorebiSpace
73 end

Back to source controls