RectangularTowers.lean

1 import KomorebiPaperVI.RectangularSemigroup
2 import Mathlib.Analysis.Normed.Group.FunctionSeries
3 
4 /-! Author: Komorebi P. Generator criteria for varying-Hilbert-space refinement towers.
5 Summability across different operator spaces means summability of the real norms. -/
6 namespace KomorebiPaperVI.RectangularTowers
7 open Set
8 open scoped NNReal
9 open KomorebiPaperVI.RectangularFractional KomorebiPaperVI.RectangularSemigroup
10 set_option backward.isDefEq.respectTransparency false
11 variable {H : ℕ → Type*} [∀ n,NormedAddCommGroup (H n)] [∀ n,InnerProductSpace ℂ (H n)]
12     [∀ n,CompleteSpace (H n)]
13 
14 noncomputable def generatorNorm (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n) (n : ℕ) : ℝ :=
15   ‖defect (A (n+1)) (A n) (C n)‖
16 noncomputable def fractionalNorm (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
17     (p : ℝ≥0) (n : ℕ) : ℝ := ‖fractionalDefect (A (n+1)) (A n) (C n) p‖
18 noncomputable def timeNorm (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
19     (p : ℝ≥0) (t : ℝ) (n : ℕ) : ℝ := ‖timeDefect (A (n+1)) (A n) (C n) p t‖
20 
21 theorem holder_constant_positive (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1) :
22     0 < FractionalNormBounds.holderConstant p := by
23   unfold FractionalNormBounds.holderConstant
24   exact div_pos (mul_pos (Real.rpow_pos_of_pos (by norm_num) _)
25     (BetaNormalization.sine_factor_positive p hp)) (mul_pos hp.1 (sub_pos.mpr hp.2))
26 
27 theorem holder_majorant (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
28     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
29     (M : ℝ) (hC : ∀ n,‖C n‖ ≤ M) (n : ℕ) :
30     fractionalNorm A C p n ≤ FractionalNormBounds.holderConstant p*M^(1-(p:ℝ))*(generatorNorm A C n)^(p:ℝ) := by
31   calc
32     _ ≤ FractionalNormBounds.holderConstant p*‖C n‖^(1-(p:ℝ))*(generatorNorm A C n)^(p:ℝ) :=
33       holder_estimate p hp (A (n+1)) (A n) (C n) (hA _) (hA _)
34     _ ≤ _ := by
35       have hk := (holder_constant_positive p hp).le
36       have hg : 0 ≤ (generatorNorm A C n)^(p:ℝ) := Real.rpow_nonneg (norm_nonneg _) _
37       exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left
38         (Real.rpow_le_rpow (norm_nonneg _) (hC n) (sub_nonneg.mpr hp.2.le)) hk) hg
39 
40 theorem generator_holder_summable (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
41     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
42     (M : ℝ) (hC : ∀ n,‖C n‖ ≤ M)
43     (hs : Summable (fun n => (generatorNorm A C n)^(p:ℝ))) : Summable (fractionalNorm A C p) := by
44   apply (hs.mul_left (FractionalNormBounds.holderConstant p*M^(1-(p:ℝ)))).of_norm_bounded
45   intro n
46   rw [Real.norm_of_nonneg (show 0 ≤ fractionalNorm A C p n from norm_nonneg _)]
47   exact holder_majorant A C hA p hp M hC n
48 
49 theorem generator_gap_summable (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
50     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
51     (m : ℝ) (hm : 0 < m) (hgap : ∀ n,algebraMap ℝ (H n →L[ℂ] H n) m ≤ A n)
52     (hs : Summable (generatorNorm A C)) : Summable (fractionalNorm A C p) := by
53   apply (hs.mul_left ((p:ℝ)*m^((p:ℝ)-1))).of_norm_bounded
54   intro n
55   rw [Real.norm_of_nonneg (show 0 ≤ fractionalNorm A C p n from norm_nonneg _)]
56   exact common_gap_estimate p hp m hm (A (n+1)) (A n) (C n) (hA _) (hA _) (hgap _) (hgap _)
57 
58 theorem bounded_time_majorant (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
59     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : 0 < p) (T t : ℝ) (ht : t∈Icc 0 T) (n : ℕ) :
60     timeNorm A C p t n ≤ T*fractionalNorm A C p n :=
61   (fractional_contraction_bound (A (n+1)) (A n) (C n) (hA _) (hA _) p hp t ht.1).trans
62     (mul_le_mul_of_nonneg_right ht.2 (norm_nonneg _))
63 
64 theorem time_norms_summable (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
65     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : 0 < p) (t : ℝ) (ht : 0 ≤ t)
66     (hs : Summable (fractionalNorm A C p)) : Summable (timeNorm A C p t) := by
67   apply (hs.mul_left t).of_norm_bounded
68   intro n
69   rw [Real.norm_of_nonneg (show 0 ≤ timeNorm A C p t n from norm_nonneg _)]
70   exact bounded_time_majorant A C hA p hp t t ⟨ht,le_rfl⟩ n
71 
72 theorem bounded_time_uniform_convergence (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
73     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : 0 < p) (T : ℝ)
74     (hs : Summable (fractionalNorm A C p)) :
75     TendstoUniformlyOn (fun N t => ∑ n ∈ Finset.range N,timeNorm A C p t n)
76       (fun t => ∑' n,timeNorm A C p t n) Filter.atTop (Icc 0 T) := by
77   apply tendstoUniformlyOn_tsum_nat (hs.mul_left T)
78   intro n t ht
79   rw [Real.norm_of_nonneg (show 0 ≤ timeNorm A C p t n from norm_nonneg _)]
80   exact bounded_time_majorant A C hA p hp T t ht n
81 
82 theorem holder_tower (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
83     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
84     (M : ℝ) (hC : ∀ n,‖C n‖ ≤ M) (hs : Summable (fun n => (generatorNorm A C n)^(p:ℝ))) :
85     Summable (fractionalNorm A C p) ∧
86     (∀ t,0 ≤ t → Summable (timeNorm A C p t)) ∧
87     (∀ T,TendstoUniformlyOn (fun N t => ∑ n ∈ Finset.range N,timeNorm A C p t n)
88       (fun t => ∑' n,timeNorm A C p t n) Filter.atTop (Icc 0 T)) := by
89   have h := generator_holder_summable A C hA p hp M hC hs
90   exact ⟨h,fun t ht => time_norms_summable A C hA p hp.1 t ht h,
91     fun T => bounded_time_uniform_convergence A C hA p hp.1 T h⟩
92 
93 theorem gap_tower (A : ∀ n,H n →L[ℂ] H n) (C : ∀ n,H (n+1) →L[ℂ] H n)
94     (hA : ∀ n,0 ≤ A n) (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1)
95     (m : ℝ) (hm : 0 < m) (hgap : ∀ n,algebraMap ℝ (H n →L[ℂ] H n) m ≤ A n)
96     (hs : Summable (generatorNorm A C)) :
97     Summable (fractionalNorm A C p) ∧
98     (∀ t,0 ≤ t → Summable (timeNorm A C p t)) ∧
99     (∀ T,TendstoUniformlyOn (fun N t => ∑ n ∈ Finset.range N,timeNorm A C p t n)
100       (fun t => ∑' n,timeNorm A C p t n) Filter.atTop (Icc 0 T)) := by
101   have h := generator_gap_summable A C hA p hp m hm hgap hs
102   exact ⟨h,fun t ht => time_norms_summable A C hA p hp.1 t ht h,
103     fun T => bounded_time_uniform_convergence A C hA p hp.1 T h⟩
104 
105 end KomorebiPaperVI.RectangularTowers

Back to source controls