MovingDescent.lean

1 import KomorebiSpace.MovingKernelBounds
2 import KomorebiSpace.DescentClosedRange
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Perturbing the actual quantitative-descent projector
8 
9 The raw local candidate space and its Hilbert norm are fixed. Both the local
10 and overlap operators may change. Each system must carry its own local and
11 restricted-matching stability evidence. The new theorem compares the actual
12 v0.30 two-stage repairs, not newly substituted projection definitions.
13 -/
14 universe u v w
15 noncomputable section
16 namespace KomorebiSpace
17 namespace MovingDescent
18 open HilbertKernelProjection QuantitativeDescent
19 variable {E : Type u} {R : Type v} {Y : Type w}
20 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
21 variable [NormedAddCommGroup R] [NormedSpace ℝ R] [CompleteSpace R]
22 variable [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]
23 variable (D : E →L[ℝ] R) (C : E →L[ℝ] Y)
24 
25 /-- The old two-stage theorem supplies a bound on its unchanged joint residual. -/
26 def bound (hD : IsClosed (Set.range D)) (hB : IsClosed (Set.range (matching D C))) :
27     ResidualRobustness.Bound (joint D C) where
28   constant := stabilityGain D C hD hB
29   nonneg := stabilityGain_nonneg D C hD hB
30   estimate x := by
31     rw [← repair_eq_projection]
32     exact stable_repair D C hD hB x
33 
34 omit [CompleteSpace E] [CompleteSpace R] [CompleteSpace Y] in
35 /-- The product residual uses max: local and overlap uncertainties are not added. -/
36 theorem joint_operator_error (D' : E →L[ℝ] R) (C' : E →L[ℝ] Y)
37     {εD εC : ℝ} (hD : ‖D-D'‖ ≤ εD) (hC : ‖C-C'‖ ≤ εC) :
38     ‖joint D C-joint D' C'‖ ≤ max εD εC := by
39   have hεD : 0 ≤ εD := (norm_nonneg _).trans hD
40   have hεC : 0 ≤ εC := (norm_nonneg _).trans hC
41   apply ContinuousLinearMap.opNorm_le_bound _ (hεD.trans (le_max_left _ _))
42   intro x
43   change ‖(D x-D' x,C x-C' x)‖ ≤ _
44   rw [Prod.norm_def]
45   apply max_le
46   · exact ((D-D').le_opNorm x).trans
47       (mul_le_mul_of_nonneg_right (hD.trans (le_max_left _ _)) (norm_nonneg x))
48   · exact ((C-C').le_opNorm x).trans
49       (mul_le_mul_of_nonneg_right (hC.trans (le_max_right _ _)) (norm_nonneg x))
50 
51 /-- Motion of the actual global two-stage repairs. -/
52 theorem repair_motion (D' : E →L[ℝ] R) (C' : E →L[ℝ] Y)
53     (hD : IsClosed (Set.range D)) (hB : IsClosed (Set.range (matching D C)))
54     (hD' : IsClosed (Set.range D')) (hB' : IsClosed (Set.range (matching D' C')))
55     {εD εC : ℝ} (heD : ‖D-D'‖ ≤ εD) (heC : ‖C-C'‖ ≤ εC) :
56     ‖repair D C-repair D' C'‖ ≤
57       max (stabilityGain D C hD hB) (stabilityGain D' C' hD' hB') * max εD εC := by
58   have hid : repair D C=projection (joint D C) := by ext x; exact repair_eq_projection D C x
59   have hid' : repair D' C'=projection (joint D' C') := by ext x; exact repair_eq_projection D' C' x
60   rw [hid,hid']
61   exact MovingKernel.projection_opNorm _ _ (bound D C hD hB) (bound D' C' hD' hB')
62     (joint_operator_error D C D' C' heD heC)
63 
64 /-- Simultaneous change of local observations and reference model. -/
65 theorem repaired_data_motion (D' : E →L[ℝ] R) (C' : E →L[ℝ] Y)
66     (hD : IsClosed (Set.range D)) (hB : IsClosed (Set.range (matching D C)))
67     (hD' : IsClosed (Set.range D')) (hB' : IsClosed (Set.range (matching D' C')))
68     {εD εC : ℝ} (heD : ‖D-D'‖ ≤ εD) (heC : ‖C-C'‖ ≤ εC) (x y : E) :
69     ‖repair D C x-repair D' C' y‖ ≤ ‖x-y‖ +
70       (max (stabilityGain D C hD hB) (stabilityGain D' C' hD' hB') * max εD εC)*‖y‖ := by
71   rw [repair_eq_projection,repair_eq_projection]
72   exact MovingKernel.repaired_input_motion _ _ (bound D C hD hB) (bound D' C' hD' hB')
73     (joint_operator_error D C D' C' heD heC) x y
74 
75 end MovingDescent
76 end KomorebiSpace
77 end

Back to source controls