FractionalTowers.lean

1 import KomorebiPaperVI.FractionalSemigroup
2 import Mathlib.Analysis.Normed.Group.FunctionSeries
3 
4 /-! Author: Komorebi P. Uniform bounded-time control from summable actual fractional defects.
5 The generator-to-fractional estimates remain the separate obligation of Theorem 10.3. -/
6 namespace KomorebiPaperVI.FractionalTowers
7 open Set
8 open KomorebiPaperVI.FractionalSemigroup
9 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
10 variable {R : Type*} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
11 
12 noncomputable def timeDefect (A C : ℕ → R) (a t : ℝ) (n : ℕ) : R :=
13   C n*evolution (A (n+1)) a t-evolution (A n) a t*C n
14 
15 theorem bounded_time_majorant (A C : ℕ → R) (hA : ∀ n,0 ≤ A n)
16     (a T : ℝ) (ha : 0 < a) (n : ℕ) (t : ℝ) (ht : t∈Icc 0 T) :
17     ‖timeDefect A C a t n‖ ≤ T*‖defect (A (n+1)) (A n) (C n) a‖ := by
18   exact (fractional_contraction_bound _ _ _ (hA (n+1)) (hA n) a t ha ht.1).trans
19     (mul_le_mul_of_nonneg_right ht.2 (norm_nonneg _))
20 
21 theorem time_defects_norm_summable (A C : ℕ → R) (hA : ∀ n,0 ≤ A n)
22     (a t : ℝ) (ha : 0 < a) (ht : 0 ≤ t)
23     (hs : Summable (fun n => ‖defect (A (n+1)) (A n) (C n) a‖)) :
24     Summable (fun n => ‖timeDefect A C a t n‖) := by
25   apply (hs.mul_left t).of_norm_bounded
26   intro n
27   rw [Real.norm_of_nonneg (norm_nonneg _)]
28   exact fractional_contraction_bound _ _ _ (hA (n+1)) (hA n) a t ha ht
29 
30 theorem time_defects_summable (A C : ℕ → R) (hA : ∀ n,0 ≤ A n)
31     (a t : ℝ) (ha : 0 < a) (ht : 0 ≤ t)
32     (hs : Summable (fun n => ‖defect (A (n+1)) (A n) (C n) a‖)) :
33     Summable (timeDefect A C a t) := (time_defects_norm_summable A C hA a t ha ht hs).of_norm
34 
35 theorem bounded_time_uniform_convergence (A C : ℕ → R) (hA : ∀ n,0 ≤ A n)
36     (a T : ℝ) (ha : 0 < a)
37     (hs : Summable (fun n => ‖defect (A (n+1)) (A n) (C n) a‖)) :
38     TendstoUniformlyOn (fun N t => ∑ n ∈ Finset.range N,timeDefect A C a t n)
39       (fun t => ∑' n,timeDefect A C a t n) Filter.atTop (Icc 0 T) := by
40   apply tendstoUniformlyOn_tsum_nat (hs.mul_left T)
41   intro n t ht
42   exact bounded_time_majorant A C hA a T ha n t ht
43 
44 end KomorebiPaperVI.FractionalTowers

Back to source controls