SpectralPackets.lean

1 import KomorebiPaperVI.Semigroups
2 import Mathlib.Analysis.SpecialFunctions.Pow.Real
3 
4 /-! Author: Komorebi P. Finite spectral resolution, including the actual exponential bridge. -/
5 namespace KomorebiPaperVI.SpectralPackets
6 open scoped BigOperators
7 variable {I R : Type*} [Fintype I] [DecidableEq I] [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R]
8 
9 noncomputable def resolve (P : I → R) (c : I → ℝ) : R := ∑ i, c i • P i
10 
11 omit [CompleteSpace R] in
12 theorem resolve_mul (P : I → R) (h : ∀ i j, P i*P j=if i=j then P i else 0)
13     (c d : I → ℝ) : resolve P c*resolve P d=resolve P (fun i => c i*d i) := by
14   classical
15   simp only [resolve,Finset.sum_mul,Finset.mul_sum,smul_mul_smul_comm,h]
16   simp [smul_ite]
17 
18 omit [CompleteSpace R] in
19 theorem resolve_left_packet (P : I → R) (h : ∀ i j, P i*P j=if i=j then P i else 0)
20     (c : I → ℝ) (j : I) : P j*resolve P c=c j • P j := by
21   classical
22   simp [resolve,Finset.mul_sum,Algebra.mul_smul_comm,h,smul_ite]
23 
24 omit [CompleteSpace R] in
25 theorem resolve_right_packet (P : I → R) (h : ∀ i j, P i*P j=if i=j then P i else 0)
26     (c : I → ℝ) (j : I) : resolve P c*P j=c j • P j := by
27   classical
28   simp [resolve,Finset.sum_mul,Algebra.smul_mul_assoc,h,smul_ite]
29 
30 noncomputable def resolutionHom (P : I → R) (hP : ∑ i, P i=1)
31     (h : ∀ i j, P i*P j=if i=j then P i else 0) : (I → ℝ) →+* R where
32   toFun := resolve P
33   map_zero' := by simp [resolve]
34   map_one' := by simpa [resolve] using hP
35   map_add' c d := by simp [resolve,add_smul,Finset.sum_add_distrib]
36   map_mul' c d := (resolve_mul P h c d).symm
37 
38 omit [CompleteSpace R] in
39 theorem exp_resolution (P : I → R) (hP : ∑ i, P i=1)
40     (h : ∀ i j, P i*P j=if i=j then P i else 0) (c : I → ℝ) :
41     NormedSpace.exp (resolve P c)=resolve P (fun i => Real.exp (c i)) := by
42   let : NormedAlgebra ℚ R := NormedAlgebra.restrictScalars ℚ ℝ R
43   have hc : Continuous (resolutionHom P hP h) := by
44     change Continuous (resolve P)
45     unfold resolve
46     fun_prop
47   have he := NormedSpace.map_exp (resolutionHom P hP h) hc c
48   change resolve P (NormedSpace.exp c)=NormedSpace.exp (resolve P c) at he
49   simpa only [Pi.exp_def,← Real.exp_eq_exp_ℝ] using he.symm
50 
51 noncomputable def fractional (P : I → R) (lam : I → ℝ) (a : ℝ) : R :=
52   resolve P (fun i => (lam i)^a)
53 
54 noncomputable def spectralTransfer (P : I → R) (lam : I → ℝ) (a t : ℝ) : R :=
55   resolve P (fun i => Real.exp (-t*(lam i)^a))
56 
57 omit [CompleteSpace R] in
58 theorem fractional_add (P : I → R) (h : ∀ i j, P i*P j=if i=j then P i else 0)
59     (lam : I → ℝ) (hl : ∀ i, 0 ≤ lam i) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
60     fractional P lam a*fractional P lam b=fractional P lam (a+b) := by
61   unfold fractional
62   rw [resolve_mul P h]
63   congr 1
64   funext i
65   exact (Real.rpow_add' (hl i) (add_pos ha hb).ne').symm
66 
67 omit [CompleteSpace R] in
68 theorem spectral_transfer_exponential (P : I → R) (hP : ∑ i, P i=1)
69     (h : ∀ i j, P i*P j=if i=j then P i else 0) (lam : I → ℝ) (a t : ℝ) :
70     NormedSpace.exp ((-t) • fractional P lam a)=spectralTransfer P lam a t := by
71   have hs : (-t) • fractional P lam a=resolve P (fun i => -t*(lam i)^a) := by
72     simp [fractional,resolve,Finset.smul_sum,smul_smul]
73   rw [hs,exp_resolution P hP h]
74   rfl
75 
76 omit [CompleteSpace R] in
77 theorem spectral_transfer_add (P : I → R) (h : ∀ i j, P i*P j=if i=j then P i else 0)
78     (lam : I → ℝ) (a s t : ℝ) :
79     spectralTransfer P lam a s*spectralTransfer P lam a t=spectralTransfer P lam a (s+t) := by
80   unfold spectralTransfer
81   rw [resolve_mul P h]
82   congr 1
83   funext i
84   rw [← Real.exp_add]
85   congr 1
86   ring
87 
88 omit [CompleteSpace R] in
89 theorem fractional_reduces (P : I → R) (h : ∀ i j, P i*P j=if i=j then P i else 0)
90     (lam : I → ℝ) (a : ℝ) (j : I) :
91     P j*fractional P lam a=(lam j)^a • P j ∧
92       fractional P lam a*P j=(lam j)^a • P j :=
93   ⟨resolve_left_packet P h _ j,resolve_right_packet P h _ j⟩
94 
95 omit [CompleteSpace R] in
96 theorem spectral_transfer_reduces (P : I → R) (h : ∀ i j, P i*P j=if i=j then P i else 0)
97     (lam : I → ℝ) (a t : ℝ) (j : I) :
98     P j*spectralTransfer P lam a t=Real.exp (-t*(lam j)^a) • P j ∧
99       spectralTransfer P lam a t*P j=Real.exp (-t*(lam j)^a) • P j :=
100   ⟨resolve_left_packet P h _ j,resolve_right_packet P h _ j⟩
101 
102 end KomorebiPaperVI.SpectralPackets

Back to source controls