NormedDefects.lean

1 import Mathlib.Analysis.Normed.Ring.Basic
2 import Mathlib.Tactic.NoncommRing
3 import Mathlib.Tactic.Linarith
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Quantitative defects and transported finite telescopes
9 
10 The noncommutative ring model includes bounded endomorphism algebras when those
11 are supplied. Arbitrary square defects cannot be added across distinct Hom
12 spaces without whiskering them into a common Hom space.
13 -/
14 universe u
15 namespace KomorebiSpace
16 namespace NormedDefects
17 
18 variable {R : Type u}
19 
20 def defect [Ring R] (v f f' u : R) : R := v*f - f'*u
21 
22 section Ring
23 variable [Ring R]
24 
25 theorem horizontal (u v w f g f' g' : R) :
26     defect w (g*f) (g'*f') u = defect w g g' v * f + g' * defect v f f' u := by
27   unfold defect
28   noncomm_ring
29 
30 /-- Algebraic compression-shell formula, with the projection identities explicit. -/
31 theorem compression_shell (P Q T : R) (hPP : P*P = P) (hQP : Q*P = P) :
32     (Q*T*Q)*P - P*(P*T*P) = (Q-P)*T*P := by
33   calc
34     (Q*T*Q)*P - P*(P*T*P) = Q*T*(Q*P) - (P*P)*T*P := by noncomm_ring
35     _ = Q*T*P - P*T*P := by rw [hQP, hPP]
36     _ = (Q-P)*T*P := by noncomm_ring
37 
38 /-- A finite transported Stokes identity for a certified sequence of path swaps. -/
39 theorem transported_telescope (T A Ω B : ℕ → R)
40     (hswap : ∀ k, T (k+1) - T k = A k * Ω k * B k) (n : ℕ) :
41     T n - T 0 = ∑ k ∈ Finset.range n, A k * Ω k * B k := by
42   induction n with
43   | zero => simp
44   | succ n ih =>
45     rw [Finset.sum_range_succ, ← ih, ← hswap n]
46     abel
47 end Ring
48 
49 section Normed
50 variable [NormedRing R]
51 
52 theorem horizontal_norm (u v w f g f' g' : R) :
53     ‖defect w (g*f) (g'*f') u‖ ≤
54       ‖defect w g g' v‖ * ‖f‖ + ‖g'‖ * ‖defect v f f' u‖ := by
55   rw [horizontal]
56   exact (norm_add_le _ _).trans (add_le_add (norm_mul_le _ _) (norm_mul_le _ _))
57 
58 theorem horizontal_contractive (u v w f g f' g' : R)
59     (hf : ‖f‖ ≤ 1) (hg : ‖g'‖ ≤ 1) :
60     ‖defect w (g*f) (g'*f') u‖ ≤ ‖defect w g g' v‖ + ‖defect v f f' u‖ := by
61   calc
62     ‖defect w (g*f) (g'*f') u‖ ≤
63         ‖defect w g g' v‖ * ‖f‖ + ‖g'‖ * ‖defect v f f' u‖ :=
64       horizontal_norm u v w f g f' g'
65     _ ≤ ‖defect w g g' v‖ * 1 + 1 * ‖defect v f f' u‖ :=
66       add_le_add (mul_le_mul_of_nonneg_left hf (norm_nonneg _))
67         (mul_le_mul_of_nonneg_right hg (norm_nonneg _))
68     _ = _ := by rw [mul_one, one_mul]
69 
70 theorem whiskered_norm (a e b : R) (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) :
71     ‖a*e*b‖ ≤ ‖e‖ := by
72   calc
73     ‖a*e*b‖ ≤ ‖a*e‖ * ‖b‖ := norm_mul_le _ _
74     _ ≤ (‖a‖*‖e‖)*‖b‖ := mul_le_mul_of_nonneg_right (norm_mul_le _ _) (norm_nonneg _)
75     _ ≤ (1*‖e‖)*1 := mul_le_mul
76       (mul_le_mul_of_nonneg_right ha (norm_nonneg _)) hb
77       (norm_nonneg _) (mul_nonneg (by norm_num) (norm_nonneg _))
78     _ = ‖e‖ := by rw [one_mul, mul_one]
79 
80 theorem transported_stokes_bound (T A Ω B : ℕ → R)
81     (hswap : ∀ k, T (k+1) - T k = A k * Ω k * B k)
82     (hA : ∀ k, ‖A k‖ ≤ 1) (hB : ∀ k, ‖B k‖ ≤ 1) (n : ℕ) :
83     ‖T n - T 0‖ ≤ ∑ k ∈ Finset.range n, ‖Ω k‖ := by
84   rw [transported_telescope T A Ω B hswap n]
85   apply (norm_sum_le _ _).trans
86   apply Finset.sum_le_sum
87   intro k hk
88   exact whiskered_norm _ _ _ (hA k) (hB k)
89 
90 end Normed
91 end NormedDefects
92 end KomorebiSpace

Back to source controls