PositiveResolvent.lean

1 import KomorebiPaperVI.FractionalSemigroup
2 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
3 
4 /-! Author: Komorebi P. Literal positive resolvents and their operator norm bounds. -/
5 namespace KomorebiPaperVI.PositiveResolvent
6 open Set
7 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
8 set_option backward.isDefEq.respectTransparency false
9 variable {R : Type*} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
10 
11 noncomputable def resolvent (A : R) (t : ℝ) : R := cfc (fun x : ℝ => (t+x)⁻¹) A
12 
13 theorem spectral_positive (A : R) (hA : 0 ≤ A) (t : ℝ) (ht : 0 < t)
14     (x : ℝ) (hx : x∈spectrum ℝ A) : 0 < t+x := by
15   have hx0 : 0 ≤ x := spectrum_nonneg_of_nonneg hA hx
16   linarith
17 
18 theorem resolvent_inverse (A : R) (hA : 0 ≤ A) (t : ℝ) (ht : 0 < t) :
19     resolvent A t=Ring.inverse (algebraMap ℝ R t+A) := by
20   unfold resolvent
21   rw [cfc_inv (fun x : ℝ => t+x) A (fun x hx => (spectral_positive A hA t ht x hx).ne')]
22   rw [cfc_add A (fun _ : ℝ => t) (fun x : ℝ => x),cfc_const t A,cfc_id' (R := ℝ) (a := A) hA.isSelfAdjoint]
23 
24 theorem resolvent_left_inverse (A : R) (hA : 0 ≤ A) (t : ℝ) (ht : 0 < t) :
25     (algebraMap ℝ R t+A)*resolvent A t=1 := by
26   have hc : ContinuousOn (fun x : ℝ => (t+x)⁻¹) (spectrum ℝ A) := by
27     apply ContinuousOn.inv₀ (by fun_prop)
28     exact fun x hx => (spectral_positive A hA t ht x hx).ne'
29   have he : algebraMap ℝ R t+A=cfc (fun x : ℝ => t+x) A := by
30     rw [cfc_add A (fun _ : ℝ => t) (fun x : ℝ => x),cfc_const t A,cfc_id' (R := ℝ) (a := A) hA.isSelfAdjoint]
31   rw [he,resolvent,← cfc_mul (fun x : ℝ => t+x) (fun x : ℝ => (t+x)⁻¹) A (by fun_prop) hc]
32   rw [← cfc_const_one ℝ A]
33   apply cfc_congr
34   intro x hx
35   exact mul_inv_cancel₀ (spectral_positive A hA t ht x hx).ne'
36 
37 theorem resolvent_right_inverse (A : R) (hA : 0 ≤ A) (t : ℝ) (ht : 0 < t) :
38     resolvent A t*(algebraMap ℝ R t+A)=1 := by
39   have he : algebraMap ℝ R t+A=cfc (fun x : ℝ => t+x) A := by
40     rw [cfc_add A (fun _ : ℝ => t) (fun x : ℝ => x),cfc_const t A,cfc_id' (R := ℝ) (a := A) hA.isSelfAdjoint]
41   have h := resolvent_left_inverse A hA t ht
42   rw [he] at h ⊢
43   exact (cfc_commute_cfc (fun x : ℝ => (t+x)⁻¹) (fun x : ℝ => t+x) A).eq.trans h
44 
45 theorem resolvent_gap_norm (A : R) (hA : 0 ≤ A) (t m : ℝ) (ht : 0 < t) (hm : 0 ≤ m)
46     (hg : algebraMap ℝ R m ≤ A) : ‖resolvent A t‖ ≤ (t+m)⁻¹ := by
47   apply norm_cfc_le (by positivity)
48   intro x hx
49   have hmx : m ≤ x := (algebraMap_le_iff_le_spectrum hA.isSelfAdjoint).mp hg x hx
50   rw [Real.norm_of_nonneg (inv_nonneg.mpr (spectral_positive A hA t ht x hx).le)]
51   exact inv_anti₀ (by positivity) (by linarith)
52 
53 theorem resolvent_norm (A : R) (hA : 0 ≤ A) (t : ℝ) (ht : 0 < t) :
54     ‖resolvent A t‖ ≤ t⁻¹ := by
55   simpa using resolvent_gap_norm A hA t 0 ht le_rfl (by simpa using hA)
56 
57 theorem resolvent_defect (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B) (t : ℝ) (ht : 0 < t) :
58     resolvent B t*C-C*resolvent A t=resolvent B t*(C*A-B*C)*resolvent A t := by
59   have hAinv := resolvent_left_inverse A hA t ht
60   have hBinv := resolvent_right_inverse B hB t ht
61   have hc := Algebra.commutes (R := ℝ) (A := R) t C
62   have hm : C*A-B*C=C*(algebraMap ℝ R t+A)-(algebraMap ℝ R t+B)*C := by
63     simp only [mul_add,add_mul,hc]
64     abel
65   rw [hm]
66   calc
67     _ = resolvent B t*C*((algebraMap ℝ R t+A)*resolvent A t)-
68           (resolvent B t*(algebraMap ℝ R t+B))*C*resolvent A t := by rw [hAinv,hBinv]; simp
69     _ = _ := by noncomm_ring
70 
71 theorem saturation_cfc (A : R) (hA : 0 ≤ A) (t : ℝ) (ht : 0 < t) :
72     A*resolvent A t=cfc (fun x : ℝ => x*(t+x)⁻¹) A := by
73   have hc : ContinuousOn (fun x : ℝ => (t+x)⁻¹) (spectrum ℝ A) := by
74     apply ContinuousOn.inv₀ (by fun_prop)
75     exact fun x hx => (spectral_positive A hA t ht x hx).ne'
76   rw [cfc_mul (fun x : ℝ => x) (fun x : ℝ => (t+x)⁻¹) A (by fun_prop) hc,cfc_id' ℝ A hA.isSelfAdjoint]
77   rfl
78 
79 theorem saturation_norm (A : R) (hA : 0 ≤ A) (t : ℝ) (ht : 0 < t) :
80     ‖A*resolvent A t‖ ≤ 1 := by
81   rw [saturation_cfc A hA t ht]
82   apply norm_cfc_le zero_le_one
83   intro x hx
84   have hx0 : 0 ≤ x := spectrum_nonneg_of_nonneg hA hx
85   rw [Real.norm_of_nonneg (mul_nonneg hx0 (inv_nonneg.mpr (spectral_positive A hA t ht x hx).le)),← div_eq_mul_inv]
86   exact (div_le_one (spectral_positive A hA t ht x hx)).mpr (by linarith)
87 
88 end KomorebiPaperVI.PositiveResolvent

Back to source controls