KnownEdge.lean

1 import Mathlib.Analysis.Normed.Group.Basic
2 import Mathlib.Tactic
3 
4 /-!
5 Author: Komorebi P.
6 Checked source. Theorem 6.1 and Corollary 6.2 at their
7 algebraic/normed-group level. No edge-discovery or Lp mask theorem is asserted.
8 -/
9 
10 open scoped BigOperators
11 
12 namespace KomorebiPaperV
13 
14 section Algebra
15 variable {E : Type*} [AddCommGroup E]
16 
17 theorem known_edge_error (s j : E) (Q : E → E) :
18     (s + j) - (Q s + j) = s - Q s := by
19   abel
20 
21 theorem estimated_edge_error (s shat j jhat : E) :
22     (s + j) - (shat + jhat) = (s - shat) + (j - jhat) := by
23   abel
24 
25 theorem several_known_edges_error {A : Type*} (t : Finset A)
26     (s : E) (j : A → E) (Q : E → E) :
27     (s + ∑ a ∈ t, j a) - (Q s + ∑ a ∈ t, j a) = s - Q s := by
28   exact known_edge_error s (∑ a ∈ t, j a) Q
29 end Algebra
30 
31 section Norms
32 variable {E : Type*} [SeminormedAddCommGroup E]
33 
34 theorem known_edge_norm (s j : E) (Q : E → E) :
35     ‖(s + j) - (Q s + j)‖ = ‖s - Q s‖ := by
36   rw [known_edge_error]
37 
38 theorem several_known_edges_norm {A : Type*} (t : Finset A)
39     (s : E) (j : A → E) (Q : E → E) :
40     ‖(s + ∑ a ∈ t, j a) - (Q s + ∑ a ∈ t, j a)‖ = ‖s - Q s‖ := by
41   rw [several_known_edges_error]
42 
43 theorem estimated_edge_norm_bound (s shat j jhat : E) :
44     ‖(s + j) - (shat + jhat)‖ ≤ ‖s - shat‖ + ‖j - jhat‖ := by
45   rw [estimated_edge_error]
46   exact norm_add_le _ _
47 end Norms
48 
49 end KomorebiPaperV

Back to source controls