BoundedApproximateRealization.lean

1 import Mathlib.Analysis.InnerProductSpace.Adjoint
2 import Mathlib.Analysis.Normed.Module.WeakDual
3 
4 /-!
5 # Bounded approximate realization (WR01)
6 
7 The bounded approximation theorem for real Hilbert spaces, retaining the exact
8 norm budget. The proof uses weak-star compactness of the dual ball and the Riesz
9 isometric equivalence. It does not assume separability or a closed operator range,
10 and it does not assert strong convergence of the supplied candidates.
11 -/
12 
13 noncomputable section
14 
15 open Filter Set Metric Topology
16 
17 namespace KomorebiSpace.BoundedApproximateRealization
18 
19 variable {H Y : Type*}
20 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
21 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
22 
23 /-- Even a frequently recurring budget bound is enough for exact realization.
24 This stronger filter form makes the full divergence-to-infinity corollary immediate. -/
25 theorem exists_solution_of_frequently_bounded
26     (T : H →L[ℝ] Y) {ι : Type*} {l : Filter ι} [NeBot l]
27     (u : ι → H) (r : Y) (M : ℝ)
28     (hbound : ∃ᶠ i in l, ‖u i‖ ≤ M)
29     (himage : Tendsto (fun i => T (u i)) l (𝓝 r)) :
30     ∃ a : H, T a = r ∧ ‖a‖ ≤ M := by
31   let v : ι → WeakDual ℝ H := fun i =>
32     StrongDual.toWeakDual (InnerProductSpace.toDual ℝ H (u i))
33   have hv : ∃ᶠ i in l,
34       v i ∈ WeakDual.toStrongDual ⁻¹' closedBall (0 : StrongDual ℝ H) M := by
35     exact hbound.mono fun i hi => by
36       simpa [v, Metric.mem_closedBall, dist_eq_norm] using hi
37   obtain ⟨φ, hφball, hφ⟩ :=
38     (WeakDual.isCompact_closedBall (0 : StrongDual ℝ H) M).exists_mapClusterPt_of_frequently hv
39   let a : H := (InnerProductSpace.toDual ℝ H).symm (WeakDual.toStrongDual φ)
40   refine ⟨a, ?_, ?_⟩
41   · apply ext_inner_right ℝ
42     intro y
43     have heval := hφ.continuousAt_comp (WeakDual.eval_continuous (T.adjoint y)).continuousAt
44     have hlim : Tendsto (fun i => (v i) (T.adjoint y)) l (𝓝 (inner ℝ r y)) := by
45       simpa only [v, StrongDual.toWeakDual_apply,
46         InnerProductSpace.toDual_apply_apply, T.adjoint_inner_right] using
47         himage.inner tendsto_const_nhds
48     have heq : φ (T.adjoint y) = inner ℝ r y :=
49       eq_of_nhds_neBot (heval.clusterPt.mono hlim).neBot
50     simpa only [a, ← T.adjoint_inner_right, InnerProductSpace.toDual_symm_apply,
51       WeakDual.toStrongDual_apply] using heq
52   · have hnorm : ‖WeakDual.toStrongDual φ‖ ≤ M := by
53       simpa only [Set.mem_preimage, Metric.mem_closedBall, dist_eq_norm, sub_zero] using hφball
54     simpa only [a, LinearIsometryEquiv.norm_map] using hnorm
55 
56 /-- WR01, including preservation of the same uniform norm budget. -/
57 theorem exists_solution_of_bounded_approximation
58     (T : H →L[ℝ] Y) (u : ℕ → H) (r : Y) (M : ℝ)
59     (hbound : ∀ n, ‖u n‖ ≤ M)
60     (himage : Tendsto (fun n => T (u n)) atTop (𝓝 r)) :
61     ∃ a : H, T a = r ∧ ‖a‖ ≤ M :=
62   exists_solution_of_frequently_bounded T u r M
63     (Filter.Eventually.of_forall hbound).frequently himage
64 
65 /-- WR01 in the residual norm formulation printed in the monograph. -/
66 theorem exists_solution_of_bounded_residual_tendsto_zero
67     (T : H →L[ℝ] Y) (u : ℕ → H) (r : Y) (M : ℝ)
68     (hbound : ∀ n, ‖u n‖ ≤ M)
69     (hresidual : Tendsto (fun n => ‖T (u n) - r‖) atTop (𝓝 0)) :
70     ∃ a : H, T a = r ∧ ‖a‖ ≤ M := by
71   apply exists_solution_of_bounded_approximation T u r M hbound
72   exact tendsto_iff_norm_sub_tendsto_zero.mpr hresidual
73 
74 /-- Exact solvability is equivalent to existence of a bounded approximating sequence. -/
75 theorem mem_range_iff_bounded_approximation (T : H →L[ℝ] Y) (r : Y) :
76     r ∈ Set.range T ↔
77       ∃ (u : ℕ → H) (M : ℝ), (∀ n, ‖u n‖ ≤ M) ∧
78         Tendsto (fun n => ‖T (u n) - r‖) atTop (𝓝 0) := by
79   constructor
80   · rintro ⟨a, rfl⟩
81     refine ⟨fun _ => a, ‖a‖, fun _ => le_rfl, ?_⟩
82     simpa only [sub_self, norm_zero] using
83       (tendsto_const_nhds : Tendsto (fun _ : ℕ => (0 : ℝ)) atTop (𝓝 0))
84   · rintro ⟨u, M, hbound, hresidual⟩
85     obtain ⟨a, ha, _⟩ :=
86       exists_solution_of_bounded_residual_tendsto_zero T u r M hbound hresidual
87     exact ⟨a, ha⟩
88 
89 /-- For unattained data, every approximating sequence escapes every finite norm budget.
90 No closed-range assumption is used, and the conclusion is convergence to infinity,
91 not merely failure of a uniform bound. -/
92 theorem norm_tendsto_atTop_of_not_mem_range
93     (T : H →L[ℝ] Y) (u : ℕ → H) (r : Y)
94     (hr : r ∉ Set.range T)
95     (himage : Tendsto (fun n => T (u n)) atTop (𝓝 r)) :
96     Tendsto (fun n => ‖u n‖) atTop atTop := by
97   apply Filter.tendsto_atTop.mpr
98   intro M
99   by_contra h
100   have hfreq : ∃ᶠ n in atTop, ‖u n‖ ≤ M := by
101     exact (Filter.not_eventually.mp h).mono fun n hn => (lt_of_not_ge hn).le
102   obtain ⟨a, ha, _⟩ := exists_solution_of_frequently_bounded T u r M hfreq himage
103   exact hr ⟨a, ha⟩
104 
105 end KomorebiSpace.BoundedApproximateRealization

Back to source controls