ProtectedBoundedRealization.lean

1 import KomorebiSpace.BoundedApproximateRealization
2 import KomorebiSpace.ProtectedHilbertRepair
3 
4 /-!
5 # Bounded protected approximate realization
6 
7 WR01 is applied to the actual protected kernel with its inherited Hilbert norm.
8 The conclusion constructs an exact repaired candidate and retains the very same
9 correction budget. No closed-range hypothesis is introduced.
10 -/
11 
12 set_option autoImplicit false
13 noncomputable section
14 
15 open Filter Topology
16 
17 namespace KomorebiSpace.ProtectedBoundedRealization
18 
19 variable {E Y Z : Type*}
20 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
21 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
22 variable [NormedAddCommGroup Z] [NormedSpace ℝ Z]
23 
24 /-- An exact repair with the original protected data and the same norm budget. -/
25 theorem exists_exact_repair_of_bounded_approximation
26     (D : E →L[ℝ] Y) (p : E →L[ℝ] Z) (f : E)
27     (u : ℕ → p.ker) (M : ℝ)
28     (hbound : ∀ n, ‖u n‖ ≤ M)
29     (hresidual : Tendsto (fun n => ‖D (u n) - D f‖) atTop (𝓝 0)) :
30     ∃ y : E, D y = 0 ∧ p y = p f ∧ ‖f - y‖ ≤ M := by
31   obtain ⟨a, ha, hnorm⟩ :=
32     BoundedApproximateRealization.exists_solution_of_bounded_residual_tendsto_zero
33       (ProtectedHilbertRepair.restricted D p) u (D f) M hbound hresidual
34   refine ⟨f - (a : E), ?_, ?_, ?_⟩
35   · rw [map_sub]
36     exact sub_eq_zero.mpr ha.symm
37   · rw [map_sub]
38     have hp : p (a : E) = 0 := a.property
39     rw [hp, sub_zero]
40   · rw [sub_sub_cancel]
41     exact hnorm
42 
43 end KomorebiSpace.ProtectedBoundedRealization

Back to source controls