SamplingRepair.lean

1 import KomorebiSpace.ResidualSampling
2 import KomorebiSpace.ResidualNaturality
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Quantitative comparison of the two sampling / repair routes
8 
9 This instantiates the cochain comparison with the actual Banach tower
10 resampling maps. Sections of the fine and coarse differential are explicit
11 inputs. Their existence is not claimed for arbitrary contractive towers.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace BanachTower
17 open SplitDefect
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 variable (M : ℕ) (hgap : ∀ n, φ (n+1) - φ n ≤ M)
23 
24 def samplingDefectMap : DefectMap (differential X Y)
25     (differential (resample X hX φ hφ) (resample Y hY φ hφ)) where
26   candidate := sampleCLM X Y hX hY φ hφ
27   residual := residualSampleCLM X Y hX hY φ hφ M hgap
28   commutes := resampling_chain X Y hX hY φ hφ M hgap
29 
30 variable (A : Section (differential X Y))
31 variable (B : Section (differential (resample X hX φ hφ) (resample Y hY φ hφ)))
32 
33 /-- This is exactly the mismatch of the previously constructed sampling maps. -/
34 def samplingMismatch := (samplingDefectMap X Y hX hY φ hφ M hgap).mismatch A B
35 
36 theorem samplingMismatch_exact (r : Residuals X Y) :
37     differential (resample X hX φ hφ) (resample Y hY φ hφ)
38       (samplingMismatch X Y hX hY φ hφ M hgap A B r) = 0 :=
39   (samplingDefectMap X Y hX hY φ hφ M hgap).mismatch_exact A B r
40 
41 theorem sampling_repair_formula (f : Candidates X Y) :
42     B.project (sampleCLM X Y hX hY φ hφ f) -
43       sampleCLM X Y hX hY φ hφ (A.project f) =
44     samplingMismatch X Y hX hY φ hφ M hgap A B (differential X Y f) :=
45   (samplingDefectMap X Y hX hY φ hφ M hgap).repair_change A B f
46 
47 /-- The mismatch vanishes on exact inputs, irrespective of the chosen sections. -/
48 theorem sampling_repairs_agree_on_exact (f : Candidates X Y) (hf : Exact X Y f) :
49     B.project (sampleCLM X Y hX hY φ hφ f) =
50       sampleCLM X Y hX hY φ hφ (A.project f) := by
51   rw [A.project_fixes _ ((exact_iff_differential_zero X Y f).mp hf)]
52   exact B.project_fixes _ ((exact_iff_differential_zero _ _ _).mp
53     (sample_exact X Y hX hY φ hφ f hf))
54 
55 theorem samplingMismatch_opNorm :
56     ‖samplingMismatch X Y hX hY φ hφ M hgap A B‖ ≤ ‖A.lift‖ + (M : ℝ)*‖B.lift‖ := by
57   apply ((samplingDefectMap X Y hX hY φ hφ M hgap).mismatch_opNorm A B).trans
58   change ‖sampleCLM X Y hX hY φ hφ‖ * ‖A.lift‖ +
59     ‖B.lift‖ * ‖residualSampleCLM X Y hX hY φ hφ M hgap‖ ≤ _
60   calc
61     _ ≤ 1 * ‖A.lift‖ + ‖B.lift‖ * (M : ℝ) := add_le_add
62       (mul_le_mul_of_nonneg_right (sampleCLM_opNorm X Y hX hY φ hφ) (norm_nonneg _))
63       (mul_le_mul_of_nonneg_left (residualSampleCLM_opNorm X Y hX hY φ hφ M hgap)
64         (norm_nonneg _))
65     _ = _ := by ring
66 
67 include hgap in
68 theorem sampling_repair_bound (f : Candidates X Y) :
69     ‖B.project (sampleCLM X Y hX hY φ hφ f) -
70       sampleCLM X Y hX hY φ hφ (A.project f)‖ ≤
71         (‖A.lift‖ + (M : ℝ)*‖B.lift‖) * ‖differential X Y f‖ := by
72   rw [sampling_repair_formula X Y hX hY φ hφ M hgap]
73   exact ((samplingMismatch X Y hX hY φ hφ M hgap A B).le_opNorm _).trans
74     (mul_le_mul_of_nonneg_right (samplingMismatch_opNorm X Y hX hY φ hφ M hgap A B)
75       (norm_nonneg _))
76 
77 include hgap in
78 /-- The discrepancy tends to zero, though equality at each finite stage is not automatic. -/
79 theorem sampling_repair_discrepancy_tendsto_zero (f : ℕ → Candidates X Y)
80     (hf : Filter.Tendsto (fun k => differential X Y (f k)) Filter.atTop (nhds 0)) :
81     Filter.Tendsto (fun k => B.project (sampleCLM X Y hX hY φ hφ (f k)) -
82       sampleCLM X Y hX hY φ hφ (A.project (f k))) Filter.atTop (nhds 0) :=
83   (samplingDefectMap X Y hX hY φ hφ M hgap).repair_discrepancy_tendsto_zero A B f hf
84 
85 /-- Exact naturality holds precisely when the sections intertwine the two sampling maps. -/
86 theorem sampling_repair_natural_iff :
87     (∀ f, B.project (sampleCLM X Y hX hY φ hφ f) =
88       sampleCLM X Y hX hY φ hφ (A.project f)) ↔
89       (sampleCLM X Y hX hY φ hφ).comp A.lift =
90         B.lift.comp (residualSampleCLM X Y hX hY φ hφ M hgap) :=
91   (samplingDefectMap X Y hX hY φ hφ M hgap).repair_natural_iff A B
92 
93 end BanachTower
94 end KomorebiSpace
95 end

Back to source controls