ReleaseDefectPolynomial.lean

1 import KomorebiVerification.PaperII.TypedLinearDefects
2 
3 set_option autoImplicit false
4 namespace Komorebi.PaperII.ReleaseDefectPolynomial
5 open scoped BigOperators
6 open TypedLinearDefects
7 universe u v w
8 
9 /-- The full polynomial defect, with every coefficient retained. The zero-degree
10 summand vanishes by the all-natural-powers telescope. -/
11 theorem polynomial_defect
12     {R : Type u} [CommSemiring R]
13     {Xf : Type v} {Xc : Type w}
14     [AddCommGroup Xf] [AddCommGroup Xc] [Module R Xf] [Module R Xc]
15     (C : Xf →ₗ[R] Xc) (Tf : Module.End R Xf) (Tc : Module.End R Xc)
16     (p : Polynomial R) :
17     C.comp (polynomialAction p Tf) - (polynomialAction p Tc).comp C =
18       p.sum (fun n a => a • (∑ k ∈ Finset.range n,
19         (Tc ^ (n - 1 - k)).comp ((defect C Tf Tc).comp (Tf ^ k)))) := by
20   classical
21   calc
22     _ = p.sum (fun n a => a • (C.comp (Tf ^ n) - (Tc ^ n).comp C)) := by
23       ext x
24       simp [polynomialAction, Polynomial.sum_def, Finset.sum_sub_distrib, smul_sub]
25     _ = _ := by
26       simp only [Polynomial.sum_def]
27       apply Finset.sum_congr rfl
28       intro n hn
29       rw [power_defect_identity_all]
30 
31 /-- The same full identity in the space of bounded linear maps, without a
32 zero-defect assumption or any completeness assumption. -/
33 theorem continuous_polynomial_defect
34     {𝕜 : Type u} [NontriviallyNormedField 𝕜]
35     {Ef : Type v} {Ec : Type w}
36     [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
37     [NormedSpace 𝕜 Ef] [NormedSpace 𝕜 Ec]
38     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
39     (p : Polynomial 𝕜) :
40     C.comp (continuousPolynomialAction p Tf) -
41         (continuousPolynomialAction p Tc).comp C =
42       p.sum (fun n a => a • (∑ k ∈ Finset.range n,
43         (Tc ^ (n - 1 - k)).comp ((continuousDefect C Tf Tc).comp (Tf ^ k)))) := by
44   classical
45   calc
46     _ = p.sum (fun n a => a • (C.comp (Tf ^ n) - (Tc ^ n).comp C)) := by
47       ext x
48       simp [continuousPolynomialAction, Polynomial.sum_def,
49         Finset.sum_sub_distrib, smul_sub]
50     _ = _ := by
51       simp only [Polynomial.sum_def]
52       apply Finset.sum_congr rfl
53       intro n hn
54       rw [continuous_power_defect_identity_all]
55 
56 end Komorebi.PaperII.ReleaseDefectPolynomial

Back to source controls