DiagonalRangeObstruction.lean

1 import KomorebiSpace.InfiniteDiagonalModel
2 import KomorebiSpace.HilbertKernelProjection
3 
4 /-!
5 # The concrete infinite diagonal closed-range obstruction
6 
7 The vectors here are actual unit coordinate vectors in `lp (fun _ : ℕ => ℝ) 2`.
8 The operator is the same `T` used by the diagonal regularization model.
9 -/
10 
11 set_option autoImplicit false
12 noncomputable section
13 namespace KomorebiSpace.DiagonalRegularization
14 open Filter Topology
15 open scoped RealInnerProductSpace
16 
17 /-- The unit vector in natural coordinate `j`, representing printed coordinate `j+1`. -/
18 def unitCoordinate (j : ℕ) : H := lp.single 2 j (1 : ℝ)
19 
20 @[simp] theorem norm_unitCoordinate (j : ℕ) : ‖unitCoordinate j‖ = 1 := by
21   simp [unitCoordinate, lp.norm_single (by norm_num : (0 : ENNReal) < 2)]
22 
23 /-- The actual diagonal operator has eigenvalue `1/(j+1)` on each coordinate. -/
24 theorem T_unitCoordinate (j : ℕ) : T (unitCoordinate j) = wCoord j • unitCoordinate j := by
25   apply lp.ext
26   funext k
27   by_cases hk : k = j
28   · subst k
29     simp [unitCoordinate]
30   · simp [unitCoordinate, lp.single_apply, hk]
31 
32 /-- Unit witnesses have exactly the printed reciprocal residual norm. -/
33 theorem norm_T_unitCoordinate (j : ℕ) : ‖T (unitCoordinate j)‖ = 1 / ((j : ℝ) + 1) := by
34   rw [T_unitCoordinate, norm_smul, norm_unitCoordinate, mul_one]
35   simp [wCoord, index, Real.norm_eq_abs, abs_of_pos (by positivity : (0 : ℝ) < j + 1),
36     one_div]
37 
38 /-- The residuals of actual unit vectors tend to zero in the infinite Hilbert model. -/
39 theorem tendsto_norm_T_unitCoordinate :
40     Tendsto (fun j : ℕ => ‖T (unitCoordinate j)‖) atTop (𝓝 0) := by
41   simpa only [norm_T_unitCoordinate] using
42     (tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ))
43 
44 /-- Injectivity identifies the exact space of the actual diagonal operator with zero. -/
45 theorem T_ker_eq_bot : T.ker = ⊥ := by
46   exact LinearMap.ker_eq_bot.mpr T_injective
47 
48 /-- The coordinate witnesses lie in the orthogonal complement required by the abstract theorem. -/
49 theorem unitCoordinate_mem_ker_orthogonal (j : ℕ) : unitCoordinate j ∈ T.kerᗮ := by
50   rw [T_ker_eq_bot, Submodule.bot_orthogonal_eq_top]
51   trivial
52 
53 /-- Every proposed finite inverse gain fails on a concrete unit coordinate vector. -/
54 theorem unitCoordinate_witness (C : ℝ) (_hC : 0 ≤ C) :
55     ∃ j : ℕ, C * ‖T (unitCoordinate j)‖ < 1 := by
56   obtain ⟨j, hj⟩ := exists_nat_gt C
57   refine ⟨j, ?_⟩
58   rw [norm_T_unitCoordinate, mul_one_div]
59   exact (div_lt_one (by positivity : (0 : ℝ) < j + 1)).mpr (by linarith)
60 
61 /-- The actual infinite diagonal operator has nonclosed range. -/
62 theorem T_not_closed_range : ¬ IsClosed (Set.range T) := by
63   apply HilbertKernelProjection.not_closed_range_of_unit_witnesses T
64   intro C hC
65   obtain ⟨j, hj⟩ := unitCoordinate_witness C hC
66   exact ⟨unitCoordinate j, unitCoordinate_mem_ker_orthogonal j, norm_unitCoordinate j, hj⟩
67 
68 /-- Images of the actual finite unit prefixes converge in Hilbert norm to `w`. -/
69 theorem tendsto_T_hardPrefix :
70     Tendsto (fun N : ℕ => T (hardPrefix N)) atTop (𝓝 w) := by
71   have hsq : Tendsto (fun N : ℕ => ‖w - T (hardPrefix N)‖^2) atTop (𝓝 0) := by
72     simpa only [norm_hardPrefix_residual_sq] using
73       (tendsto_sum_nat_add (fun j : ℕ => (wCoord j)^2))
74   have hn := Real.continuous_sqrt.continuousAt.tendsto.comp hsq
75   apply tendsto_iff_norm_sub_tendsto_zero.mpr
76   simpa only [Function.comp_def, Real.sqrt_sq (norm_nonneg _), Real.sqrt_zero, norm_sub_rev] using hn
77 
78 /-- The escaping datum lies in the closure of the actual operator range. -/
79 theorem w_mem_closure_range : w ∈ closure (Set.range T) := by
80   apply mem_closure_of_tendsto tendsto_T_hardPrefix
81   exact Filter.Eventually.of_forall (fun N => ⟨hardPrefix N, rfl⟩)
82 
83 /-- Any exact preimage would have every coordinate equal to one, contradicting square summability. -/
84 theorem w_not_mem_range : w ∉ Set.range T := by
85   rintro ⟨x, hx⟩
86   have hcoord (j : ℕ) : x j = 1 := by
87     have hj := congrArg (fun u : H => u j) hx
88     have hw0 : wCoord j ≠ 0 := by
89       unfold wCoord index
90       positivity
91     apply mul_left_cancel₀ hw0
92     simpa only [T_apply, w_apply, mul_one] using hj
93   have hs : Summable (fun _ : ℕ => (1 : ℝ)) := by
94     simpa only [hcoord, one_pow] using summable_coordinates_sq x
95   exact one_ne_zero ((summable_const_iff (1 : ℝ)).mp hs)
96 
97 /-- The printed diagonal example exhibits closure without exact attainability. -/
98 theorem w_mem_closure_not_range :
99     w ∈ closure (Set.range T) ∧ w ∉ Set.range T :=
100   ⟨w_mem_closure_range, w_not_mem_range⟩
101 
102 end KomorebiSpace.DiagonalRegularization

Back to source controls