CoupledPositiveReal.lean

1 import CoupledCharacteristic
2 import Mathlib.Analysis.Complex.RealDeriv
3 import Mathlib.Analysis.Calculus.Deriv.MeanValue
4 
5 /-! # Positive-real comparisons for the coupled canonical functions
6 
7 All ordered inequalities concern real-valued restrictions. The complex
8 functions are identified with their embeddings on the real axis.
9 -/
10 
11 set_option autoImplicit false
12 set_option maxHeartbeats 1500000
13 
14 noncomputable section
15 
16 open Filter Set
17 open scoped Topology
18 
19 namespace Komorebi.SpecialFunctions.Coupled.Scales
20 
21 def UReal (s : Scales) (x : ℝ) : ℝ := (s.U (x : ℂ)).re
22 def VReal (s : Scales) (x : ℝ) : ℝ := (s.V (x : ℂ)).re
23 
24 theorem real_series_hasSum (s : Scales) (hs : s.positive)
25     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (x : ℝ) :
26     HasSum (fun n => (s.coefficients n).1 * x ^ (2 * n + 1)) (s.UReal x) ∧
27     HasSum (fun n => (s.coefficients n).2 * x ^ (2 * n + 1)) (s.VReal x) := by
28   have h := s.coefficient_series_entire hs hstrict (x : ℂ)
29   constructor
30   · simpa only [UReal, U, oddSum, ← Complex.ofReal_pow, ← Complex.ofReal_mul, Complex.ofReal_re] using
31       Complex.hasSum_re h.1.of_norm.hasSum
32   · simpa only [VReal, V, oddSum, ← Complex.ofReal_pow, ← Complex.ofReal_mul, Complex.ofReal_re] using
33       Complex.hasSum_re h.2.of_norm.hasSum
34 
35 theorem real_axis_identification (s : Scales) (hs : s.positive)
36     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (x : ℝ) :
37     s.U (x : ℂ) = (s.UReal x : ℂ) ∧ s.V (x : ℂ) = (s.VReal x : ℂ) := by
38   have h := s.coefficient_series_entire hs hstrict (x : ℂ)
39   have hr := s.real_series_hasSum hs hstrict x
40   constructor
41   · exact h.1.of_norm.hasSum.unique (by
42       simpa only [Complex.ofReal_mul, Complex.ofReal_pow] using Complex.hasSum_ofReal.mpr hr.1)
43   · exact h.2.of_norm.hasSum.unique (by
44       simpa only [Complex.ofReal_mul, Complex.ofReal_pow] using Complex.hasSum_ofReal.mpr hr.2)
45 
46 theorem real_axis_zero (s : Scales) : s.UReal 0 = 0 ∧ s.VReal 0 = 0 := by
47   simp [UReal, VReal, U, V, oddSum]
48 
49 theorem real_axis_nonneg (s : Scales) (hs : s.positive)
50     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {x : ℝ} (hx : 0 ≤ x) :
51     0 ≤ s.UReal x ∧ 0 ≤ s.VReal x := by
52   have h := s.real_series_hasSum hs hstrict x
53   constructor
54   · rw [← h.1.tsum_eq]
55     exact tsum_nonneg fun n => mul_nonneg (s.coefficients_positive hs n).1.le (pow_nonneg hx _)
56   · rw [← h.2.tsum_eq]
57     exact tsum_nonneg fun n => mul_nonneg (s.coefficients_positive hs n).2.le (pow_nonneg hx _)
58 
59 theorem real_axis_lower_linear (s : Scales) (hs : s.positive)
60     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {x : ℝ} (hx : 0 ≤ x) :
61     x ≤ s.UReal x ∧ x ≤ s.VReal x := by
62   have h := s.real_series_hasSum hs hstrict x
63   constructor
64   · simpa [coefficients_zero] using
65       le_hasSum h.1 0 (fun n _ => mul_nonneg (s.coefficients_positive hs n).1.le (pow_nonneg hx _))
66   · simpa [coefficients_zero] using
67       le_hasSum h.2 0 (fun n _ => mul_nonneg (s.coefficients_positive hs n).2.le (pow_nonneg hx _))
68 
69 theorem real_axis_hasDerivAt (s : Scales) (hs : s.positive)
70     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) (x : ℝ) :
71     HasDerivAt s.UReal (1 + s.UReal (s.q * x) * s.VReal (s.r * x)) x ∧
72     HasDerivAt s.VReal (1 + s.UReal (s.a * x) * s.VReal (s.b * x)) x := by
73   have h := (s.coupled_entire_solution hs hstrict).2.2 (x : ℂ)
74   constructor
75   · apply h.1.real_of_complex.congr_deriv
76     rw [← Complex.ofReal_mul, ← Complex.ofReal_mul,
77       (s.real_axis_identification hs hstrict (s.q * x)).1,
78       (s.real_axis_identification hs hstrict (s.r * x)).2]
79     simp
80   · apply h.2.real_of_complex.congr_deriv
81     rw [← Complex.ofReal_mul, ← Complex.ofReal_mul,
82       (s.real_axis_identification hs hstrict (s.a * x)).1,
83       (s.real_axis_identification hs hstrict (s.b * x)).2]
84     simp
85 
86 theorem real_axis_differentiable (s : Scales) (hs : s.positive)
87     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
88     Differentiable ℝ s.UReal ∧ Differentiable ℝ s.VReal :=
89   ⟨fun x => (s.real_axis_hasDerivAt hs hstrict x).1.differentiableAt,
90     fun x => (s.real_axis_hasDerivAt hs hstrict x).2.differentiableAt⟩
91 
92 theorem real_axis_deriv_ge_one (s : Scales) (hs : s.positive)
93     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {x : ℝ} (hx : 0 ≤ x) :
94     1 ≤ deriv s.UReal x ∧ 1 ≤ deriv s.VReal x := by
95   rw [(s.real_axis_hasDerivAt hs hstrict x).1.deriv,
96     (s.real_axis_hasDerivAt hs hstrict x).2.deriv]
97   have hq := s.real_axis_nonneg hs hstrict (mul_nonneg hs.1.le hx)
98   have hr := s.real_axis_nonneg hs hstrict (mul_nonneg hs.2.1.le hx)
99   have ha := s.real_axis_nonneg hs hstrict (mul_nonneg hs.2.2.1.le hx)
100   have hb := s.real_axis_nonneg hs hstrict (mul_nonneg hs.2.2.2.le hx)
101   constructor
102   · linarith [mul_nonneg hq.1 hr.2]
103   · linarith [mul_nonneg ha.1 hb.2]
104 
105 theorem real_axis_strictMono (s : Scales) (hs : s.positive)
106     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) :
107     StrictMonoOn s.UReal (Ici 0) ∧ StrictMonoOn s.VReal (Ici 0) := by
108   have hd := s.real_axis_differentiable hs hstrict
109   constructor
110   · apply strictMonoOn_of_deriv_pos (convex_Ici 0) hd.1.continuous.continuousOn
111     intro x hx
112     have hx0 : 0 ≤ x := interior_subset hx
113     linarith [(s.real_axis_deriv_ge_one hs hstrict hx0).1]
114   · apply strictMonoOn_of_deriv_pos (convex_Ici 0) hd.2.continuous.continuousOn
115     intro x hx
116     have hx0 : 0 ≤ x := interior_subset hx
117     linarith [(s.real_axis_deriv_ge_one hs hstrict hx0).2]
118 
119 theorem real_axis_log_positive (s : Scales) (hs : s.positive)
120     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {x : ℝ} (hx : 1 < x) :
121     0 < Real.log (s.UReal x) ∧ 0 < Real.log (s.VReal x) := by
122   have h := s.real_axis_lower_linear hs hstrict (by linarith : 0 ≤ x)
123   exact ⟨Real.log_pos (lt_of_lt_of_le hx h.1), Real.log_pos (lt_of_lt_of_le hx h.2)⟩
124 
125 theorem odd_series_norm_le_real_sum {c : ℕ → ℝ} {z A : ℂ} {R F : ℝ}
126     (hc : ∀ n, 0 ≤ c n) (hz : ‖z‖ ≤ R)
127     (hA : HasSum (fun n => (c n : ℂ) * z ^ (2 * n + 1)) A)
128     (hF : HasSum (fun n => c n * R ^ (2 * n + 1)) F) : ‖A‖ ≤ F := by
129   apply hA.norm_le_of_bounded hF
130   intro n
131   rw [norm_mul, Complex.norm_of_nonneg (hc n), norm_pow]
132   exact mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (norm_nonneg z) hz _) (hc n)
133 
134 theorem complex_norm_le_real_axis (s : Scales) (hs : s.positive)
135     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {z : ℂ} {R : ℝ} (hz : ‖z‖ ≤ R) :
136     ‖s.U z‖ ≤ s.UReal R ∧ ‖s.V z‖ ≤ s.VReal R := by
137   have h := s.coefficient_series_entire hs hstrict z
138   have hr := s.real_series_hasSum hs hstrict R
139   exact ⟨odd_series_norm_le_real_sum (fun n => (s.coefficients_positive hs n).1.le) hz
140       h.1.of_norm.hasSum hr.1,
141     odd_series_norm_le_real_sum (fun n => (s.coefficients_positive hs n).2.le) hz
142       h.2.of_norm.hasSum hr.2⟩
143 
144 theorem real_axis_norm (s : Scales) (hs : s.positive)
145     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 0 ≤ R) :
146     ‖s.U (R : ℂ)‖ = s.UReal R ∧ ‖s.V (R : ℂ)‖ = s.VReal R := by
147   have he := s.real_axis_identification hs hstrict R
148   have hp := s.real_axis_nonneg hs hstrict hR
149   rw [he.1, he.2]
150   exact ⟨Complex.norm_of_nonneg hp.1, Complex.norm_of_nonneg hp.2⟩
151 
152 theorem sphere_norm_isGreatest {f : ℂ → ℂ} {R F : ℝ} (hR : 0 ≤ R)
153     (he : ‖f (R : ℂ)‖ = F) (hb : ∀ z, ‖z‖ ≤ R → ‖f z‖ ≤ F) :
154     IsGreatest ((fun z => ‖f z‖) '' Metric.sphere (0 : ℂ) R) F := by
155   constructor
156   · refine ⟨(R : ℂ), ?_, he⟩
157     simpa using hR
158   · rintro y ⟨z, hz, rfl⟩
159     have hzR : ‖z‖ = R := by simpa only [Metric.mem_sphere, dist_zero_right] using hz
160     exact hb z hzR.le
161 
162 theorem maximum_modulus_real_axis (s : Scales) (hs : s.positive)
163     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 0 ≤ R) :
164     IsGreatest ((fun z => ‖s.U z‖) '' Metric.sphere (0 : ℂ) R) (s.UReal R) ∧
165     IsGreatest ((fun z => ‖s.V z‖) '' Metric.sphere (0 : ℂ) R) (s.VReal R) := by
166   have he := s.real_axis_norm hs hstrict hR
167   exact ⟨sphere_norm_isGreatest hR he.1 (fun z hz => (s.complex_norm_le_real_axis hs hstrict hz).1),
168     sphere_norm_isGreatest hR he.2 (fun z hz => (s.complex_norm_le_real_axis hs hstrict hz).2)⟩
169 
170 /-- Mean-value comparison on a unit interval; inequalities stay in the real field. -/
171 theorem unit_shift_lower_from_deriv {f g h : ℝ → ℝ} {p q R : ℝ}
172     (hf : Differentiable ℝ f) (hf0 : ∀ x, 0 ≤ x → 0 ≤ f x)
173     (hg0 : ∀ x, 0 ≤ x → 0 ≤ g x) (hh0 : ∀ x, 0 ≤ x → 0 ≤ h x)
174     (hgm : MonotoneOn g (Ici 0)) (hhm : MonotoneOn h (Ici 0))
175     (hd : ∀ x, deriv f x = 1 + g (p * x) * h (q * x))
176     (hp : 0 ≤ p) (hq : 0 ≤ q) (hR : 1 ≤ R) :
177     g (p * (R - 1)) * h (q * (R - 1)) ≤ f R := by
178   have hR0 : 0 ≤ R - 1 := by linarith
179   have hbound : ∀ x ∈ interior (Icc (R - 1) R),
180       g (p * (R - 1)) * h (q * (R - 1)) ≤ deriv f x := by
181     intro x hx
182     have hxI : x ∈ Icc (R - 1) R := interior_subset hx
183     have hx0 : 0 ≤ x := le_trans hR0 hxI.1
184     have hgp := hgm (mul_nonneg hp hR0) (mul_nonneg hp hx0)
185       (mul_le_mul_of_nonneg_left hxI.1 hp)
186     have hhq := hhm (mul_nonneg hq hR0) (mul_nonneg hq hx0)
187       (mul_le_mul_of_nonneg_left hxI.1 hq)
188     have hm := mul_le_mul hgp hhq (hh0 _ (mul_nonneg hq hR0)) (hg0 _ (mul_nonneg hp hx0))
189     rw [hd x]
190     linarith only [hm]
191   have hcomp := (convex_Icc (R - 1) R).mul_sub_le_image_sub_of_le_deriv
192     hf.continuous.continuousOn hf.differentiableOn hbound
193     (R - 1) ⟨le_rfl, by linarith⟩ R ⟨by linarith, le_rfl⟩ (by linarith)
194   have hn := hf0 (R - 1) hR0
195   nlinarith only [hcomp, hn]
196 
197 theorem real_axis_unit_lower (s : Scales) (hs : s.positive)
198     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 1 ≤ R) :
199     s.UReal (s.q * (R - 1)) * s.VReal (s.r * (R - 1)) ≤ s.UReal R ∧
200     s.UReal (s.a * (R - 1)) * s.VReal (s.b * (R - 1)) ≤ s.VReal R := by
201   have hd := s.real_axis_differentiable hs hstrict
202   have hm := s.real_axis_strictMono hs hstrict
203   have hu0 : ∀ x : ℝ, 0 ≤ x → 0 ≤ s.UReal x :=
204     fun x hx => (s.real_axis_nonneg hs hstrict hx).1
205   have hv0 : ∀ x : ℝ, 0 ≤ x → 0 ≤ s.VReal x :=
206     fun x hx => (s.real_axis_nonneg hs hstrict hx).2
207   exact ⟨unit_shift_lower_from_deriv hd.1 hu0 hu0 hv0 hm.1.monotoneOn hm.2.monotoneOn
208       (fun x => (s.real_axis_hasDerivAt hs hstrict x).1.deriv) hs.1.le hs.2.1.le hR,
209     unit_shift_lower_from_deriv hd.2 hv0 hu0 hv0 hm.1.monotoneOn hm.2.monotoneOn
210       (fun x => (s.real_axis_hasDerivAt hs hstrict x).2.deriv) hs.2.2.1.le hs.2.2.2.le hR⟩
211 
212 theorem real_axis_log_unit_lower (s : Scales) (hs : s.positive)
213     (hstrict : s.q < 1 ∧ s.r < 1 ∧ s.a < 1 ∧ s.b < 1) {R : ℝ} (hR : 1 < R) :
214     Real.log (s.UReal (s.q * (R - 1))) + Real.log (s.VReal (s.r * (R - 1))) ≤
215       Real.log (s.UReal R) ∧
216     Real.log (s.UReal (s.a * (R - 1))) + Real.log (s.VReal (s.b * (R - 1))) ≤
217       Real.log (s.VReal R) := by
218   have hp : 0 < R - 1 := by linarith
219   have hq0 := mul_pos hs.1 hp
220   have hr0 := mul_pos hs.2.1 hp
221   have ha0 := mul_pos hs.2.2.1 hp
222   have hb0 := mul_pos hs.2.2.2 hp
223   have huq := lt_of_lt_of_le hq0 (s.real_axis_lower_linear hs hstrict hq0.le).1
224   have hvr := lt_of_lt_of_le hr0 (s.real_axis_lower_linear hs hstrict hr0.le).2
225   have hua := lt_of_lt_of_le ha0 (s.real_axis_lower_linear hs hstrict ha0.le).1
226   have hvb := lt_of_lt_of_le hb0 (s.real_axis_lower_linear hs hstrict hb0.le).2
227   have hc := s.real_axis_unit_lower hs hstrict hR.le
228   have h1 := Real.log_le_log (mul_pos huq hvr) hc.1
229   have h2 := Real.log_le_log (mul_pos hua hvb) hc.2
230   rw [Real.log_mul (ne_of_gt huq) (ne_of_gt hvr)] at h1
231   rw [Real.log_mul (ne_of_gt hua) (ne_of_gt hvb)] at h2
232   exact ⟨h1, h2⟩
233 
234 def minScale (s : Scales) : ℝ := min (min s.q s.r) (min s.a s.b)
235 def lowerThreshold (s : Scales) : ℝ := 1 + 2 / s.minScale
236 
237 theorem minScale_bounds (s : Scales) :
238     s.minScale ≤ s.q ∧ s.minScale ≤ s.r ∧ s.minScale ≤ s.a ∧ s.minScale ≤ s.b := by
239   exact ⟨(min_le_left _ _).trans (min_le_left _ _),
240     (min_le_left _ _).trans (min_le_right _ _),
241     (min_le_right _ _).trans (min_le_left _ _),
242     (min_le_right _ _).trans (min_le_right _ _)⟩
243 
244 theorem minScale_positive (s : Scales) (hs : s.positive) : 0 < s.minScale :=
245   lt_min (lt_min hs.1 hs.2.1) (lt_min hs.2.2.1 hs.2.2.2)
246 
247 theorem lowerThreshold_gt_one (s : Scales) (hs : s.positive) : 1 < s.lowerThreshold := by
248   have hm := s.minScale_positive hs
249   dsimp [lowerThreshold]
250   linarith [div_pos (by norm_num : (0 : ℝ) < 2) hm]
251 
252 theorem lower_child_radii (s : Scales) (hs : s.positive) {R : ℝ} (hR : s.lowerThreshold ≤ R) :
253     2 ≤ s.q * (R - 1) ∧ 2 ≤ s.r * (R - 1) ∧
254     2 ≤ s.a * (R - 1) ∧ 2 ≤ s.b * (R - 1) := by
255   have hm := s.minScale_positive hs
256   have hR0 : 0 ≤ R - 1 := by linarith [s.lowerThreshold_gt_one hs]
257   have hdiv : 2 / s.minScale ≤ R - 1 := by dsimp [lowerThreshold] at hR; linarith
258   have htwo : 2 ≤ s.minScale * (R - 1) := by
259     calc
260       2 = s.minScale * (2 / s.minScale) := by field_simp [ne_of_gt hm]
261       _ ≤ s.minScale * (R - 1) := mul_le_mul_of_nonneg_left hdiv hm.le
262   have hb := s.minScale_bounds
263   exact ⟨htwo.trans (mul_le_mul_of_nonneg_right hb.1 hR0),
264     htwo.trans (mul_le_mul_of_nonneg_right hb.2.1 hR0),
265     htwo.trans (mul_le_mul_of_nonneg_right hb.2.2.1 hR0),
266     htwo.trans (mul_le_mul_of_nonneg_right hb.2.2.2 hR0)⟩
267 
268 end Komorebi.SpecialFunctions.Coupled.Scales

Back to source controls