FractionalSemigroup.lean

1 import KomorebiPaperVI.Semigroups
2 import KomorebiPaperVI.BanachDefects
3 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
4 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
5 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
6 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
7 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
8 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
9 
10 /-! Author: Komorebi P. Actual positive CFC powers and their exponential contraction. -/
11 set_option backward.isDefEq.respectTransparency false
12 namespace KomorebiPaperVI.FractionalSemigroup
13 open KomorebiPaperVI.Semigroups
14 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
15 variable {R : Type*} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
16 
17 noncomputable def power (A : R) (a : ℝ) : R := CFC.rpow A a
18 
19 theorem power_nonnegative (A : R) (a : ℝ) : 0 ≤ power A a := CFC.rpow_nonneg
20 
21 theorem exponential_cfc (A : R) (hA : 0 ≤ A) (a t : ℝ) (ha : 0 < a) :
22     NormedSpace.exp ((-t) • power A a)=
23       cfc (fun x : ℝ => Real.exp (-t*x^a)) A := by
24   have hp : IsSelfAdjoint (power A a) := (power_nonnegative A a).isSelfAdjoint
25   rw [← CFC.real_exp_eq_normedSpace_exp (by cfc_tac : IsSelfAdjoint ((-t) • power A a))]
26   rw [← cfc_comp_smul (-t) Real.exp (power A a)]
27   unfold power
28   have he : CFC.rpow A a=cfc (fun x : ℝ => x^a) A := CFC.rpow_eq_cfc_real hA
29   simp only [smul_eq_mul]
30   rw [he,← cfc_comp (fun x : ℝ => Real.exp (-t*x)) (fun x : ℝ => x^a) A hA.isSelfAdjoint (by fun_prop) (Real.continuous_rpow_const ha.le).continuousOn]
31   rfl
32 
33 theorem exponential_contraction (A : R) (hA : 0 ≤ A) (a t : ℝ) (ha : 0 < a) (ht : 0 ≤ t) :
34     ‖NormedSpace.exp ((-t) • power A a)‖ ≤ 1 := by
35   rw [exponential_cfc A hA a t ha]
36   apply norm_cfc_le (by norm_num)
37   intro x hx
38   have hx0 : 0 ≤ x := by grind
39   rw [Real.norm_of_nonneg (Real.exp_pos _).le,Real.exp_le_one_iff]
40   exact mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr ht) (Real.rpow_nonneg hx0 _)
41 
42 theorem exponential_gap (A : R) (hA : 0 ≤ A) (a t m : ℝ) (ha : 0 < a)
43     (ht : 0 ≤ t) (hm : 0 ≤ m) (hgap : algebraMap ℝ R m ≤ A) :
44     ‖NormedSpace.exp ((-t) • power A a)‖ ≤ Real.exp (-t*m^a) := by
45   rw [exponential_cfc A hA a t ha]
46   apply norm_cfc_le (Real.exp_pos _).le
47   intro x hx
48   have hx : m ≤ x := (algebraMap_le_iff_le_spectrum hA.isSelfAdjoint).mp hgap x hx
49   rw [Real.norm_of_nonneg (Real.exp_pos _).le,Real.exp_le_exp]
50   exact mul_le_mul_of_nonpos_left (Real.rpow_le_rpow hm hx ha.le) (neg_nonpos.mpr ht)
51 
52 noncomputable def defect (A B C : R) (a : ℝ) : R := C*power A a-power B a*C
53 noncomputable def evolution (A : R) (a t : ℝ) : R := NormedSpace.exp ((-t) • power A a)
54 
55 theorem evolution_transfer (A : R) (a t : ℝ) : evolution A a t=transfer (-power A a) t := by
56   simp [evolution,transfer,smul_neg,neg_smul]
57 
58 theorem fractional_duhamel (A B C : R) (a t : ℝ) :
59     C*evolution A a t-evolution B a t*C=
60       -(∫ r in 0..t,evolution B a (t-r)*defect A B C a*evolution A a r) := by
61   simp only [evolution_transfer]
62   rw [BanachDefects.duhamel]
63   have he : C*(-power A a)-(-power B a)*C= -defect A B C a := by
64     simp only [defect,mul_neg,neg_mul]
65     abel
66   rw [he]
67   simp only [mul_neg,neg_mul,intervalIntegral.integral_neg]
68 
69 theorem fractional_contraction_bound (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B)
70     (a t : ℝ) (ha : 0 < a) (ht : 0 ≤ t) :
71     ‖C*evolution A a t-evolution B a t*C‖ ≤ t*‖defect A B C a‖ := by
72   simp only [evolution_transfer]
73   have h := BanachDefects.contraction_bound (-power A a) (-power B a) C t ht
74     (fun r hr => by rw [← evolution_transfer]; exact exponential_contraction A hA a r ha hr)
75     (fun r hr => by rw [← evolution_transfer]; exact exponential_contraction B hB a r ha hr)
76   have he : C*(-power A a)-(-power B a)*C= -defect A B C a := by
77     simp only [defect,mul_neg,neg_mul]
78     abel
79   simpa only [he,norm_neg] using h
80 
81 theorem fractional_gap_bound (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B)
82     (a t m : ℝ) (ha : 0 < a) (ht : 0 ≤ t) (hm : 0 ≤ m)
83     (hgA : algebraMap ℝ R m ≤ A) (hgB : algebraMap ℝ R m ≤ B) :
84     ‖C*evolution A a t-evolution B a t*C‖ ≤ t*Real.exp (-t*m^a)*‖defect A B C a‖ := by
85   rw [fractional_duhamel,norm_neg]
86   have hc : Continuous (fun r => evolution B a (t-r)*defect A B C a*evolution A a r) := by
87     simp only [evolution_transfer]
88     fun_prop
89   calc
90     _ ≤ ∫ r in 0..t,‖evolution B a (t-r)*defect A B C a*evolution A a r‖ :=
91       intervalIntegral.norm_integral_le_integral_norm ht
92     _ ≤ ∫ _ in 0..t,Real.exp (-t*m^a)*‖defect A B C a‖ := by
93       apply intervalIntegral.integral_mono_on ht (hc.norm.intervalIntegrable 0 t) intervalIntegrable_const
94       intro r hr
95       calc
96         _ ≤ ‖evolution B a (t-r)‖*‖defect A B C a‖*‖evolution A a r‖ :=
97           norm_mul_le_of_le (norm_mul_le _ _) le_rfl
98         _ ≤ Real.exp (-(t-r)*m^a)*‖defect A B C a‖*Real.exp (-r*m^a) := by
99           gcongr
100           · exact exponential_gap B hB a (t-r) m ha (by linarith [hr.2]) hm hgB
101           · exact exponential_gap A hA a r m ha hr.1 hm hgA
102         _ = _ := by
103           rw [mul_right_comm,← Real.exp_add]
104           congr 2
105           ring
106     _ = _ := by
107       simp only [intervalIntegral.integral_const,sub_zero,smul_eq_mul]
108       ring
109 
110 end KomorebiPaperVI.FractionalSemigroup

Back to source controls