CoupledEntire.lean

1 import CoupledAnalytic
2 
3 /-!
4 # Entire coupled functions under strict contraction
5 
6 The recurrence and the sums are unchanged from Blocks 01 and 02. The new
7 mechanism propagates absolute convergence using the recurrence denominator
8 and the absolutely convergent Cauchy product.
9 -/
10 
11 set_option autoImplicit false
12 set_option maxHeartbeats 1000000
13 
14 noncomputable section
15 
16 namespace Komorebi.SpecialFunctions.Coupled.Scales
17 
18 /-- The finite Cauchy-product coefficient at a fixed evaluation point. -/
19 def oddConvolution (c d : ℕ → ℝ) (x y : ℝ) (z : ℂ) (n : ℕ) : ℂ :=
20   ∑ i ∈ Finset.range (n + 1),
21     ((c i : ℂ) * ((x : ℂ) * z) ^ (2 * i + 1)) *
22       ((d (n - i) : ℂ) * ((y : ℂ) * z) ^ (2 * (n - i) + 1))
23 
24 theorem oddConvolution_eq (c d : ℕ → ℝ) (x y : ℝ) (z : ℂ) (n : ℕ) :
25     oddConvolution c d x y z n =
26       ((∑ i : Fin (n + 1), x ^ (2 * i.val + 1) * y ^ (2 * (n - i.val) + 1) *
27         c i.val * d (n - i.val) : ℝ) : ℂ) * z ^ (2 * n + 2) := by
28   unfold oddConvolution
29   rw [← Fin.sum_univ_eq_sum_range]
30   simp only [Complex.ofReal_sum, Finset.sum_mul, Complex.ofReal_mul, Complex.ofReal_pow]
31   apply Finset.sum_congr rfl
32   intro i _
33   have hi : i.val ≤ n := by omega
34   have he : (2 * i.val + 1) + (2 * (n - i.val) + 1) = 2 * n + 2 := by omega
35   simp only [mul_pow]
36   calc
37     _ = (x : ℂ) ^ (2 * i.val + 1) * (y : ℂ) ^ (2 * (n - i.val) + 1) *
38         (c i.val : ℂ) * (d (n - i.val) : ℂ) *
39         (z ^ (2 * i.val + 1) * z ^ (2 * (n - i.val) + 1)) := by ring
40     _ = _ := by rw [← pow_add, he]
41 
42 /-- The recurrence relates the next series term to the finite Cauchy product. -/
43 theorem next_term_mul_denominator (c d : ℕ → ℝ) (x y : ℝ) (z : ℂ) (n : ℕ) :
44     ((nextCoefficient x y (fun j => (c j, d j)) n : ℂ) * z ^ (2 * (n + 1) + 1)) *
45       ((2 * (n : ℝ) + 3 : ℝ) : ℂ) = z * oddConvolution c d x y z n := by
46   have h := congrArg (fun t : ℝ => (t : ℂ))
47     (nextCoefficient_mul_denominator x y (fun j => (c j, d j)) n)
48   rw [oddConvolution_eq]
49   calc
50     _ = ((nextCoefficient x y (fun j => (c j, d j)) n : ℂ) *
51         ((2 * (n : ℝ) + 3 : ℝ) : ℂ)) * z ^ (2 * (n + 1) + 1) := by ring
52     _ = _ := by rw [← Complex.ofReal_mul, h]; ring
53 
54 /-- No summability or positivity is assumed in this pointwise norm estimate. -/
55 theorem next_term_norm_le (c d : ℕ → ℝ) (x y : ℝ) (z : ℂ) (n : ℕ) :
56     ‖(nextCoefficient x y (fun j => (c j, d j)) n : ℂ) * z ^ (2 * (n + 1) + 1)‖ ≤
57       ‖z‖ * ‖oddConvolution c d x y z n‖ := by
58   have h := congrArg norm (next_term_mul_denominator c d x y z n)
59   have hd : 0 ≤ 2 * (n : ℝ) + 3 := by positivity
60   simp only [norm_mul, Complex.norm_of_nonneg hd] at h
61   have hn : 0 ≤ ‖(nextCoefficient x y (fun j => (c j, d j)) n : ℂ) *
62       z ^ (2 * (n + 1) + 1)‖ := norm_nonneg _
63   have hden : (1 : ℝ) ≤ 2 * (n : ℝ) + 3 := by
64     have := Nat.cast_nonneg (α := ℝ) n
65     linarith
66   calc
67     _ = _ * (1 : ℝ) := (mul_one _).symm
68     _ ≤ _ * (2 * (n : ℝ) + 3) := mul_le_mul_of_nonneg_left hden hn
69     _ = _ := by simpa only [norm_mul] using h
70 
71 /-- Convergence at the two contracted arguments implies convergence of the
72 coefficient series one recurrence step outward. -/
73 theorem odd_series_bootstrap {c d e : ℕ → ℝ} {x y : ℝ} (z : ℂ)
74     (hrec : ∀ n, e (n + 1) = nextCoefficient x y (fun j => (c j, d j)) n)
75     (hc : Summable (fun n => ‖(c n : ℂ) * ((x : ℂ) * z) ^ (2 * n + 1)‖))
76     (hd : Summable (fun n => ‖(d n : ℂ) * ((y : ℂ) * z) ^ (2 * n + 1)‖)) :
77     Summable (fun n => ‖(e n : ℂ) * z ^ (2 * n + 1)‖) := by
78   have hconv : Summable (fun n => ‖oddConvolution c d x y z n‖) := by
79     simpa only [oddConvolution] using
80       (summable_norm_sum_mul_range_of_summable_norm (R := ℂ)
81         (f := fun n => (c n : ℂ) * ((x : ℂ) * z) ^ (2 * n + 1))
82         (g := fun n => (d n : ℂ) * ((y : ℂ) * z) ^ (2 * n + 1)) hc hd)
83   have htail : Summable (fun n => ‖(e (n + 1) : ℂ) * z ^ (2 * (n + 1) + 1)‖) := by
84     apply Summable.of_nonneg_of_le (fun n => norm_nonneg _) _ (hconv.mul_left ‖z‖)
85     intro n
86     rw [hrec]
87     exact next_term_norm_le c d x y z n
88   exact (summable_nat_add_iff 1).mp htail
89 
90 /-- Absolute convergence of both constructed odd coefficient series. -/
91 def NormConverges (s : Scales) (z : ℂ) : Prop :=
92   Summable (fun n => ‖((s.coefficients n).1 : ℂ) * z ^ (2 * n + 1)‖) ∧
93   Summable (fun n => ‖((s.coefficients n).2 : ℂ) * z ^ (2 * n + 1)‖)
94 
95 theorem coefficient_series_bootstrap (s : Scales) (z : ℂ)
96     (hq : s.NormConverges ((s.q : ℂ) * z))
97     (hr : s.NormConverges ((s.r : ℂ) * z))
98     (ha : s.NormConverges ((s.a : ℂ) * z))
99     (hb : s.NormConverges ((s.b : ℂ) * z)) : s.NormConverges z := by
100   constructor
101   · apply odd_series_bootstrap z _ hq.1 hr.2
102     intro n
103     exact congrArg Prod.fst (s.coefficients_solution.2 n)
104   · apply odd_series_bootstrap z _ ha.1 hb.2
105     intro n
106     exact congrArg Prod.snd (s.coefficients_solution.2 n)
107 
108 /-- The largest of the four labeled positive scales. -/
109 def maxScale (s : Scales) : ℝ := max (max s.q s.r) (max s.a s.b)
110 
111 theorem maxScale_bounds (s : Scales) :
112     s.q ≤ s.maxScale ∧ s.r ≤ s.maxScale ∧ s.a ≤ s.maxScale ∧ s.b ≤ s.maxScale :=
113   ⟨(le_max_left _ _).trans (le_max_left _ _),
114     (le_max_right _ _).trans (le_max_left _ _),
115     (le_max_left _ _).trans (le_max_right _ _),
116     (le_max_right _ _).trans (le_max_right _ _)⟩
117 
118 theorem maxScale_lt_one (s : Scales)
119     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) : s.maxScale < 1 :=
120   max_lt (max_lt hstrict.1 hstrict.2.1) (max_lt hstrict.2.2.1 hstrict.2.2.2)
121 
122 /-- Convergence on every level of the contraction ladder. The estimate uses
123 multiplication by Q^n, avoiding any division by a possibly zero radius. -/
124 theorem coefficient_series_on_ladder (s : Scales) (hs : s.positive)
125     (hsmall : s.q ≤ 1 ∧ s.r ≤ 1 ∧ s.a ≤ 1 ∧ s.b ≤ 1)
126     {Q : ℝ} (hQ : 0 ≤ Q) (hscales : s.q ≤ Q ∧ s.r ≤ Q ∧ s.a ≤ Q ∧ s.b ≤ Q)
127     (n : ℕ) (z : ℂ) (hz : ‖z‖ * Q ^ n ≤ 1) : s.NormConverges z := by
128   induction n generalizing z with
129   | zero =>
130     have hnorm : ‖z‖ ≤ 1 := by simpa using hz
131     exact s.coefficient_series_absolutely_convergent hs hsmall z (by nlinarith [norm_nonneg z])
132   | succ n ih =>
133     have harg {t : ℝ} (ht : 0 ≤ t) (htQ : t ≤ Q) :
134         ‖(t : ℂ) * z‖ * Q ^ n ≤ 1 := by
135       rw [norm_mul, Complex.norm_of_nonneg ht]
136       calc
137         _ ≤ (Q * ‖z‖) * Q ^ n := mul_le_mul_of_nonneg_right
138           (mul_le_mul_of_nonneg_right htQ (norm_nonneg z)) (pow_nonneg hQ _)
139         _ = ‖z‖ * Q ^ (n + 1) := by rw [pow_succ]; ring
140         _ ≤ 1 := hz
141     exact s.coefficient_series_bootstrap z
142       (ih _ (harg hs.1.le hscales.1)) (ih _ (harg hs.2.1.le hscales.2.1))
143       (ih _ (harg hs.2.2.1.le hscales.2.2.1))
144       (ih _ (harg hs.2.2.2.le hscales.2.2.2))
145 
146 /-- Strict contraction promotes the previously local absolute convergence to
147 every complex point, for the same coefficient sequences. -/
148 theorem coefficient_series_entire (s : Scales) (hs : s.positive)
149     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (z : ℂ) : s.NormConverges z := by
150   have hQ0 : 0 ≤ s.maxScale := hs.1.le.trans s.maxScale_bounds.1
151   have hlim : Filter.Tendsto (fun n : ℕ => ‖z‖ * s.maxScale ^ n)
152       Filter.atTop (nhds 0) := by
153     simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one hQ0 (s.maxScale_lt_one hstrict)).const_mul ‖z‖
154   obtain ⟨n, hn⟩ := (hlim.eventually_lt_const (by norm_num : (0 : ℝ) < 1)).exists
155   exact s.coefficient_series_on_ladder hs
156     ⟨hstrict.1.le, hstrict.2.1.le, hstrict.2.2.1.le, hstrict.2.2.2.le⟩
157     hQ0 s.maxScale_bounds n z hn.le
158 
159 /-- A summable positive-radius majorant controls each smaller complex point. -/
160 theorem odd_term_norm_le_radius (c : ℕ → ℝ) {R : ℝ} (hR : 0 ≤ R)
161     {z : ℂ} (hz : ‖z‖ ≤ R) (n : ℕ) :
162     ‖(c n : ℂ) * z ^ (2 * n + 1)‖ ≤
163       ‖(c n : ℂ) * (R : ℂ) ^ (2 * n + 1)‖ := by
164   simp only [norm_mul, norm_pow, Complex.norm_of_nonneg hR]
165   exact mul_le_mul_of_nonneg_left
166     (pow_le_pow_left₀ (norm_nonneg z) hz _) (norm_nonneg _)
167 
168 theorem oddSum_differentiableOn_of_radius {c : ℕ → ℝ} {R : ℝ} (hR : 0 ≤ R)
169     (hc : Summable (fun n => ‖(c n : ℂ) * (R : ℂ) ^ (2 * n + 1)‖)) :
170     DifferentiableOn ℂ (oddSum c) (Metric.ball 0 R) := by
171   apply Complex.differentiableOn_tsum_of_summable_norm hc
172   · intro n
173     exact (differentiable_const _ |>.mul (differentiable_id.pow _)).differentiableOn
174   · exact Metric.isOpen_ball
175   · intro n z hz
176     exact odd_term_norm_le_radius c hR (show ‖z‖ < R by simpa using hz).le n
177 
178 theorem oddSum_hasSum_deriv_of_radius {c : ℕ → ℝ} {R : ℝ} (hR : 0 ≤ R)
179     (hc : Summable (fun n => ‖(c n : ℂ) * (R : ℂ) ^ (2 * n + 1)‖))
180     {z : ℂ} (hz : ‖z‖ < R) :
181     HasSum (fun n => (c n : ℂ) * (2 * n + 1) * z ^ (2 * n)) (deriv (oddSum c) z) := by
182   have h := Complex.hasSum_deriv_of_summable_norm hc
183     (fun n => (differentiable_const _ |>.mul (differentiable_id.pow (2 * n + 1))).differentiableOn)
184     Metric.isOpen_ball
185     (fun n w hw => odd_term_norm_le_radius c hR (show ‖w‖ < R by simpa using hw).le n)
186     (show z ∈ Metric.ball 0 R by simpa using hz)
187   convert! h using 1
188   ext n
189   exact (oddTerm_hasDerivAt c n z).deriv.symm
190 
191 theorem oddSum_entire_of_norm_summable {c : ℕ → ℝ}
192     (hc : ∀ z : ℂ, Summable (fun n => ‖(c n : ℂ) * z ^ (2 * n + 1)‖)) :
193     Differentiable ℂ (oddSum c) := by
194   intro z
195   have h := oddSum_differentiableOn_of_radius (c := c)
196     (R := ‖z‖ + 1) (by positivity) (hc (‖z‖ + 1 : ℝ))
197   exact h.differentiableAt (Metric.isOpen_ball.mem_nhds (by simp))
198 
199 theorem coupled_entire (s : Scales) (hs : s.positive)
200     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
201     Differentiable ℂ s.U ∧ Differentiable ℂ s.V :=
202   ⟨oddSum_entire_of_norm_summable (fun z => (s.coefficient_series_entire hs hstrict z).1),
203     oddSum_entire_of_norm_summable (fun z => (s.coefficient_series_entire hs hstrict z).2)⟩
204 
205 theorem oddSum_hasSum_deriv_entire {c : ℕ → ℝ}
206     (hc : ∀ z : ℂ, Summable (fun n => ‖(c n : ℂ) * z ^ (2 * n + 1)‖)) (z : ℂ) :
207     HasSum (fun n => (c n : ℂ) * (2 * n + 1) * z ^ (2 * n)) (deriv (oddSum c) z) :=
208   oddSum_hasSum_deriv_of_radius (R := ‖z‖ + 1) (by positivity)
209     (hc (‖z‖ + 1 : ℝ)) (lt_add_one ‖z‖)
210 
211 /-- The shifted differentiated term is exactly the finite Cauchy coefficient. -/
212 theorem next_derivative_term_eq (c d : ℕ → ℝ) (x y : ℝ) (z : ℂ) (n : ℕ) :
213     (nextCoefficient x y (fun j => (c j, d j)) n : ℂ) *
214       (2 * (n + 1) + 1) * z ^ (2 * (n + 1)) = oddConvolution c d x y z n := by
215   rw [oddConvolution_eq]
216   have h := congrArg (fun t : ℝ => (t : ℂ))
217     (nextCoefficient_mul_denominator x y (fun j => (c j, d j)) n)
218   simp only [Complex.ofReal_mul, Complex.ofReal_add, Complex.ofReal_ofNat,
219     Complex.ofReal_natCast] at h
220   convert congrArg (fun t : ℂ => t * z ^ (2 * n + 2)) h using 1
221   ring
222 
223 theorem oddSum_entire_equation {c d e : ℕ → ℝ}
224     (he : ∀ w : ℂ, Summable (fun n => ‖(e n : ℂ) * w ^ (2 * n + 1)‖))
225     {x y : ℝ} (he0 : e 0 = 1)
226     (hrec : ∀ n, e (n + 1) = nextCoefficient x y (fun j => (c j, d j)) n)
227     (z : ℂ)
228     (hc : Summable (fun n => ‖(c n : ℂ) * ((x : ℂ) * z) ^ (2 * n + 1)‖))
229     (hd : Summable (fun n => ‖(d n : ℂ) * ((y : ℂ) * z) ^ (2 * n + 1)‖)) :
230     deriv (oddSum e) z = 1 + oddSum c ((x : ℂ) * z) * oddSum d ((y : ℂ) * z) := by
231   have hprod : oddSum c ((x : ℂ) * z) * oddSum d ((y : ℂ) * z) =
232       ∑' n, oddConvolution c d x y z n :=
233     tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm
234       (f := fun n => (c n : ℂ) * ((x : ℂ) * z) ^ (2 * n + 1))
235       (g := fun n => (d n : ℂ) * ((y : ℂ) * z) ^ (2 * n + 1)) hc hd
236   have hsum := oddSum_hasSum_deriv_entire he z
237   rw [← hsum.tsum_eq, hsum.summable.tsum_eq_zero_add]
238   simp only [he0, Complex.ofReal_one, Nat.cast_zero, mul_zero, zero_add, pow_zero, mul_one]
239   rw [hprod]
240   congr 1
241   apply tsum_congr
242   intro n
243   rw [hrec]
244   simpa only [Nat.cast_add, Nat.cast_one] using next_derivative_term_eq c d x y z n
245 
246 theorem coupled_entire_equations (s : Scales) (hs : s.positive)
247     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (z : ℂ) :
248     deriv s.U z = 1 + s.U ((s.q : ℂ) * z) * s.V ((s.r : ℂ) * z) ∧
249     deriv s.V z = 1 + s.U ((s.a : ℂ) * z) * s.V ((s.b : ℂ) * z) := by
250   have h0 := s.coefficients_zero
251   constructor
252   · apply oddSum_entire_equation (fun w => (s.coefficient_series_entire hs hstrict w).1)
253       (congrArg Prod.fst h0) _ z
254       (s.coefficient_series_entire hs hstrict _).1 (s.coefficient_series_entire hs hstrict _).2
255     intro n
256     exact congrArg Prod.fst (s.coefficients_solution.2 n)
257   · apply oddSum_entire_equation (fun w => (s.coefficient_series_entire hs hstrict w).2)
258       (congrArg Prod.snd h0) _ z
259       (s.coefficient_series_entire hs hstrict _).1 (s.coefficient_series_entire hs hstrict _).2
260     intro n
261     exact congrArg Prod.snd (s.coefficients_solution.2 n)
262 
263 /-- The constructed pair is an entire normalized solution, without a gluing
264 choice or a hypothesis that the infinite sums already solve the equations. -/
265 theorem coupled_entire_solution (s : Scales) (hs : s.positive)
266     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
267     s.U 0 = 0 ∧ s.V 0 = 0 ∧
268       ∀ z : ℂ,
269         HasDerivAt s.U (1 + s.U ((s.q : ℂ) * z) * s.V ((s.r : ℂ) * z)) z ∧
270         HasDerivAt s.V (1 + s.U ((s.a : ℂ) * z) * s.V ((s.b : ℂ) * z)) z := by
271   refine ⟨oddSum_zero _, oddSum_zero _, ?_⟩
272   intro z
273   have hd := s.coupled_entire hs hstrict
274   exact ⟨(s.coupled_entire_equations hs hstrict z).1 ▸ (hd.1 z).hasDerivAt,
275     (s.coupled_entire_equations hs hstrict z).2 ▸ (hd.2 z).hasDerivAt⟩
276 
277 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls