Normed.lean

1 import KomorebiLSM.Realization
2 import KomorebiLSM.LinearClosure
3 import Mathlib.Analysis.Normed.Operator.NormedSpace
4 import Mathlib.Tactic.Linarith
5 
6 /-! Norm inequalities for P1 and P7, using actual continuous linear maps and
7 Mathlib's operator norm, rather than postulated error budgets. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM
10 universe u v w
11 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
12 variable {X : Type v} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
13 variable {C : Type w} [NormedAddCommGroup C] [NormedSpace 𝕜 C]
14 
15 /-- Bridge from bounded linear realization to the exact set-level contract. -/
16 def continuousRealization (A : X →L[𝕜] C) (S : C →L[𝕜] X)
17     (h : ∀ x, S (A x) = x) : Realization X C := ⟨A, S, h⟩
18 
19 theorem realization_norm_product (A : X →L[𝕜] C) (S : C →L[𝕜] X)
20     (h : ∀ x, S (A x) = x) (x : X) : ‖x‖ ≤ ‖S‖ * ‖A x‖ := by
21   have hs := S.le_opNorm (A x)
22   rwa [h] at hs
23 
24 theorem synthesis_norm_positive [Nontrivial X]
25     (A : X →L[𝕜] C) (S : C →L[𝕜] X) (h : ∀ x, S (A x) = x) :
26     0 < ‖S‖ := by
27   apply norm_pos_iff.mpr
28   intro hs
29   obtain ⟨x, hx⟩ := exists_ne (0 : X)
30   have hzero := h x
31   rw [hs, zero_apply] at hzero
32   exact hx hzero.symm
33 
34 theorem analysis_norm_lower [Nontrivial X]
35     (A : X →L[𝕜] C) (S : C →L[𝕜] X) (h : ∀ x, S (A x) = x) (x : X) :
36     ‖x‖ / ‖S‖ ≤ ‖A x‖ := by
37   apply (div_le_iff₀ (synthesis_norm_positive A S h)).mpr
38   simpa only [mul_comm] using realization_norm_product A S h x
39 
40 theorem synthesis_perturbation_bound (S : C →L[𝕜] X) (c e : C) :
41     ‖S (c + e) - S c‖ ≤ ‖S‖ * ‖e‖ := by
42   simpa only [map_add, add_sub_cancel_left] using S.le_opNorm e
43 
44 /-- The omitted vector is measured after applying Q, while amplification is
45 measured with PLQ itself. The idempotence proof justifies that sharper form. -/
46 theorem closure_norm_bound (P L : X →L[𝕜] X)
47     (idem : ∀ x, P (P x) = P x) (x : X) :
48     ‖P (L x) - P (L (P x))‖ ≤
49       ‖P.comp (L.comp (ContinuousLinearMap.id 𝕜 X - P))‖ * ‖x - P x‖ := by
50   let Q := ContinuousLinearMap.id 𝕜 X - P
51   let D := P.comp (L.comp Q)
52   have h := D.le_opNorm (Q x)
53   have hq : Q (Q x) = Q x := by
54     simp only [Q, sub_apply, ContinuousLinearMap.id_apply,
55       map_sub, idem, sub_self, sub_zero]
56   change ‖P (L (Q (Q x)))‖ ≤ ‖D‖ * ‖Q x‖ at h
57   rw [hq] at h
58   simpa only [D, Q, sub_apply, ContinuousLinearMap.id_apply,
59     map_sub] using h
60 
61 /-- The metric obstruction in P22 applies to every common proposed fine state. -/
62 theorem refinement_worst_case_lower (w a b : X) :
63     (1 / 2 : ℝ) * ‖a - b‖ ≤ max ‖w-a‖ ‖w-b‖ := by
64   have htri : ‖a-b‖ ≤ ‖w-a‖ + ‖w-b‖ := by
65     calc
66       ‖a-b‖ = ‖(a-w)+(w-b)‖ := by congr 1; abel
67       _ ≤ ‖a-w‖ + ‖w-b‖ := norm_add_le _ _
68       _ = ‖w-a‖ + ‖w-b‖ := by rw [norm_sub_rev a w]
69   have ha := le_max_left ‖w-a‖ ‖w-b‖
70   have hb := le_max_right ‖w-a‖ ‖w-b‖
71   linarith
72 
73 end Komorebi.LSM

Back to source controls