CanonicalJets.lean

1 import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
2 import Mathlib.Algebra.DirectSum.Decomposition
3 import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
4 import Mathlib.Analysis.Complex.Polynomial.Basic
5 
6 /-! Author: Komorebi P. Canonical finite-dimensional matrix functions from Taylor jets. -/
7 namespace KomorebiPaperVI.CanonicalJets
8 open Module
9 set_option backward.isDefEq.respectTransparency false
10 variable {V W : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
11   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
12 
13 noncomputable instance decomposition (A : End ℂ V) :
14     DirectSum.Decomposition A.maxGenEigenspace := by
15   classical
16   exact (DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
17     A.independent_maxGenEigenspace A.iSup_maxGenEigenspace_eq_top).chooseDecomposition
18 
19 noncomputable def jet (A : End ℂ V) (a : ℂ → ℕ → ℂ) (μ : ℂ) (n : ℕ) : End ℂ V :=
20   ∑ k ∈ Finset.range n, a μ k • (A-μ • 1)^k
21 
22 noncomputable def calculus (A : End ℂ V) (a : ℂ → ℕ → ℂ) : End ℂ V := by
23   classical
24   exact (DirectSum.toModule ℂ ℂ V (fun μ =>
25     (jet A a μ (finrank ℂ V)).comp (A.maxGenEigenspace μ).subtype)).comp
26     (DirectSum.decomposeLinearEquiv A.maxGenEigenspace).toLinearMap
27 
28 theorem calculus_on_component (A : End ℂ V) (a : ℂ → ℕ → ℂ) (μ : ℂ)
29     (x : V) (hx : x ∈ A.maxGenEigenspace μ) :
30     calculus A a x=jet A a μ (finrank ℂ V) x := by
31   classical
32   unfold calculus
33   dsimp only [LinearMap.comp_apply,LinearEquiv.coe_toLinearMap]
34   rw [DirectSum.decomposeLinearEquiv_apply_coe A.maxGenEigenspace μ ⟨x,hx⟩,
35     DirectSum.toModule_lof]
36   rfl
37 
38 theorem power_kills (A : End ℂ V) (μ : ℂ) (x : V)
39     (hx : x ∈ A.maxGenEigenspace μ) (k : ℕ) (hk : finrank ℂ V ≤ k) :
40     ((A-μ • 1)^k) x=0 := by
41   have h := A.genEigenspace_le_genEigenspace_finrank μ ⊤ hx
42   have h' : x ∈ A.genEigenspace μ k :=
43     (A.genEigenspace μ).monotone (by exact_mod_cast hk) h
44   exact LinearMap.mem_ker.mp (Module.End.mem_genEigenspace_nat.mp h')
45 
46 theorem jet_stable (A : End ℂ V) (a : ℂ → ℕ → ℂ) (μ : ℂ) (x : V)
47     (hx : x ∈ A.maxGenEigenspace μ) (n : ℕ) (hn : finrank ℂ V ≤ n) :
48     jet A a μ n x=jet A a μ (finrank ℂ V) x := by
49   classical
50   unfold jet
51   simp only [LinearMap.sum_apply,LinearMap.smul_apply]
52   symm
53   apply Finset.sum_subset (Finset.range_mono hn)
54   intro k _ hk
55   rw [power_kills A μ x hx k (by simpa using hk),smul_zero]
56 
57 omit [FiniteDimensional ℂ V] [FiniteDimensional ℂ W] in
58 theorem shift_intertwines (A : End ℂ V) (B : End ℂ W) (C : V →ₗ[ℂ] W)
59     (h : B.comp C=C.comp A) (μ : ℂ) (x : V) :
60     C ((A-μ • 1) x)=(B-μ • 1) (C x) := by
61   have hh := LinearMap.congr_fun h x
62   simpa using hh.symm
63 
64 omit [FiniteDimensional ℂ V] [FiniteDimensional ℂ W] in
65 theorem power_intertwines (A : End ℂ V) (B : End ℂ W) (C : V →ₗ[ℂ] W)
66     (h : B.comp C=C.comp A) (μ : ℂ) (k : ℕ) (x : V) :
67     C (((A-μ • 1)^k) x)=((B-μ • 1)^k) (C x) := by
68   induction k generalizing x with
69   | zero => simp
70   | succ k ih =>
71     rw [pow_succ',pow_succ',Module.End.mul_apply,Module.End.mul_apply,
72       shift_intertwines A B C h μ,ih]
73 
74 omit [FiniteDimensional ℂ V] [FiniteDimensional ℂ W] in
75 theorem jet_intertwines (A : End ℂ V) (B : End ℂ W) (C : V →ₗ[ℂ] W)
76     (h : B.comp C=C.comp A) (a : ℂ → ℕ → ℂ) (μ : ℂ) (n : ℕ) (x : V) :
77     C (jet A a μ n x)=jet B a μ n (C x) := by
78   simp only [jet,LinearMap.sum_apply,LinearMap.smul_apply,map_sum,map_smul,
79     power_intertwines A B C h μ]
80 
81 theorem canonical_naturality (A : End ℂ V) (B : End ℂ W) (C : V →ₗ[ℂ] W)
82     (h : B.comp C=C.comp A) (a : ℂ → ℕ → ℂ) :
83     C.comp (calculus A a)=(calculus B a).comp C := by
84   apply DirectSum.decompose_lhom_ext A.maxGenEigenspace
85   intro μ
86   ext x
87   have hx := Module.End.mapsTo_genEigenspace_of_comp C h μ ⊤ x.property
88   change C (calculus A a x)=calculus B a (C x)
89   rw [calculus_on_component A a μ x x.property,
90     calculus_on_component B a μ (C x) hx,
91     ← jet_stable A a μ x x.property (max (finrank ℂ V) (finrank ℂ W)) (le_max_left _ _),
92     ← jet_stable B a μ (C x) hx (max (finrank ℂ V) (finrank ℂ W)) (le_max_right _ _)]
93   exact jet_intertwines A B C h a μ _ x
94 
95 noncomputable def holomorphic (A : End ℂ V) (f : ℂ → ℂ) : End ℂ V :=
96   calculus A (fun μ k => iteratedDeriv k f μ / k.factorial)
97 
98 theorem holomorphic_naturality (A : End ℂ V) (B : End ℂ W) (C : V →ₗ[ℂ] W)
99     (h : B.comp C=C.comp A) (f : ℂ → ℂ) :
100     C.comp (holomorphic A f)=(holomorphic B f).comp C :=
101   canonical_naturality A B C h _
102 
103 end KomorebiPaperVI.CanonicalJets

Back to source controls