FractionalNormBounds.lean

1 import KomorebiPaperVI.FractionalResolvent
2 import KomorebiPaperVI.FractionalScalarBounds
3 
4 /-! Author: Komorebi P. Norm estimates for the actual fractional resolvent defect. -/
5 namespace KomorebiPaperVI.FractionalNormBounds
6 open Set MeasureTheory Real
7 open KomorebiPaperVI.PositiveResolvent KomorebiPaperVI.NormalizedFractional KomorebiPaperVI.FractionalResolvent
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 noncomputable def integrand (p t : ℝ) (A B C : R) : R :=
14   t^p • (PositiveResolvent.resolvent B t*(C*A-B*C)*PositiveResolvent.resolvent A t)
15 
16 theorem integrand_saturation (p t : ℝ) (hp : p∈Ioo 0 1) (ht : 0 < t) (A : R) (hA : 0 ≤ A) :
17     cfcₙ (rpowIntegrand₀₁ p t) A=t^(p-1) • (A*PositiveResolvent.resolvent A t) := by
18   have hc : ContinuousOn (fun x : ℝ => (t+x)⁻¹) (spectrum ℝ A) := by
19     apply ContinuousOn.inv₀ (by fun_prop)
20     exact fun x hx => (spectral_positive A hA t ht x hx).ne'
21   rw [cfcₙ_eq_cfc (hf := (continuousOn_rpowIntegrand₀₁_Ici hp ht).mono (by grind)) (hf0 := by simp)]
22   have he : cfc (rpowIntegrand₀₁ p t) A=cfc (fun x : ℝ => t^(p-1) • (x*(t+x)⁻¹)) A := by
23     apply cfc_congr
24     intro x hx
25     rw [rpowIntegrand₀₁_eq_pow_div hp ht.le (spectrum_nonneg_of_nonneg hA hx)]
26     simp only [smul_eq_mul,div_eq_mul_inv,mul_assoc]
27   rw [he,cfc_smul (t^(p-1)) (fun x : ℝ => x*(t+x)⁻¹) A ((continuous_id.continuousOn).mul hc),← saturation_cfc A hA t ht]
28 
29 theorem integrand_low_bound (p t : ℝ) (hp : p∈Ioo 0 1) (ht : 0 < t)
30     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B) : ‖integrand p t A B C‖ ≤ 2*‖C‖*t^(p-1) := by
31   rw [integrand,← integrand_defect p t hp ht A B C hA hB,
32     integrand_saturation p t hp ht A hA,integrand_saturation p t hp ht B hB,
33     Algebra.mul_smul_comm,Algebra.smul_mul_assoc,← smul_sub,norm_smul,
34     Real.norm_of_nonneg (Real.rpow_nonneg ht.le _)]
35   have ha := saturation_norm A hA t ht
36   have hb := saturation_norm B hB t ht
37   calc
38     _ ≤ t^(p-1)*(‖C‖*‖A*PositiveResolvent.resolvent A t‖+‖B*PositiveResolvent.resolvent B t‖*‖C‖) := by
39       gcongr
40       exact (norm_sub_le _ _).trans (add_le_add (norm_mul_le _ _) (norm_mul_le _ _))
41     _ ≤ t^(p-1)*(‖C‖*1+1*‖C‖) := by gcongr
42     _ = _ := by ring
43 
44 theorem integrand_gap_bound (p t m : ℝ) (ht : 0 < t) (hm : 0 ≤ m)
45     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B)
46     (hgA : algebraMap ℝ R m ≤ A) (hgB : algebraMap ℝ R m ≤ B) :
47     ‖integrand p t A B C‖ ≤ ‖C*A-B*C‖*(t^p/(t+m)^2) := by
48   rw [integrand,norm_smul,Real.norm_of_nonneg (Real.rpow_nonneg ht.le _)]
49   calc
50     _ ≤ t^p*(‖PositiveResolvent.resolvent B t‖*‖C*A-B*C‖*‖PositiveResolvent.resolvent A t‖) := by
51       gcongr
52       exact norm_mul_le_of_le (norm_mul_le _ _) le_rfl
53     _ ≤ t^p*((t+m)⁻¹*‖C*A-B*C‖*(t+m)⁻¹) := by
54       gcongr
55       · exact resolvent_gap_norm B hB t m ht hm hgB
56       · exact resolvent_gap_norm A hA t m ht hm hgA
57     _ = _ := by
58       have htm : t+m ≠ 0 := ne_of_gt (add_pos_of_pos_of_nonneg ht hm)
59       field_simp [htm]
60 
61 theorem integrand_high_bound (p t : ℝ) (ht : 0 < t)
62     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B) :
63     ‖integrand p t A B C‖ ≤ ‖C*A-B*C‖*t^(p-2) := by
64   have h := integrand_gap_bound p t 0 ht le_rfl A B C hA hB (by simpa using hA) (by simpa using hB)
65   simpa only [add_zero,Real.rpow_sub ht,Real.rpow_two] using h
66 
67 theorem common_gap_estimate (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1) (m : ℝ) (hm : 0 < m)
68     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B)
69     (hgA : algebraMap ℝ R m ≤ A) (hgB : algebraMap ℝ R m ≤ B) :
70     ‖C*CFC.nnrpow A p-CFC.nnrpow B p*C‖ ≤ (p:ℝ)*m^((p:ℝ)-1)*‖C*A-B*C‖ := by
71   have hd := normalized_defect p hp A B C hA hB
72   have hk : 0 < coefficient p := BetaNormalization.sine_factor_positive p hp
73   have hs : 0 < Real.sin (Real.pi*(p:ℝ)) := by
74     apply Real.sin_pos_of_pos_of_lt_pi
75     · exact mul_pos Real.pi_pos hp.1
76     · nlinarith [Real.pi_pos,hp.2]
77   have hg : IntegrableOn (fun t : ℝ => t^(p:ℝ)/(t+m)^2) (Ioi 0) := by
78     by_contra hn
79     have hz := integral_undef hn
80     rw [BetaNormalization.gap_integral p m hp hm] at hz
81     exact (mul_pos (Real.rpow_pos_of_pos hm _) (div_pos (mul_pos hp.1 Real.pi_pos) hs)).ne' hz
82   rw [hd.2,norm_smul,Real.norm_of_nonneg hk.le]
83   calc
84     _ ≤ coefficient p*(∫ t in Ioi 0,‖integrand p t A B C‖) := by
85       apply mul_le_mul_of_nonneg_left (norm_integral_le_integral_norm _) hk.le
86     _ ≤ coefficient p*(∫ t in Ioi 0,‖C*A-B*C‖*(t^(p:ℝ)/(t+m)^2)) := by
87       apply mul_le_mul_of_nonneg_left _ hk.le
88       apply setIntegral_mono_on hd.1.norm (hg.const_mul _) measurableSet_Ioi
89       intro t ht
90       exact integrand_gap_bound p t m ht hm.le A B C hA hB hgA hgB
91     _ = _ := by
92       rw [integral_const_mul,mul_left_comm,coefficient,BetaNormalization.normalized_gap_integral p m hp hm]
93       ring
94 
95 noncomputable def holderConstant (p : ℝ) : ℝ := 2^(1-p)*coefficient p/(p*(1-p))
96 
97 theorem holder_estimate (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
98     (A B C : R) (hA : 0 ≤ A) (hB : 0 ≤ B) :
99     ‖C*CFC.nnrpow A p-CFC.nnrpow B p*C‖ ≤
100       holderConstant p*‖C‖^(1-(p:ℝ))*‖C*A-B*C‖^(p:ℝ) := by
101   by_cases hc : C=0
102   · subst C
103     simp [Real.zero_rpow hp.1.ne']
104   by_cases hd : C*A-B*C=0
105   · have he := exact_fractional_intertwining p hp A B C hA hB (sub_eq_zero.mp hd)
106     rw [he,sub_self,norm_zero,hd]
107     simp [Real.zero_rpow hp.1.ne']
108   have hcn : 0 < ‖C‖ := norm_pos_iff.mpr hc
109   have hdn : 0 < ‖C*A-B*C‖ := norm_pos_iff.mpr hd
110   have hf := normalized_defect p hp A B C hA hB
111   have hk : 0 < coefficient p := BetaNormalization.sine_factor_positive p hp
112   have hbound := FractionalScalarBounds.split_norm_bound (integrand p · A B C) p (2*‖C‖) ‖C*A-B*C‖
113     (‖C*A-B*C‖/(2*‖C‖)) hp (by positivity) hf.1
114     (fun t ht => integrand_low_bound p t hp ht A B C hA hB)
115     (fun t ht => integrand_high_bound p t ht A B C hA hB)
116   rw [FractionalScalarBounds.optimize_split p (2*‖C‖) ‖C*A-B*C‖ hp (by positivity) hdn] at hbound
117   rw [hf.2,norm_smul,Real.norm_of_nonneg hk.le]
118   calc
119     _ ≤ coefficient p*((2*‖C‖)^(1-(p:ℝ))*‖C*A-B*C‖^(p:ℝ)/((p:ℝ)*(1-(p:ℝ)))) :=
120       mul_le_mul_of_nonneg_left hbound hk.le
121     _ = _ := by
122       rw [Real.mul_rpow (by norm_num : (0:ℝ) ≤ 2) (norm_nonneg C)]
123       unfold holderConstant
124       ring
125 
126 end KomorebiPaperVI.FractionalNormBounds

Back to source controls