CoreStability.lean

1 import KomorebiLSM.IdentificationBound
2 
3 set_option autoImplicit false
4 set_option maxHeartbeats 400000
5 namespace Komorebi.LSM.Identification
6 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
7 variable [FiniteDimensional ℝ E]
8 
9 /-- The fitted core uses the constructed Moore--Penrose inverse. The two-sided
10 inverse laws below identify it with the ordinary square inverse. -/
11 @[irreducible] noncomputable def coreFit (H E' F' B : E →L[ℝ] E) : E →L[ℝ] E :=
12   (B.comp H + F').comp (pinvL (H+E'))
13 
14 theorem core_perturbed_surjective (H E' : E →L[ℝ] E) (hE : ‖E'‖ < rowGain H) :
15     Function.Surjective (H+E') :=
16   surjective_of_adjoint_lower (H+E') (rowGain H-‖E'‖) (sub_pos.mpr hE)
17     (rowGain_perturbation H E')
18 
19 theorem square_pinv_left (H : E →L[ℝ] E) (hs : Function.Surjective H) (x : E) :
20     pinvL H (H x) = x := by
21   have hi : Function.Injective H := (LinearMap.injective_iff_surjective (f := H.toLinearMap)).mpr hs
22   apply hi
23   exact pinvL_right H hs (H x)
24 
25 theorem core_inverse_laws (H E' : E →L[ℝ] E) (hE : ‖E'‖ < rowGain H) :
26     (∀ x, (H+E') (pinvL (H+E') x) = x) ∧
27     (∀ x, pinvL (H+E') ((H+E') x) = x) := by
28   have hs := core_perturbed_surjective H E' hE
29   exact ⟨pinvL_right _ hs, square_pinv_left _ hs⟩
30 
31 theorem core_error_identity (H E' F' B : E →L[ℝ] E) (hE : ‖E'‖ < rowGain H) :
32     coreFit H E' F' B - B = (F'-B.comp E').comp (pinvL (H+E')) := by
33   simpa [coreFit] using noisy_identification_identity H 0 E' F' B hE
34 
35 theorem core_error_bound (H E' F' B : E →L[ℝ] E) (hE : ‖E'‖ < rowGain H) :
36     ‖coreFit H E' F' B - B‖ ≤
37       (‖F'‖+‖B‖*‖E'‖)/(rowGain H-‖E'‖) := by
38   simpa [coreFit] using noisy_identification_bound H 0 E' F' B hE
39 
40 theorem core_fitted_residual (H E' F' B : E →L[ℝ] E) (hE : ‖E'‖ < rowGain H) :
41     (coreFit H E' F' B-B).comp H = F'-(coreFit H E' F' B).comp E' := by
42   apply ContinuousLinearMap.ext
43   intro x
44   have he : coreFit H E' F' B ((H+E') x) = B (H x)+F' x := by
45     simp only [coreFit, ContinuousLinearMap.comp_apply]
46     rw [square_pinv_left _ (core_perturbed_surjective H E' hE)]
47     rfl
48   simp only [add_apply, map_add] at he
49   simp only [ContinuousLinearMap.comp_apply, sub_apply]
50   exact sub_eq_sub_iff_add_eq_add.mpr (by simpa [add_comm] using he)
51 
52 theorem core_fitted_identity (H E' F' B : E →L[ℝ] E) (hE : ‖E'‖ < rowGain H) :
53     coreFit H E' F' B-B = (F'-(coreFit H E' F' B).comp E').comp (pinvL H) := by
54   have hs := surjective_of_adjoint_lower H (rowGain H)
55     (lt_of_le_of_lt (norm_nonneg E') hE) (rowGain_lower H)
56   rw [← core_fitted_residual H E' F' B hE]
57   ext x
58   simp only [ContinuousLinearMap.comp_apply]
59   rw [pinvL_right H hs]
60 
61 theorem core_fitted_bound (H E' F' B : E →L[ℝ] E) (hE : ‖E'‖ < rowGain H) :
62     ‖coreFit H E' F' B-B‖ ≤ (‖F'‖+‖coreFit H E' F' B‖*‖E'‖)/rowGain H := by
63   have hs : 0 < rowGain H := lt_of_le_of_lt (norm_nonneg E') hE
64   have hn : ‖F'-(coreFit H E' F' B).comp E'‖ ≤ ‖F'‖+‖coreFit H E' F' B‖*‖E'‖ :=
65     (norm_sub_le _ _).trans (add_le_add le_rfl (ContinuousLinearMap.opNorm_comp_le _ _))
66   rw [core_fitted_identity H E' F' B hE]
67   calc
68     _ ≤ ‖F'-(coreFit H E' F' B).comp E'‖ * ‖pinvL H‖ := ContinuousLinearMap.opNorm_comp_le _ _
69     _ ≤ (‖F'‖+‖coreFit H E' F' B‖*‖E'‖) * (rowGain H)⁻¹ :=
70       mul_le_mul hn (pinvL_bound H (rowGain H) hs (rowGain_lower H)) (norm_nonneg _) (by positivity)
71     _ = _ := (div_eq_mul_inv _ _).symm
72 
73 theorem core_checked_fitted_bound (H E' F' B : E →L[ℝ] E)
74     (hE : ‖E'‖ < rowGain H) (e : ℝ) (he : ‖E'‖ ≤ e)
75     (hgap : e < rowGain (H+E')) :
76     ‖coreFit H E' F' B-B‖ ≤
77       (‖F'‖+‖coreFit H E' F' B‖*‖E'‖)/(rowGain (H+E')-e) := by
78   have hl : ∀ v, (rowGain (H+E')-e)*‖v‖ ≤ ‖H.adjoint v‖ := by
79     intro v
80     have h := rowGain_perturbation (H+E') (-E') v
81     simp only [norm_neg, add_neg_cancel_right] at h
82     exact (mul_le_mul_of_nonneg_right (sub_le_sub_left he _) (norm_nonneg v)).trans h
83   have hn : ‖F'-(coreFit H E' F' B).comp E'‖ ≤ ‖F'‖+‖coreFit H E' F' B‖*‖E'‖ :=
84     (norm_sub_le _ _).trans (add_le_add le_rfl (ContinuousLinearMap.opNorm_comp_le _ _))
85   rw [core_fitted_identity H E' F' B hE]
86   calc
87     _ ≤ ‖F'-(coreFit H E' F' B).comp E'‖ * ‖pinvL H‖ := ContinuousLinearMap.opNorm_comp_le _ _
88     _ ≤ (‖F'‖+‖coreFit H E' F' B‖*‖E'‖) * (rowGain (H+E')-e)⁻¹ :=
89       mul_le_mul hn (pinvL_bound H _ (sub_pos.mpr hgap) hl) (norm_nonneg _) (by positivity)
90     _ = _ := (div_eq_mul_inv _ _).symm
91 
92 end Komorebi.LSM.Identification

Back to source controls