CascadeDensity.lean

1 import KomorebiSpace.CascadeLimits
2 
3 set_option autoImplicit false
4 
5 /-!
6 # A checkable density criterion for infinite reconstruction
7 
8 Under a uniform remainder bound, recoverable data are exactly the norm closure
9 of data killed at some finite coarse level. This is a criterion, not a blanket
10 density assertion. Uniform boundedness is not inferred from split surjectivity.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace
15 namespace CoarseningCascade
16 open Filter Set
17 open scoped Topology
18 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
19 variable (T : CoarseningCascade.{u,v} 𝕜)
20 
21 /-- Data whose retained hierarchy terminates at a finite level. -/
22 def finiteCore : Set (T.Obj 0) := {x | ∃ N, T.remainder N x = 0}
23 
24 @[simp] theorem mem_finiteCore (x : T.Obj 0) :
25     x ∈ T.finiteCore ↔ ∃ N, T.remainder N x = 0 := Iff.rfl
26 
27 /-- A remainder that is zero stays zero under further coarsening. -/
28 theorem remainder_zero_after (x : T.Obj 0) (N : ℕ) (hN : T.remainder N x = 0)
29     (n : ℕ) (hn : N ≤ n) : T.remainder n x = 0 := by
30   rw [← T.remainder_nested_right N n hn x, hN, map_zero]
31 
32 theorem finiteCore_recoverable (x : T.Obj 0) (hx : x ∈ T.finiteCore) :
33     x ∈ T.recoverable := by
34   obtain ⟨N, hN⟩ := hx
35   apply tendsto_const_nhds.congr'
36   filter_upwards [eventually_ge_atTop N] with n hn
37   exact (T.remainder_zero_after x N hN n hn).symm
38 
39 /-- The finite reconstructed approximants always lie in the finite core. -/
40 theorem partial_mem_finiteCore (x : T.Obj 0) (N : ℕ) :
41     T.reconstructed N x ∈ T.finiteCore := ⟨N, T.remainder_partial x N⟩
42 
43 /-- Recovery forces approximation by data killed at a finite level. -/
44 theorem recoverable_mem_closure_finiteCore (x : T.Obj 0) (hx : x ∈ T.recoverable) :
45     x ∈ closure T.finiteCore := by
46   have ht := (T.partial_tendsto_iff x).2 hx
47   exact isClosed_closure.mem_of_tendsto ht
48     (Filter.Eventually.of_forall (fun N => subset_closure (T.partial_mem_finiteCore x N)))
49 
50 /-- A uniform operator bound promotes finite-core approximation to recovery. -/
51 theorem recoverable_of_mem_closure (K : ℝ) (hK : 0 ≤ K)
52     (hQ : ∀ N, ‖T.remainder N‖ ≤ K) (x : T.Obj 0)
53     (hx : x ∈ closure T.finiteCore) : x ∈ T.recoverable := by
54   apply tendsto_zero_iff_norm_tendsto_zero.mpr
55   apply Metric.tendsto_atTop.mpr
56   intro ε hε
57   have hK1 : 0 < K+1 := by linarith
58   obtain ⟨y, ⟨N, hN⟩, hxy⟩ := Metric.mem_closure_iff.1 hx
59     (ε/(K+1)) (div_pos hε hK1)
60   refine ⟨N, fun n hn => ?_⟩
61   have hy : T.remainder n y = 0 := T.remainder_zero_after y N hN n hn
62   have hd : T.remainder n x = T.remainder n (x-y) := by rw [map_sub, hy, sub_zero]
63   have hnlt : ‖T.remainder n x‖ < ε := by
64     calc
65       _ = ‖T.remainder n (x-y)‖ := congrArg norm hd
66       _ ≤ ‖T.remainder n‖ * ‖x-y‖ := (T.remainder n).le_opNorm _
67       _ ≤ K * ‖x-y‖ := mul_le_mul_of_nonneg_right (hQ n) (norm_nonneg _)
68       _ ≤ (K+1) * ‖x-y‖ := by nlinarith [norm_nonneg (x-y)]
69       _ < (K+1) * (ε/(K+1)) :=
70         mul_lt_mul_of_pos_left (by simpa only [dist_eq_norm] using hxy) hK1
71       _ = ε := by field_simp
72   simpa only [Real.dist_eq, sub_zero, abs_of_nonneg (norm_nonneg _)] using hnlt
73 
74 /-- Exact description of the infinite reconstruction domain under uniform bounds. -/
75 theorem recoverable_iff_closure_finiteCore (K : ℝ) (hK : 0 ≤ K)
76     (hQ : ∀ N, ‖T.remainder N‖ ≤ K) (x : T.Obj 0) :
77     x ∈ T.recoverable ↔ x ∈ closure T.finiteCore :=
78   ⟨T.recoverable_mem_closure_finiteCore x, T.recoverable_of_mem_closure K hK hQ x⟩
79 
80 /-- Universal reconstruction is equivalent to density, not assumed from the outset. -/
81 theorem all_recoverable_iff_dense (K : ℝ) (hK : 0 ≤ K)
82     (hQ : ∀ N, ‖T.remainder N‖ ≤ K) :
83     (∀ x, x ∈ T.recoverable) ↔ Dense T.finiteCore := by
84   constructor
85   · intro h x
86     exact T.recoverable_mem_closure_finiteCore x (h x)
87   · intro h x
88     exact T.recoverable_of_mem_closure K hK hQ x (h x)
89 
90 /-- A directly usable infinite reconstruction theorem from stability and density. -/
91 theorem ordered_reconstruction_of_dense (K : ℝ) (hK : 0 ≤ K)
92     (hQ : ∀ N, ‖T.remainder N‖ ≤ K) (hdense : Dense T.finiteCore)
93     (x : T.Obj 0) :
94     Tendsto (fun N => ∑ n ∈ Finset.range N, T.detailTerm x n) atTop (𝓝 x) := by
95   apply (T.ordered_reconstruction_iff x).2
96   exact T.recoverable_of_mem_closure K hK hQ x (hdense x)
97 
98 /-- Density plus stability excludes all nonzero persistent coarse information. -/
99 theorem persistent_eq_bot_of_dense (K : ℝ) (hK : 0 ≤ K)
100     (hQ : ∀ N, ‖T.remainder N‖ ≤ K) (hdense : Dense T.finiteCore) :
101     T.persistent = ⊥ := by
102   apply le_antisymm _ bot_le
103   intro x hx
104   rw [Submodule.mem_bot]
105   exact T.persistent_recoverable_zero x hx
106     (T.recoverable_of_mem_closure K hK hQ x (hdense x))
107 
108 end CoarseningCascade
109 end KomorebiSpace
110 end

Back to source controls