RectangularSemigroup.lean

1 import KomorebiPaperVI.ComplexSemigroups
2 
3 /-! Author: Komorebi P. Fractional semigroup refinement between distinct Hilbert spaces. -/
4 namespace KomorebiPaperVI.RectangularSemigroup
5 open Set MeasureTheory
6 open scoped NNReal
7 open KomorebiPaperVI.RectangularFractional KomorebiPaperVI.Semigroups
8 set_option backward.isDefEq.respectTransparency false
9 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
10 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
11     [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
12 
13 noncomputable def evolution (A : E →L[ℂ] E) (p : ℝ≥0) (t : ℝ) : E →L[ℂ] E :=
14   transfer (-power A p) t
15 
16 noncomputable def timeDefect (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F)
17     (p : ℝ≥0) (t : ℝ) : E →L[ℂ] F := C.comp (evolution A p t)-(evolution B p t).comp C
18 
19 theorem evolution_exponential (A : E →L[ℂ] E) (p : ℝ≥0) (t : ℝ) :
20     evolution A p t=NormedSpace.exp ((-t) • power A p) := by
21   simp [evolution,transfer,smul_neg,neg_smul]
22 
23 theorem evolution_cfc (A : E →L[ℂ] E) (p : ℝ≥0) (hp : 0 < p) (t : ℝ) :
24     evolution A p t=FractionalSemigroup.evolution A p t := by
25   rw [evolution_exponential]
26   unfold power FractionalSemigroup.evolution FractionalSemigroup.power
27   congr 2
28   exact CFC.nnrpow_eq_rpow hp
29 
30 theorem contraction (A : E →L[ℂ] E) (hA : 0 ≤ A) (p : ℝ≥0) (hp : 0 < p)
31     (t : ℝ) (ht : 0 ≤ t) : ‖evolution A p t‖ ≤ 1 := by
32   rw [evolution_cfc A p hp t]
33   exact FractionalSemigroup.exponential_contraction A hA p t hp ht
34 
35 theorem gap_decay (A : E →L[ℂ] E) (hA : 0 ≤ A) (p : ℝ≥0) (hp : 0 < p)
36     (t m : ℝ) (ht : 0 ≤ t) (hm : 0 ≤ m) (hgA : algebraMap ℝ (E →L[ℂ] E) m ≤ A) :
37     ‖evolution A p t‖ ≤ Real.exp (-t*m^(p:ℝ)) := by
38   rw [evolution_cfc A p hp t]
39   exact FractionalSemigroup.exponential_gap A hA p t m hp ht hm hgA
40 
41 theorem fractional_duhamel (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F)
42     (p : ℝ≥0) (t : ℝ) :
43     timeDefect A B C p t= -(∫ r in 0..t,(evolution B p (t-r)).comp
44       ((fractionalDefect A B C p).comp (evolution A p r))) := by
45   unfold timeDefect evolution
46   rw [ComplexSemigroups.duhamel_rectangular]
47   have he : C.comp (-power A p)-(-power B p).comp C= -fractionalDefect A B C p := by
48     simp only [fractionalDefect,ContinuousLinearMap.comp_neg,ContinuousLinearMap.neg_comp]
49     abel
50   rw [he]
51   simp only [ContinuousLinearMap.neg_comp,ContinuousLinearMap.comp_neg,intervalIntegral.integral_neg]
52 
53 theorem fractional_contraction_bound (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F)
54     (hA : 0 ≤ A) (hB : 0 ≤ B) (p : ℝ≥0) (hp : 0 < p) (t : ℝ) (ht : 0 ≤ t) :
55     ‖timeDefect A B C p t‖ ≤ t*‖fractionalDefect A B C p‖ := by
56   have h := ComplexSemigroups.contraction_duhamel_bound (-power A p) (-power B p) C t ht
57     (fun r hr => contraction A hA p hp r hr) (fun r hr => contraction B hB p hp r hr)
58   have he : C.comp (-power A p)-(-power B p).comp C= -fractionalDefect A B C p := by
59     simp only [fractionalDefect,ContinuousLinearMap.comp_neg,ContinuousLinearMap.neg_comp]
60     abel
61   simpa only [timeDefect,evolution,he,norm_neg] using h
62 
63 theorem fractional_gap_bound (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F)
64     (hA : 0 ≤ A) (hB : 0 ≤ B) (p : ℝ≥0) (hp : 0 < p) (t m : ℝ) (ht : 0 ≤ t) (hm : 0 ≤ m)
65     (hgA : algebraMap ℝ (E →L[ℂ] E) m ≤ A) (hgB : algebraMap ℝ (F →L[ℂ] F) m ≤ B) :
66     ‖timeDefect A B C p t‖ ≤ t*Real.exp (-t*m^(p:ℝ))*‖fractionalDefect A B C p‖ := by
67   rw [fractional_duhamel,norm_neg]
68   have hc : Continuous (fun r => (evolution B p (t-r)).comp
69       ((fractionalDefect A B C p).comp (evolution A p r))) := by
70     unfold evolution
71     fun_prop
72   calc
73     _ ≤ ∫ r in 0..t,‖(evolution B p (t-r)).comp ((fractionalDefect A B C p).comp (evolution A p r))‖ :=
74       intervalIntegral.norm_integral_le_integral_norm ht
75     _ ≤ ∫ _ in 0..t,Real.exp (-t*m^(p:ℝ))*‖fractionalDefect A B C p‖ := by
76       apply intervalIntegral.integral_mono_on ht (hc.norm.intervalIntegrable 0 t) intervalIntegrable_const
77       intro r hr
78       calc
79         _ ≤ ‖evolution B p (t-r)‖*(‖fractionalDefect A B C p‖*‖evolution A p r‖) :=
80           (ContinuousLinearMap.opNorm_comp_le _ _).trans
81             (mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _))
82         _ ≤ Real.exp (-(t-r)*m^(p:ℝ))*(‖fractionalDefect A B C p‖*Real.exp (-r*m^(p:ℝ))) := by
83           gcongr
84           · exact gap_decay B hB p hp (t-r) m (by linarith [hr.2]) hm hgB
85           · exact gap_decay A hA p hp r m hr.1 hm hgA
86         _ = _ := by
87           rw [← mul_assoc,mul_right_comm,← Real.exp_add]
88           congr 2
89           ring
90     _ = _ := by
91       simp only [intervalIntegral.integral_const,sub_zero,smul_eq_mul]
92       ring
93 
94 theorem generator_gap_bound (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F)
95     (hA : 0 ≤ A) (hB : 0 ≤ B) (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1) (t m : ℝ) (ht : 0 ≤ t) (hm : 0 < m)
96     (hgA : algebraMap ℝ (E →L[ℂ] E) m ≤ A) (hgB : algebraMap ℝ (F →L[ℂ] F) m ≤ B) :
97     ‖timeDefect A B C p t‖ ≤ t*Real.exp (-t*m^(p:ℝ))*(p:ℝ)*m^((p:ℝ)-1)*‖defect A B C‖ := by
98   calc
99     _ ≤ t*Real.exp (-t*m^(p:ℝ))*‖fractionalDefect A B C p‖ :=
100       fractional_gap_bound A B C hA hB p hp.1 t m ht hm.le hgA hgB
101     _ ≤ t*Real.exp (-t*m^(p:ℝ))*((p:ℝ)*m^((p:ℝ)-1)*‖defect A B C‖) :=
102       mul_le_mul_of_nonneg_left (common_gap_estimate p hp m hm A B C hA hB hgA hgB) (by positivity)
103     _ = _ := by ring
104 
105 end KomorebiPaperVI.RectangularSemigroup

Back to source controls