PacketPerturbation.lean

1 module
2 public import Mathlib.Analysis.Normed.Operator.Basic
3 public import Mathlib.Analysis.Normed.Operator.Bilinear
4 public import Mathlib.Analysis.Normed.Group.InfiniteSum
5 
6 /-!
7 Author: Komorebi P.
8 Paper VIII item 8.1. Actual bounded linear maps and their operator norm.
9 Only error support is needed for the inequality; exact-block support is not assumed.
10 This is not a proof about IEEE arithmetic or a particular CUDA implementation.
11 -/
12 
13 public section
14 set_option autoImplicit false
15 namespace KomorebiPaperVIII
16 open scoped BigOperators
17 variable {K X I E : Type*} [NontriviallyNormedField K]
18 variable [NormedAddCommGroup X] [NormedSpace K X] [Fintype E]
19 
20 /-- The actual operator error is the sum of source-supported error blocks. -/
21 theorem packet_error_operator_identity (P : I → X →L[K] X) (src : E → I)
22     (A Δ : E → X →L[K] X) (hΔ : ∀ e, Δ e = (Δ e).comp (P (src e))) :
23     (∑ e, (A e + Δ e)) - (∑ e, A e) = ∑ e, (Δ e).comp (P (src e)) := by
24   rw [Finset.sum_add_distrib, add_sub_cancel_left]
25   exact Finset.sum_congr rfl (fun e _ => hΔ e)
26 
27 /-- The source-vector identity underlying the packetwise certificate. -/
28 theorem packet_error_action_identity (P : I → X →L[K] X) (src : E → I)
29     (A Δ : E → X →L[K] X) (hΔ : ∀ e, Δ e = (Δ e).comp (P (src e))) (x : X) :
30     ((∑ e, (A e + Δ e)) - (∑ e, A e)) x = ∑ e, Δ e (P (src e) x) := by
31   rw [packet_error_operator_identity P src A Δ hΔ]
32   simp only [sum_apply, ContinuousLinearMap.comp_apply]
33 
34 /-- Theorem 8.1, absolute form, for the actual vector produced by the perturbed operator. -/
35 theorem packet_perturbation_bound (P : I → X →L[K] X) (src : E → I)
36     (A Δ : E → X →L[K] X) (hΔ : ∀ e, Δ e = (Δ e).comp (P (src e))) (x : X) :
37     ‖((∑ e, (A e + Δ e)) - (∑ e, A e)) x‖ ≤ ∑ e, ‖Δ e‖ * ‖P (src e) x‖ := by
38   rw [packet_error_action_identity P src A Δ hΔ]
39   exact (norm_sum_le _ _).trans (Finset.sum_le_sum (fun e _ => (Δ e).le_opNorm _))
40 
41 /-- Theorem 8.1, relative edge-error form. -/
42 theorem packet_relative_perturbation_bound (P : I → X →L[K] X) (src : E → I)
43     (A Δ : E → X →L[K] X) (hΔ : ∀ e, Δ e = (Δ e).comp (P (src e)))
44     (ε : E → ℝ) (hε : ∀ e, ‖Δ e‖ ≤ ε e * ‖A e‖) (x : X) :
45     ‖((∑ e, (A e + Δ e)) - (∑ e, A e)) x‖ ≤
46       ∑ e, ε e * ‖A e‖ * ‖P (src e) x‖ := by
47   apply (packet_perturbation_bound P src A Δ hΔ x).trans
48   exact Finset.sum_le_sum (fun e _ => mul_le_mul_of_nonneg_right (hε e) (norm_nonneg _))
49 
50 /-- A uniform operator certificate, suitable for use in later product-chain estimates. -/
51 theorem packet_operator_perturbation_bound (P : I → X →L[K] X) (src : E → I)
52     (A Δ : E → X →L[K] X) (hΔ : ∀ e, Δ e = (Δ e).comp (P (src e))) :
53     ‖(∑ e, (A e + Δ e)) - (∑ e, A e)‖ ≤ ∑ e, ‖Δ e‖ * ‖P (src e)‖ := by
54   rw [packet_error_operator_identity P src A Δ hΔ]
55   exact (norm_sum_le _ _).trans
56     (Finset.sum_le_sum (fun e _ => ContinuousLinearMap.opNorm_comp_le _ _))
57 
58 /-- Contractive source projectors turn the local errors into a simple uniform bound. -/
59 theorem contractive_packet_operator_bound (P : I → X →L[K] X) (src : E → I)
60     (A Δ : E → X →L[K] X) (hΔ : ∀ e, Δ e = (Δ e).comp (P (src e)))
61     (hP : ∀ i, ‖P i‖ ≤ 1) :
62     ‖(∑ e, (A e + Δ e)) - (∑ e, A e)‖ ≤ ∑ e, ‖Δ e‖ := by
63   apply (packet_operator_perturbation_bound P src A Δ hΔ).trans
64   apply Finset.sum_le_sum
65   intro e _
66   simpa using mul_le_mul_of_nonneg_left (hP (src e)) (norm_nonneg (Δ e))
67 
68 end KomorebiPaperVIII
69 
70 #print axioms KomorebiPaperVIII.packet_error_operator_identity
71 #print axioms KomorebiPaperVIII.packet_error_action_identity
72 #print axioms KomorebiPaperVIII.packet_perturbation_bound
73 #print axioms KomorebiPaperVIII.packet_relative_perturbation_bound
74 #print axioms KomorebiPaperVIII.packet_operator_perturbation_bound
75 #print axioms KomorebiPaperVIII.contractive_packet_operator_bound

Back to source controls