RectangularFractional.lean

1 import KomorebiPaperVI.FractionalNormBounds
2 import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
3 import Mathlib.Analysis.InnerProductSpace.StarOrder
4 
5 /-! Author: Komorebi P. Fractional defects between distinct complex Hilbert spaces. -/
6 namespace KomorebiPaperVI.RectangularFractional
7 open Set MeasureTheory Real
8 open scoped NNReal
9 open KomorebiPaperVI.NormalizedFractional
10 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
11 set_option backward.isDefEq.respectTransparency false
12 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
13     [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
14 
15 noncomputable def defect (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) : E →L[ℂ] F :=
16   C.comp A-B.comp C
17 noncomputable def power (A : E →L[ℂ] E) (p : ℝ≥0) : E →L[ℂ] E := CFC.nnrpow A p
18 noncomputable def fractionalDefect (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (p : ℝ≥0) : E →L[ℂ] F :=
19   C.comp (power A p)-(power B p).comp C
20 noncomputable def integrand (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (p t : ℝ) : E →L[ℂ] F :=
21   C.comp (cfcₙ (rpowIntegrand₀₁ p t) A)-(cfcₙ (rpowIntegrand₀₁ p t) B).comp C
22 
23 theorem normalized_integral (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
24     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B) :
25     IntegrableOn (integrand A B C p) (Ioi 0) ∧
26       fractionalDefect A B C p=coefficient p • ∫ t in Ioi 0,integrand A B C p t := by
27   have ha := cfc_lebesgue_integral p hp A hA
28   have hb := cfc_lebesgue_integral p hp B hB
29   let L := ContinuousLinearMap.compL ℂ E E F C
30   let M := (ContinuousLinearMap.compL ℂ E F F).flip C
31   have hl : IntegrableOn (fun t => C.comp (cfcₙ (rpowIntegrand₀₁ p t) A)) (Ioi 0) := L.integrable_comp ha.1
32   have hr : IntegrableOn (fun t => (cfcₙ (rpowIntegrand₀₁ p t) B).comp C) (Ioi 0) := M.integrable_comp hb.1
33   refine ⟨hl.sub hr,?_⟩
34   unfold fractionalDefect power integrand
35   rw [ha.2,hb.2,integral_sub hl hr]
36   have hL := L.integral_comp_comm ha.1
37   have hM := M.integral_comp_comm hb.1
38   change (∫ t in Ioi 0,C.comp (cfcₙ (rpowIntegrand₀₁ p t) A))=C.comp (∫ t in Ioi 0,cfcₙ (rpowIntegrand₀₁ p t) A) at hL
39   change (∫ t in Ioi 0,(cfcₙ (rpowIntegrand₀₁ p t) B).comp C)=(∫ t in Ioi 0,cfcₙ (rpowIntegrand₀₁ p t) B).comp C at hM
40   rw [hL,hM,ContinuousLinearMap.comp_smul,ContinuousLinearMap.smul_comp,smul_sub]
41 
42 theorem low_bound (p t : ℝ) (hp : p∈Ioo 0 1) (ht : 0 < t)
43     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B) :
44     ‖integrand A B C p t‖ ≤ 2*‖C‖*t^(p-1) := by
45   unfold integrand
46   rw [FractionalNormBounds.integrand_saturation p t hp ht A hA,
47     FractionalNormBounds.integrand_saturation p t hp ht B hB,
48     ContinuousLinearMap.comp_smul,ContinuousLinearMap.smul_comp,← smul_sub,norm_smul,
49     Real.norm_of_nonneg (Real.rpow_nonneg ht.le _)]
50   have ha := PositiveResolvent.saturation_norm A hA t ht
51   have hb := PositiveResolvent.saturation_norm B hB t ht
52   calc
53     _ ≤ t^(p-1)*(‖C‖*‖A*PositiveResolvent.resolvent A t‖+‖B*PositiveResolvent.resolvent B t‖*‖C‖) := by
54       gcongr
55       exact (norm_sub_le _ _).trans (add_le_add (ContinuousLinearMap.opNorm_comp_le _ _) (ContinuousLinearMap.opNorm_comp_le _ _))
56     _ ≤ t^(p-1)*(‖C‖*1+1*‖C‖) := by gcongr
57     _ = _ := by ring
58 
59 theorem resolvent_defect (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F)
60     (hA : 0 ≤ A) (hB : 0 ≤ B) (t : ℝ) (ht : 0 < t) :
61     (PositiveResolvent.resolvent B t).comp C-C.comp (PositiveResolvent.resolvent A t)=
62       (PositiveResolvent.resolvent B t).comp ((defect A B C).comp (PositiveResolvent.resolvent A t)) := by
63   let RA := PositiveResolvent.resolvent A t
64   let RB := PositiveResolvent.resolvent B t
65   have ha := PositiveResolvent.resolvent_left_inverse A hA t ht
66   have hb := PositiveResolvent.resolvent_right_inverse B hB t ht
67   ext x
68   have hax := congrArg (fun T : E →L[ℂ] E => RB (C (T x))) ha
69   have hbx := congrArg (fun T : F →L[ℂ] F => T (C (RA x))) hb
70   simp only [Algebra.algebraMap_eq_smul_one,mul_apply_eq_comp,add_apply,
71     smul_apply,one_apply_eq_self,map_add,ContinuousLinearMap.map_smul_of_tower] at hax hbx
72   change RB (C x)-C (RA x)=RB (C (A (RA x))-B (C (RA x)))
73   rw [map_sub]
74   calc
75     _ = (t • RB (C (RA x))+RB (C (A (RA x))))-
76         (t • RB (C (RA x))+RB (B (C (RA x)))) := congrArg₂ (·-·) hax.symm hbx.symm
77     _ = _ := by abel
78 
79 
80 theorem literal_integrand (p t : ℝ) (hp : p∈Ioo 0 1) (ht : 0 < t)
81     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B) :
82     integrand A B C p t=t^p • (PositiveResolvent.resolvent B t).comp
83       ((defect A B C).comp (PositiveResolvent.resolvent A t)) := by
84   rw [integrand,FractionalResolvent.cfc_integrand p t hp ht A hA,
85     FractionalResolvent.cfc_integrand p t hp ht B hB,
86     ContinuousLinearMap.comp_smul,ContinuousLinearMap.smul_comp,← smul_sub,
87     ← resolvent_defect A B C hA hB t ht]
88   congr 1
89   ext x
90   simp only [ContinuousLinearMap.comp_apply,sub_apply,map_sub,
91     Algebra.algebraMap_eq_smul_one,smul_apply,one_apply_eq_self,
92     ContinuousLinearMap.map_smul_of_tower]
93   abel
94 
95 theorem literal_resolvent_integral (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
96     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B) :
97     let f := fun t : ℝ => t^(p:ℝ) • (Ring.inverse (algebraMap ℝ (F →L[ℂ] F) t+B)).comp
98       ((defect A B C).comp (Ring.inverse (algebraMap ℝ (E →L[ℂ] E) t+A)))
99     IntegrableOn f (Ioi 0) ∧ fractionalDefect A B C p=coefficient p • ∫ t in Ioi 0,f t := by
100   dsimp only
101   have he : (fun t : ℝ => t^(p:ℝ) • (Ring.inverse (algebraMap ℝ (F →L[ℂ] F) t+B)).comp
102       ((defect A B C).comp (Ring.inverse (algebraMap ℝ (E →L[ℂ] E) t+A))))
103       =ᵐ[volume.restrict (Ioi 0)] integrand A B C p := by
104     filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
105     rw [literal_integrand p t hp ht A B C hA hB,
106       PositiveResolvent.resolvent_inverse A hA t ht,PositiveResolvent.resolvent_inverse B hB t ht]
107   have h := normalized_integral p hp A B C hA hB
108   exact ⟨h.1.congr he.symm,h.2.trans (congrArg (coefficient p • ·) (integral_congr_ae he.symm))⟩
109 
110 theorem exact_fractional_intertwining (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
111     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B)
112     (hD : defect A B C=0) : fractionalDefect A B C p=0 := by
113   rw [(normalized_integral p hp A B C hA hB).2]
114   have he : integrand A B C p=ᵐ[volume.restrict (Ioi 0)] 0 := by
115     filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
116     rw [literal_integrand p t hp ht A B C hA hB,hD]
117     simp
118   rw [integral_congr_ae he]
119   simp
120 
121 theorem gap_bound (p t m : ℝ) (ht : 0 < t) (hm : 0 ≤ m) (hp : p∈Ioo 0 1)
122     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B)
123     (hgA : algebraMap ℝ (E →L[ℂ] E) m ≤ A) (hgB : algebraMap ℝ (F →L[ℂ] F) m ≤ B) :
124     ‖integrand A B C p t‖ ≤ ‖defect A B C‖*(t^p/(t+m)^2) := by
125   rw [literal_integrand p t hp ht A B C hA hB,norm_smul,Real.norm_of_nonneg (Real.rpow_nonneg ht.le _)]
126   calc
127     _ ≤ t^p*(‖PositiveResolvent.resolvent B t‖*(‖defect A B C‖*‖PositiveResolvent.resolvent A t‖)) := by
128       gcongr
129       exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
130         (mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _))
131     _ ≤ t^p*((t+m)⁻¹*(‖defect A B C‖*(t+m)⁻¹)) := by
132       gcongr
133       · exact PositiveResolvent.resolvent_gap_norm B hB t m ht hm hgB
134       · exact PositiveResolvent.resolvent_gap_norm A hA t m ht hm hgA
135     _ = _ := by
136       have htm : t+m ≠ 0 := ne_of_gt (add_pos_of_pos_of_nonneg ht hm)
137       field_simp [htm]
138 
139 theorem high_bound (p t : ℝ) (ht : 0 < t) (hp : p∈Ioo 0 1)
140     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B) :
141     ‖integrand A B C p t‖ ≤ ‖defect A B C‖*t^(p-2) := by
142   have h := gap_bound p t 0 ht le_rfl hp A B C hA hB (by simpa using hA) (by simpa using hB)
143   simpa only [add_zero,Real.rpow_sub ht,Real.rpow_two] using h
144 
145 theorem common_gap_estimate (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1) (m : ℝ) (hm : 0 < m)
146     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B)
147     (hgA : algebraMap ℝ (E →L[ℂ] E) m ≤ A) (hgB : algebraMap ℝ (F →L[ℂ] F) m ≤ B) :
148     ‖fractionalDefect A B C p‖ ≤ (p:ℝ)*m^((p:ℝ)-1)*‖defect A B C‖ := by
149   have hd := normalized_integral p hp A B C hA hB
150   have hk : 0 < coefficient p := BetaNormalization.sine_factor_positive p hp
151   have hs : 0 < Real.sin (Real.pi*(p:ℝ)) := by
152     apply Real.sin_pos_of_pos_of_lt_pi
153     · exact mul_pos Real.pi_pos hp.1
154     · nlinarith [Real.pi_pos,hp.2]
155   have hg : IntegrableOn (fun t : ℝ => t^(p:ℝ)/(t+m)^2) (Ioi 0) := by
156     by_contra hn
157     have hz := integral_undef hn
158     rw [BetaNormalization.gap_integral p m hp hm] at hz
159     exact (mul_pos (Real.rpow_pos_of_pos hm _) (div_pos (mul_pos hp.1 Real.pi_pos) hs)).ne' hz
160   rw [hd.2,norm_smul,Real.norm_of_nonneg hk.le]
161   calc
162     _ ≤ coefficient p*(∫ t in Ioi 0,‖integrand A B C p t‖) := by
163       apply mul_le_mul_of_nonneg_left (norm_integral_le_integral_norm _) hk.le
164     _ ≤ coefficient p*(∫ t in Ioi 0,‖defect A B C‖*(t^(p:ℝ)/(t+m)^2)) := by
165       apply mul_le_mul_of_nonneg_left _ hk.le
166       apply setIntegral_mono_on hd.1.norm (hg.const_mul _) measurableSet_Ioi
167       intro t ht
168       exact gap_bound p t m ht hm.le hp A B C hA hB hgA hgB
169     _ = _ := by
170       rw [integral_const_mul,mul_left_comm,coefficient,BetaNormalization.normalized_gap_integral p m hp hm]
171       ring
172 
173 theorem holder_estimate (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
174     (A : E →L[ℂ] E) (B : F →L[ℂ] F) (C : E →L[ℂ] F) (hA : 0 ≤ A) (hB : 0 ≤ B) :
175     ‖fractionalDefect A B C p‖ ≤
176       FractionalNormBounds.holderConstant p*‖C‖^(1-(p:ℝ))*‖defect A B C‖^(p:ℝ) := by
177   by_cases hc : C=0
178   · subst C
179     simp [fractionalDefect,defect,Real.zero_rpow hp.1.ne']
180   by_cases hd : defect A B C=0
181   · have he := exact_fractional_intertwining p hp A B C hA hB hd
182     rw [he,norm_zero,hd]
183     simp [Real.zero_rpow hp.1.ne']
184   have hcn : 0 < ‖C‖ := norm_pos_iff.mpr hc
185   have hdn : 0 < ‖defect A B C‖ := norm_pos_iff.mpr hd
186   have hf := normalized_integral p hp A B C hA hB
187   have hk : 0 < coefficient p := BetaNormalization.sine_factor_positive p hp
188   have hbound := FractionalScalarBounds.split_norm_bound (integrand A B C p) p (2*‖C‖) ‖defect A B C‖
189     (‖defect A B C‖/(2*‖C‖)) hp (by positivity) hf.1
190     (fun t ht => low_bound p t hp ht A B C hA hB)
191     (fun t ht => high_bound p t ht hp A B C hA hB)
192   rw [FractionalScalarBounds.optimize_split p (2*‖C‖) ‖defect A B C‖ hp (by positivity) hdn] at hbound
193   rw [hf.2,norm_smul,Real.norm_of_nonneg hk.le]
194   calc
195     _ ≤ coefficient p*((2*‖C‖)^(1-(p:ℝ))*‖defect A B C‖^(p:ℝ)/((p:ℝ)*(1-(p:ℝ)))) :=
196       mul_le_mul_of_nonneg_left hbound hk.le
197     _ = _ := by
198       rw [Real.mul_rpow (by norm_num : (0:ℝ) ≤ 2) (norm_nonneg C)]
199       unfold FractionalNormBounds.holderConstant
200       ring
201 
202 end KomorebiPaperVI.RectangularFractional

Back to source controls