OperatorBounds.lean

1 import KomorebiPaperVI.Semigroups
2 
3 /-! Author: Komorebi P. General growth and finite-horizon contraction bounds. -/
4 namespace KomorebiPaperVI.OperatorBounds
5 open KomorebiPaperVI.Semigroups
6 open scoped BigOperators
7 variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
8     [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
9 
10 theorem growth_duhamel_bound (A : E →L[ℝ] E) (B : F →L[ℝ] F) (C : E →L[ℝ] F)
11     (Mf Mc wf wc t : ℝ) (ht : 0 ≤ t)
12     (hA : ∀ u, 0 ≤ u → ‖transfer A u‖ ≤ Mf*Real.exp (wf*u))
13     (hB : ∀ u, 0 ≤ u → ‖transfer B u‖ ≤ Mc*Real.exp (wc*u)) :
14     ‖C.comp (transfer A t)-(transfer B t).comp C‖ ≤
15       Mf*Mc*‖C.comp A-B.comp C‖ * ∫ r in 0..t, Real.exp (wc*(t-r))*Real.exp (wf*r) := by
16   let D := C.comp A-B.comp C
17   let f := fun r => (transfer B (t-r)).comp (D.comp (transfer A r))
18   let g := fun r => Mf*Mc*‖D‖*(Real.exp (wc*(t-r))*Real.exp (wf*r))
19   have hf : Continuous f := by dsimp [f]; fun_prop
20   have hg : Continuous g := by dsimp [g]; fun_prop
21   rw [duhamel_rectangular]
22   change ‖∫ r in 0..t, f r‖ ≤ _
23   calc
24     _ ≤ ∫ r in 0..t, ‖f r‖ := intervalIntegral.norm_integral_le_integral_norm ht
25     _ ≤ ∫ r in 0..t, g r := by
26       apply intervalIntegral.integral_mono_on ht (hf.norm.intervalIntegrable 0 t) (hg.intervalIntegrable 0 t)
27       intro r hr
28       have ha := hA r hr.1
29       have hb := hB (t-r) (sub_nonneg.mpr hr.2)
30       calc
31         _ ≤ ‖transfer B (t-r)‖*‖D.comp (transfer A r)‖ := ContinuousLinearMap.opNorm_comp_le _ _
32         _ ≤ (Mc*Real.exp (wc*(t-r)))*(‖D‖*(Mf*Real.exp (wf*r))) :=
33           mul_le_mul hb ((ContinuousLinearMap.opNorm_comp_le _ _).trans
34             (mul_le_mul_of_nonneg_left ha (norm_nonneg _)))
35             (norm_nonneg _) ((norm_nonneg _).trans hb)
36         _ = g r := by dsimp [g]; ring
37     _ = _ := by dsimp [g,D]; rw [intervalIntegral.integral_const_mul]
38 
39 omit [CompleteSpace E] in
40 theorem contraction_powers (A : E →L[ℝ] E) (hA : ‖A‖ ≤ 1) (n : ℕ) : ‖A^n‖ ≤ 1 := by
41   induction n with
42   | zero =>
43     simp only [pow_zero]
44     exact ContinuousLinearMap.norm_id_le
45   | succ n ih =>
46     rw [pow_succ]
47     exact (norm_mul_le _ _).trans (by nlinarith [norm_nonneg (A^n),norm_nonneg A])
48 
49 omit [CompleteSpace E] [CompleteSpace F] in
50 theorem finite_horizon_contraction (A : E →L[ℝ] E) (B : F →L[ℝ] F) (C : E →L[ℝ] F)
51     (hA : ‖A‖ ≤ 1) (hB : ‖B‖ ≤ 1) (n : ℕ) :
52     ‖C.comp (A^n)-(B^n).comp C‖ ≤ (n:ℝ)*‖C.comp A-B.comp C‖ := by
53   induction n with
54   | zero => simp [ContinuousLinearMap.one_def]
55   | succ n ih =>
56     have he : C.comp (A^(n+1))-(B^(n+1)).comp C =
57         B.comp (C.comp (A^n)-(B^n).comp C)+(C.comp A-B.comp C).comp (A^n) := by
58       ext x
59       simp [pow_succ', mul_apply_eq_comp, ContinuousLinearMap.comp_apply]
60     rw [he]
61     calc
62       _ ≤ ‖B.comp (C.comp (A^n)-(B^n).comp C)‖+
63           ‖(C.comp A-B.comp C).comp (A^n)‖ := norm_add_le _ _
64       _ ≤ 1*((n:ℝ)*‖C.comp A-B.comp C‖)+‖C.comp A-B.comp C‖*1 := by
65         apply add_le_add
66         · exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
67             (mul_le_mul hB ih (norm_nonneg _) (by norm_num))
68         · exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
69             (mul_le_mul_of_nonneg_left (contraction_powers A hA n) (norm_nonneg _))
70       _ = _ := by push_cast; ring
71 
72 end KomorebiPaperVI.OperatorBounds

Back to source controls