FractionalResolvent.lean

1 import KomorebiPaperVI.NormalizedFractional
2 import KomorebiPaperVI.PositiveResolvent
3 
4 /-! Author: Komorebi P. The actual normalized fractional resolvent-defect integral. -/
5 namespace KomorebiPaperVI.FractionalResolvent
6 open Set MeasureTheory Real
7 open KomorebiPaperVI.PositiveResolvent KomorebiPaperVI.NormalizedFractional
8 open scoped NNReal
9 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
10 set_option backward.isDefEq.respectTransparency false
11 variable {R : Type*} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
12 
13 theorem cfc_integrand (p t : ℝ) (hp : p∈Ioo 0 1) (ht : 0 < t) (A : R) (hA : 0 ≤ A) :
14     cfcₙ (rpowIntegrand₀₁ p t) A=t^p • (algebraMap ℝ R t⁻¹-PositiveResolvent.resolvent A t) := by
15   have hc : ContinuousOn (fun x : ℝ => (t+x)⁻¹) (spectrum ℝ A) := by
16     apply ContinuousOn.inv₀ (by fun_prop)
17     exact fun x hx => (spectral_positive A hA t ht x hx).ne'
18   rw [cfcₙ_eq_cfc (hf := (continuousOn_rpowIntegrand₀₁_Ici hp ht).mono (by grind)) (hf0 := by simp)]
19   unfold rpowIntegrand₀₁
20   change cfc (fun x : ℝ => t^p • (t⁻¹-(t+x)⁻¹)) A= _
21   rw [cfc_smul (t^p) (fun x : ℝ => t⁻¹-(t+x)⁻¹) A ((continuous_const.continuousOn).sub hc),
22     cfc_sub (fun _ : ℝ => t⁻¹) (fun x : ℝ => (t+x)⁻¹) A (by fun_prop) hc,
23     cfc_const t⁻¹ A hA.isSelfAdjoint]
24   rfl
25 
26 theorem integrand_defect (p t : ℝ) (hp : p∈Ioo 0 1) (ht : 0 < t)
27     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B) :
28     C*cfcₙ (rpowIntegrand₀₁ p t) A-cfcₙ (rpowIntegrand₀₁ p t) B*C=
29       t^p • (PositiveResolvent.resolvent B t*(C*A-B*C)*PositiveResolvent.resolvent A t) := by
30   rw [cfc_integrand p t hp ht A hA,cfc_integrand p t hp ht B hB]
31   rw [Algebra.mul_smul_comm,Algebra.smul_mul_assoc,← smul_sub]
32   congr 1
33   rw [← resolvent_defect A B C hA hB t ht]
34   have hc := Algebra.commutes (R := ℝ) (A := R) t⁻¹ C
35   simp only [mul_sub,sub_mul,hc]
36   abel
37 
38 theorem normalized_defect (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
39     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B) :
40     IntegrableOn (fun t => t^(p:ℝ) • (PositiveResolvent.resolvent B t*(C*A-B*C)*PositiveResolvent.resolvent A t)) (Ioi 0) ∧
41       C*CFC.nnrpow A p-CFC.nnrpow B p*C=coefficient p •
42         ∫ t in Ioi 0,t^(p:ℝ) • (PositiveResolvent.resolvent B t*(C*A-B*C)*PositiveResolvent.resolvent A t) := by
43   have hiA := cfc_lebesgue_integral p hp A hA
44   have hiB := cfc_lebesgue_integral p hp B hB
45   have hl : IntegrableOn (fun t => C*cfcₙ (rpowIntegrand₀₁ p t) A) (Ioi 0) :=
46     (ContinuousLinearMap.mul ℝ R C).integrable_comp hiA.1
47   have hr : IntegrableOn (fun t => cfcₙ (rpowIntegrand₀₁ p t) B*C) (Ioi 0) :=
48     (ContinuousLinearMap.mul ℝ R).flip C |>.integrable_comp hiB.1
49   have hd := hl.sub hr
50   have he : EqOn (fun t => C*cfcₙ (rpowIntegrand₀₁ p t) A-cfcₙ (rpowIntegrand₀₁ p t) B*C)
51       (fun t => t^(p:ℝ) • (PositiveResolvent.resolvent B t*(C*A-B*C)*PositiveResolvent.resolvent A t)) (Ioi 0) :=
52     fun t ht => integrand_defect p t hp ht A B C hA hB
53   constructor
54   · exact (integrableOn_congr_fun he measurableSet_Ioi).mp hd
55   · rw [← setIntegral_congr_fun measurableSet_Ioi he,integral_sub hl hr,
56       integral_const_mul_of_integrable hiA.1,integral_mul_const_of_integrable hiB.1,
57       hiA.2,hiB.2,Algebra.mul_smul_comm,Algebra.smul_mul_assoc,smul_sub]
58 
59 theorem exact_fractional_intertwining (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
60     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B) (h : C*A=B*C) :
61     C*CFC.nnrpow A p=CFC.nnrpow B p*C := by
62   have he := (normalized_defect p hp A B C hA hB).2
63   simp only [h,sub_self,mul_zero,zero_mul,smul_zero,integral_zero] at he
64   exact sub_eq_zero.mp he
65 
66 end KomorebiPaperVI.FractionalResolvent

Back to source controls