DescentClosedRange.lean

1 import KomorebiSpace.QuantitativeDescent
2 
3 set_option autoImplicit false
4 universe u v w
5 noncomputable section
6 namespace KomorebiSpace
7 namespace QuantitativeDescent
8 open HilbertKernelProjection
9 variable {E : Type u} {R : Type v} {Y : Type w}
10 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
11 variable [NormedAddCommGroup R] [NormedSpace ℝ R]
12 variable [NormedAddCommGroup Y] [NormedSpace ℝ Y]
13 variable (D : E →L[ℝ] R) (C : E →L[ℝ] Y)
14 
15 @[simp] theorem locallyExact_coe (z : D.ker) : locallyExact D z.val = z := by
16   apply Subtype.ext
17   exact projection_fixes D z.val z.property
18 
19 @[simp] theorem repair_of_local (z : D.ker) :
20     repair D C z.val = (projection (matching D C) z).val := by
21   change (projection (matching D C) (locallyExact D z.val)).val = _
22   rw [locallyExact_coe]
23 
24 /-- Uncertain measurements are allowances, not equality with exact residuals. -/
25 theorem measured_error {a b γ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hγ : 0 ≤ γ)
26     (hlocal : ∀ x, ‖x-projection D x‖ ≤ a*‖D x‖)
27     (hmatch : ∀ z, ‖z-projection (matching D C) z‖ ≤ b*‖matching D C z‖)
28     (hint : InteractionBound D C γ) (x : E) (r : R) (s : Y)
29     {η₁ η₂ : ℝ} (h₁ : ‖D x-r‖ ≤ η₁) (h₂ : ‖C x-s‖ ≤ η₂) :
30     ‖x-repair D C x‖ ≤ a*(1+b*γ)*(‖r‖+η₁)+b*(‖s‖+η₂) := by
31   have hD : ‖D x‖ ≤ ‖r‖+η₁ := by
32     have h := norm_sub_le_norm_sub_add_norm_sub (D x) r 0
33     simp only [sub_zero] at h
34     linarith
35   have hC : ‖C x‖ ≤ ‖s‖+η₂ := by
36     have h := norm_sub_le_norm_sub_add_norm_sub (C x) s 0
37     simp only [sub_zero] at h
38     linarith
39   have hn : 0 ≤ a*(1+b*γ) := by positivity
40   exact (repair_error D C hb hγ hlocal hmatch hint x).trans
41     (add_le_add (mul_le_mul_of_nonneg_left hD hn) (mul_le_mul_of_nonneg_left hC hb))
42 
43 variable [CompleteSpace R] [CompleteSpace Y]
44 
45 /-- Closed joint range forces stability of overlap matching within locally exact data. -/
46 theorem matching_closed_of_joint_closed
47     (h : IsClosed (Set.range (joint D C))) : IsClosed (Set.range (matching D C)) := by
48   obtain ⟨b, hb, he⟩ := (closed_range_iff_bound (joint D C)).mp h
49   apply closed_range_of_bound (matching D C) b hb
50   intro z
51   have hz := he z.val
52   rw [← repair_eq_projection, repair_of_local] at hz
53   change ‖z.val - (projection (matching D C) z).val‖ ≤ b*‖(D z.val,C z.val)‖ at hz
54   have hzD : D z.val = 0 := z.property
55   rw [hzD, Prod.norm_def, norm_zero, max_eq_right (norm_nonneg _)] at hz
56   exact hz
57 
58 /-- The sufficient global coefficient is derived from the two actual closed ranges. -/
59 def stabilityGain (hD : IsClosed (Set.range D))
60     (hB : IsClosed (Set.range (matching D C))) : ℝ :=
61   gain D hD * (1 + gain (matching D C) hB * ‖C‖) + gain (matching D C) hB
62 
63 theorem stabilityGain_nonneg (hD : IsClosed (Set.range D))
64     (hB : IsClosed (Set.range (matching D C))) : 0 ≤ stabilityGain D C hD hB := by
65   have ha := gain_nonneg D hD
66   have hb := gain_nonneg (matching D C) hB
67   unfold stabilityGain
68   positivity
69 
70 theorem stable_repair (hD : IsClosed (Set.range D))
71     (hB : IsClosed (Set.range (matching D C))) (x : E) :
72     ‖x-repair D C x‖ ≤ stabilityGain D C hD hB * ‖joint D C x‖ := by
73   have he := repair_error D C (gain_nonneg _ hB) (norm_nonneg C)
74     (error_bound D hD) (error_bound _ hB) (operator_interaction D C) x
75   have h₁ := le_max_left ‖D x‖ ‖C x‖
76   have h₂ := le_max_right ‖D x‖ ‖C x‖
77   have ha := gain_nonneg D hD
78   have hb := gain_nonneg (matching D C) hB
79   have hn : 0 ≤ gain D hD * (1 + gain (matching D C) hB * ‖C‖) := by positivity
80   have ht := add_le_add (mul_le_mul_of_nonneg_left h₁ hn)
81     (mul_le_mul_of_nonneg_left h₂ (gain_nonneg _ hB))
82   change _ ≤ stabilityGain D C hD hB * max ‖D x‖ ‖C x‖
83   exact he.trans (by simpa only [stabilityGain, add_mul] using ht)
84 
85 theorem joint_closed_of_matching_closed (hD : IsClosed (Set.range D))
86     (hB : IsClosed (Set.range (matching D C))) : IsClosed (Set.range (joint D C)) := by
87   apply closed_range_of_bound _ (stabilityGain D C hD hB) (stabilityGain_nonneg D C hD hB)
88   intro x
89   rw [← repair_eq_projection]
90   exact stable_repair D C hD hB x
91 
92 /-- Local stability isolates the precise remaining global stability obligation. -/
93 theorem joint_closed_iff_matching_closed (hD : IsClosed (Set.range D)) :
94     IsClosed (Set.range (joint D C)) ↔ IsClosed (Set.range (matching D C)) :=
95   ⟨matching_closed_of_joint_closed D C, joint_closed_of_matching_closed D C hD⟩
96 
97 /-- Even an arbitrary nonlinear selection of global exact outputs cannot evade this criterion. -/
98 theorem matching_closed_iff_near_joint (hD : IsClosed (Set.range D)) :
99     IsClosed (Set.range (matching D C)) ↔
100       ∃ M : ℝ, 0 ≤ M ∧ ∀ x : E, ∃ y : E,
101         D y = 0 ∧ C y = 0 ∧ ‖x-y‖ ≤ M*‖joint D C x‖ := by
102   rw [← joint_closed_iff_matching_closed D C hD, closed_range_iff_near_exact]
103   simp only [joint_zero_iff, and_assoc]
104 
105 end QuantitativeDescent
106 end KomorebiSpace
107 end

Back to source controls