CoupledAnalytic.lean

1 import CoupledFormal
2 import Mathlib.Analysis.Complex.LocallyUniformLimit
3 import Mathlib.Analysis.Normed.Ring.InfiniteSum
4 
5 /-!
6 # Coupled functions: the local analytic bridge
7 
8 The recurrence is the one in `CoupledFormal`. All analytic assertions below
9 are restricted to `‖z‖ ^ 2 < 2` and positive scales at most one.
10 No entire continuation or global growth assertion is made here.
11 -/
12 
13 set_option autoImplicit false
14 set_option maxHeartbeats 800000
15 
16 noncomputable section
17 
18 namespace Komorebi.SpecialFunctions.Coupled.Scales
19 
20 /-- The function associated with an ordinary odd coefficient sequence. -/
21 def oddSum (c : ℕ → ℝ) (z : ℂ) : ℂ := ∑' n, (c n : ℂ) * z ^ (2 * n + 1)
22 
23 /-- The common open disk supplied by the coefficient majorant. -/
24 def localDisk : Set ℂ := {z | ‖z‖ ^ 2 < 2}
25 
26 theorem oddSum_zero (c : ℕ → ℝ) : oddSum c 0 = 0 := by
27   simp [oddSum]
28 
29 theorem oddSum_neg (c : ℕ → ℝ) (z : ℂ) : oddSum c (-z) = -oddSum c z := by
30   simp [oddSum, pow_add, pow_mul, tsum_neg]
31 
32 /-- A uniform geometric majorant on each smaller ball. -/
33 theorem odd_series_uniform_bound {c : ℕ → ℝ}
34     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
35     {R : ℝ} (hR : 0 ≤ R) {z : ℂ} (hz : z ∈ Metric.ball 0 R) (n : ℕ) :
36     ‖(c n : ℂ) * z ^ (2 * n + 1)‖ ≤ R * (R ^ 2 / 2) ^ n := by
37   have hzR : ‖z‖ ≤ R := (by simpa using hz : ‖z‖ < R).le
38   calc
39     _ ≤ ‖z‖ * (‖z‖ ^ 2 / 2) ^ n := odd_series_norm_bound hc z n
40     _ ≤ R * (R ^ 2 / 2) ^ n := by
41       apply mul_le_mul hzR
42       · exact pow_le_pow_left₀ (by positivity)
43           (div_le_div_of_nonneg_right (pow_le_pow_left₀ (norm_nonneg z) hzR 2) (by norm_num)) n
44       · positivity
45       · exact hR
46 
47 theorem oddSum_differentiableOn_ball {c : ℕ → ℝ}
48     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
49     {R : ℝ} (hR : 0 ≤ R) (hR2 : R ^ 2 < 2) :
50     DifferentiableOn ℂ (oddSum c) (Metric.ball 0 R) := by
51   apply Complex.differentiableOn_tsum_of_summable_norm
52     ((summable_geometric_of_lt_one (by positivity : 0 ≤ R ^ 2 / 2)
53       (by linarith : R ^ 2 / 2 < 1)).mul_left R)
54   · intro n
55     exact (differentiable_const _ |>.mul (differentiable_id.pow _)).differentiableOn
56   · exact Metric.isOpen_ball
57   · intro n z hz
58     exact odd_series_uniform_bound hc hR hz n
59 
60 /-- Every point of the disk lies in a smaller ball with a summable majorant. -/
61 theorem exists_local_radius {z : ℂ} (hz : z ∈ localDisk) :
62     ∃ R : ℝ, 0 ≤ R ∧ R ^ 2 < 2 ∧ z ∈ Metric.ball 0 R := by
63   have hs : 0 ≤ Real.sqrt 2 := Real.sqrt_nonneg _
64   have hs2 : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num)
65   have hlt : ‖z‖ < Real.sqrt 2 := by
66     dsimp [localDisk] at hz
67     nlinarith [norm_nonneg z]
68   obtain ⟨R, hzR, hRs⟩ := exists_between hlt
69   have hR : 0 ≤ R := (norm_nonneg z).trans hzR.le
70   refine ⟨R, hR, ?_, ?_⟩
71   · nlinarith
72   · simpa using hzR
73 
74 theorem oddSum_differentiableAt {c : ℕ → ℝ}
75     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
76     {z : ℂ} (hz : z ∈ localDisk) : DifferentiableAt ℂ (oddSum c) z := by
77   obtain ⟨R, hR, hR2, hzR⟩ := exists_local_radius hz
78   exact (oddSum_differentiableOn_ball hc hR hR2).differentiableAt
79     (Metric.isOpen_ball.mem_nhds hzR)
80 
81 theorem oddSum_differentiableOn {c : ℕ → ℝ}
82     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n) :
83     DifferentiableOn ℂ (oddSum c) localDisk := by
84   intro z hz
85   exact (oddSum_differentiableAt hc hz).differentiableWithinAt
86 
87 theorem oddTerm_hasDerivAt (c : ℕ → ℝ) (n : ℕ) (z : ℂ) :
88     HasDerivAt (fun w : ℂ => (c n : ℂ) * w ^ (2 * n + 1))
89       ((c n : ℂ) * (2 * n + 1) * z ^ (2 * n)) z := by
90   simpa [mul_assoc] using
91     ((hasDerivAt_id z).pow (2 * n + 1)).const_mul (c n : ℂ)
92 
93 /-- Termwise differentiation, with convergence of the differentiated series. -/
94 theorem oddSum_hasSum_deriv {c : ℕ → ℝ}
95     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
96     {z : ℂ} (hz : z ∈ localDisk) :
97     HasSum (fun n => (c n : ℂ) * (2 * n + 1) * z ^ (2 * n)) (deriv (oddSum c) z) := by
98   obtain ⟨R, hR, hR2, hzR⟩ := exists_local_radius hz
99   have h := Complex.hasSum_deriv_of_summable_norm
100     ((summable_geometric_of_lt_one (by positivity : 0 ≤ R ^ 2 / 2)
101       (by linarith : R ^ 2 / 2 < 1)).mul_left R)
102     (fun n => (differentiable_const _ |>.mul (differentiable_id.pow (2 * n + 1))).differentiableOn)
103     Metric.isOpen_ball (fun n w hw => odd_series_uniform_bound hc hR hw n) hzR
104   convert! h using 1
105   ext n
106   exact (oddTerm_hasDerivAt c n z).deriv.symm
107 
108 theorem oddSum_hasDerivAt {c : ℕ → ℝ}
109     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
110     {z : ℂ} (hz : z ∈ localDisk) :
111     HasDerivAt (oddSum c) (∑' n, (c n : ℂ) * (2 * n + 1) * z ^ (2 * n)) z := by
112   rw [(oddSum_hasSum_deriv hc hz).tsum_eq]
113   exact (oddSum_differentiableAt hc hz).hasDerivAt
114 
115 /-- The two sums are defined from the existing recursively constructed coefficients. -/
116 def U (s : Scales) : ℂ → ℂ := oddSum (fun n => (s.coefficients n).1)
117 
118 def V (s : Scales) : ℂ → ℂ := oddSum (fun n => (s.coefficients n).2)
119 
120 theorem coefficient_bounds_left (s : Scales) (hs : s.positive)
121     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1) (n : ℕ) :
122     0 ≤ (s.coefficients n).1 ∧ (s.coefficients n).1 ≤ (1 / 2 : ℝ) ^ n :=
123   ⟨(s.coefficients_positive hs n).1.le, (s.coefficients_le_geometric hs hsmall n).1⟩
124 
125 theorem coefficient_bounds_right (s : Scales) (hs : s.positive)
126     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1) (n : ℕ) :
127     0 ≤ (s.coefficients n).2 ∧ (s.coefficients n).2 ≤ (1 / 2 : ℝ) ^ n :=
128   ⟨(s.coefficients_positive hs n).2.le, (s.coefficients_le_geometric hs hsmall n).2⟩
129 
130 theorem coupled_differentiableOn (s : Scales) (hs : s.positive)
131     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1) :
132     DifferentiableOn ℂ s.U localDisk ∧ DifferentiableOn ℂ s.V localDisk :=
133   ⟨oddSum_differentiableOn (s.coefficient_bounds_left hs hsmall),
134     oddSum_differentiableOn (s.coefficient_bounds_right hs hsmall)⟩
135 
136 theorem mul_mem_localDisk {x z : ℂ} (hx : ‖x‖ ≤ 1) (hz : z ∈ localDisk) :
137     x * z ∈ localDisk := by
138   have hle : ‖x * z‖ ≤ ‖z‖ := by
139     rw [norm_mul]
140     nlinarith [norm_nonneg z]
141   exact lt_of_le_of_lt (pow_le_pow_left₀ (norm_nonneg _) hle 2) hz
142 
143 /-- The absolutely convergent Cauchy product, in the recurrence's finite indexing. -/
144 theorem oddSum_mul_eq {c d : ℕ → ℝ}
145     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
146     (hd : ∀ n, 0 ≤ d n ∧ d n ≤ (1 / 2 : ℝ) ^ n)
147     {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hx1 : x ≤ 1) (hy1 : y ≤ 1)
148     {z : ℂ} (hz : z ∈ localDisk) :
149     oddSum c ((x : ℂ) * z) * oddSum d ((y : ℂ) * z) =
150       ∑' n, ((∑ i : Fin (n + 1),
151         x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1) * c i.val * d (n - i.val) : ℝ) : ℂ) *
152         z ^ (2 * n + 2) := by
153   have hxz := mul_mem_localDisk (x := (x : ℂ))
154     (by simpa only [Complex.norm_of_nonneg hx] using hx1) hz
155   have hyz := mul_mem_localDisk (x := (y : ℂ))
156     (by simpa only [Complex.norm_of_nonneg hy] using hy1) hz
157   unfold oddSum
158   rw [tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm
159     (odd_series_norm_summable hc _ hxz) (odd_series_norm_summable hd _ hyz)]
160   apply tsum_congr
161   intro n
162   rw [← Fin.sum_univ_eq_sum_range]
163   simp only [Complex.ofReal_sum, Finset.sum_mul, Complex.ofReal_mul, Complex.ofReal_pow]
164   apply Finset.sum_congr rfl
165   intro i _
166   have hi : i.val ≤ n := by omega
167   have he : (2 * i.val + 1) + (2 * (n - i.val) + 1) = 2 * n + 2 := by omega
168   simp only [mul_pow]
169   calc
170     _ = (x : ℂ) ^ (2 * i.val + 1) * (y : ℂ) ^ (2 * (n - i.val) + 1) *
171         (c i.val : ℂ) * (d (n - i.val) : ℂ) *
172         (z ^ (2 * i.val + 1) * z ^ (2 * (n - i.val) + 1)) := by ring
173     _ = _ := by rw [← pow_add, he]
174 
175 /-- The denominator in the recurrence is nonzero, including at the first step. -/
176 theorem nextCoefficient_mul_denominator (x y : ℝ) (f : ℕ → ℝ × ℝ) (n : ℕ) :
177     nextCoefficient x y f n * (2 * (n : ℝ) + 3) =
178       ∑ i : Fin (n + 1), x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1) *
179         (f i.val).1 * (f (n - i.val)).2 := by
180   exact div_mul_cancel₀ _ (by positivity)
181 
182 /-- A local analytic equation follows from the coefficient recurrence and Cauchy product. -/
183 theorem oddSum_deriv_eq_of_recurrence {c d e : ℕ → ℝ}
184     (hc : ∀ n, 0 ≤ c n ∧ c n ≤ (1 / 2 : ℝ) ^ n)
185     (hd : ∀ n, 0 ≤ d n ∧ d n ≤ (1 / 2 : ℝ) ^ n)
186     (he : ∀ n, 0 ≤ e n ∧ e n ≤ (1 / 2 : ℝ) ^ n)
187     {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hx1 : x ≤ 1) (hy1 : y ≤ 1)
188     (he0 : e 0 = 1)
189     (hrec : ∀ n, e (n + 1) = nextCoefficient x y (fun j => (c j, d j)) n)
190     {z : ℂ} (hz : z ∈ localDisk) :
191     deriv (oddSum e) z = 1 + oddSum c ((x : ℂ) * z) * oddSum d ((y : ℂ) * z) := by
192   rw [← (oddSum_hasSum_deriv he hz).tsum_eq,
193     (oddSum_hasSum_deriv he hz).summable.tsum_eq_zero_add]
194   simp only [he0, Complex.ofReal_one, Nat.cast_zero, mul_zero, zero_add, pow_zero, mul_one]
195   rw [oddSum_mul_eq hc hd hx hy hx1 hy1 hz]
196   congr 1
197   apply tsum_congr
198   intro n
199   rw [hrec]
200   have h := congrArg (fun t : ℝ => (t : ℂ))
201     (nextCoefficient_mul_denominator x y (fun j => (c j, d j)) n)
202   simp only [Complex.ofReal_mul, Complex.ofReal_add, Complex.ofReal_ofNat,
203     Complex.ofReal_natCast] at h
204   convert congrArg (fun t : ℂ => t * z ^ (2 * n + 2)) h using 1
205   push_cast
206   ring
207 
208 theorem coupled_local_equations (s : Scales) (hs : s.positive)
209     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1)
210     {z : ℂ} (hz : z ∈ localDisk) :
211     deriv s.U z = 1 + s.U ((s.q : ℂ) * z) * s.V ((s.r : ℂ) * z) ∧
212     deriv s.V z = 1 + s.U ((s.a : ℂ) * z) * s.V ((s.b : ℂ) * z) := by
213   have h0 := s.coefficients_zero
214   constructor
215   · apply oddSum_deriv_eq_of_recurrence (s.coefficient_bounds_left hs hsmall)
216       (s.coefficient_bounds_right hs hsmall) (s.coefficient_bounds_left hs hsmall)
217       hs.1.le hs.2.1.le hsmall.1 hsmall.2.1
218     · exact congrArg Prod.fst h0
219     · intro n
220       exact congrArg Prod.fst (s.coefficients_solution.2 n)
221     · exact hz
222   · apply oddSum_deriv_eq_of_recurrence (s.coefficient_bounds_left hs hsmall)
223       (s.coefficient_bounds_right hs hsmall) (s.coefficient_bounds_right hs hsmall)
224       hs.2.2.1.le hs.2.2.2.le hsmall.2.2.1 hsmall.2.2.2
225     · exact congrArg Prod.snd h0
226     · intro n
227       exact congrArg Prod.snd (s.coefficients_solution.2 n)
228     · exact hz
229 
230 /-- The normalized analytic solution on the common disk, including both equations. -/
231 theorem coupled_local_solution (s : Scales) (hs : s.positive)
232     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1) :
233     s.U 0 = 0 ∧ s.V 0 = 0 ∧
234       ∀ z ∈ localDisk,
235         HasDerivAt s.U (1 + s.U ((s.q : ℂ) * z) * s.V ((s.r : ℂ) * z)) z ∧
236         HasDerivAt s.V (1 + s.U ((s.a : ℂ) * z) * s.V ((s.b : ℂ) * z)) z := by
237   refine ⟨oddSum_zero _, oddSum_zero _, ?_⟩
238   intro z hz
239   have hU := oddSum_differentiableAt (s.coefficient_bounds_left hs hsmall) hz
240   have hV := oddSum_differentiableAt (s.coefficient_bounds_right hs hsmall) hz
241   exact ⟨(s.coupled_local_equations hs hsmall hz).1 ▸ hU.hasDerivAt,
242     (s.coupled_local_equations hs hsmall hz).2 ▸ hV.hasDerivAt⟩
243 
244 theorem coupled_initial_derivatives (s : Scales) (hs : s.positive)
245     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1) :
246     deriv s.U 0 = 1 ∧ deriv s.V 0 = 1 := by
247   have h := s.coupled_local_equations hs hsmall (z := 0) (by norm_num [localDisk])
248   simpa only [mul_zero, U, V, oddSum_zero, zero_mul, add_zero] using h
249 
250 theorem coupled_odd (s : Scales) (z : ℂ) : s.U (-z) = -s.U z ∧ s.V (-z) = -s.V z :=
251   ⟨oddSum_neg _ _, oddSum_neg _ _⟩
252 
253 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls