Lean4
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`.
Let `f : ℂ → E` be a function such that
* `f` is differentiable on `U` and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * exp(c * |re z|))` on `U` for some `c < π / (b - a)`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of `U`.
Then `‖f z‖` is bounded by the same constant on the closed strip
`{z : ℂ | a ≤ im z ≤ b}`. Moreover, it suffices to verify the second assumption
only for sufficiently large values of `|re z|`.
-/
theorem horizontal_strip (hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b))
(hB :
∃ c < π / (b - a),
∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|)))
(hle_a : ∀ z : ℂ, im z = a → ‖f z‖ ≤ C) (hle_b : ∀ z, im z = b → ‖f z‖ ≤ C) (hza : a ≤ im z) (hzb : im z ≤ b) :
‖f z‖ ≤ C := by
-- If `im z = a` or `im z = b`, then we apply `hle_a` or `hle_b`, otherwise `im z ∈ Ioo a b`.
rw [le_iff_eq_or_lt] at hza hzb
rcases hza with hza | hza; · exact hle_a _ hza.symm
rcases hzb with hzb | hzb; · exact hle_b _ hzb
wlog hC₀ : 0 < C generalizing C
· refine le_of_forall_gt_imp_ge_of_dense fun C' hC' => this (fun w hw => ?_) (fun w hw => ?_) ?_
· exact (hle_a _ hw).trans hC'.le
· exact (hle_b _ hw).trans hC'.le
· refine ((norm_nonneg (f (a * I))).trans (hle_a _ ?_)).trans_lt hC'
rw [mul_I_im, ofReal_re]
-- After a change of variables, we deal with the strip `a - b < im z < a + b` instead
-- of `a < im z < b`
obtain ⟨a, b, rfl, rfl⟩ : ∃ a' b', a = a' - b' ∧ b = a' + b' := ⟨(a + b) / 2, (b - a) / 2, by ring, by ring⟩
have hab : a - b < a + b := hza.trans hzb
have hb : 0 < b := by simpa only [sub_eq_add_neg, add_lt_add_iff_left, neg_lt_self_iff] using hab
rw [add_sub_sub_cancel, ← two_mul, div_mul_eq_div_div] at hB
have hπb : 0 < π / 2 / b := div_pos Real.pi_div_two_pos hb
rcases hB with ⟨c, hc, B, hO⟩
obtain ⟨d, ⟨hcd, hd₀⟩, hd⟩ : ∃ d, (c < d ∧ 0 < d) ∧ d < π / 2 / b := by
simpa only [max_lt_iff] using exists_between (max_lt hc hπb)
have hb' : d * b < π / 2 := (lt_div_iff₀ hb).1 hd
set aff := (fun w => d * (w - a * I) : ℂ → ℂ)
set g := fun (ε : ℝ) (w : ℂ) =>
exp
(ε * (exp (aff w) + exp (-aff w)))
/- Since `g ε z → 1` as `ε → 0⁻`, it suffices to prove that `‖g ε z • f z‖ ≤ C`
for all negative `ε`. -/
suffices ∀ᶠ ε : ℝ in 𝓝[<] (0 : ℝ), ‖g ε z • f z‖ ≤ C
by
refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
apply ((continuous_ofReal.mul continuous_const).cexp.smul continuous_const).norm.tendsto'
simp
filter_upwards [self_mem_nhdsWithin] with ε ε₀; change ε < 0 at ε₀
obtain ⟨δ, δ₀, hδ⟩ : ∃ δ : ℝ, δ < 0 ∧ ∀ ⦃w⦄, im w ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |re w|)) :=
by
refine
⟨ε * Real.cos (d * b),
mul_neg_of_neg_of_pos ε₀ (Real.cos_pos_of_mem_Ioo <| abs_lt.1 <| (abs_of_pos (mul_pos hd₀ hb)).symm ▸ hb'),
fun w hw => ?_⟩
replace hw : |im (aff w)| ≤ d * b :=
by
rw [← Real.closedBall_eq_Icc, mem_closedBall, Real.dist_eq] at hw
rw [im_ofReal_mul, sub_im, mul_I_im, ofReal_re, _root_.abs_mul, abs_of_pos hd₀]
gcongr
simpa only [aff, re_ofReal_mul, _root_.abs_mul, abs_of_pos hd₀, sub_re, mul_I_re, ofReal_im, zero_mul, neg_zero,
sub_zero] using norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le ε₀.le hw hb'.le
have hg₁ : ∀ w, im w = a - b ∨ im w = a + b → ‖g ε w‖ ≤ 1 :=
by
refine fun w hw => (hδ <| hw.by_cases ?_ ?_).trans (Real.exp_le_one_iff.2 ?_)
exacts [fun h => h.symm ▸ left_mem_Icc.2 hab.le, fun h => h.symm ▸ right_mem_Icc.2 hab.le,
mul_nonpos_of_nonpos_of_nonneg δ₀.le (Real.exp_pos _).le]
/- Our a priori estimate on `f` implies that `g ε w • f w → 0` as `|w.re| → ∞` along the strip. In
particular, its norm is less than or equal to `C` for sufficiently large `|w.re|`. -/
obtain ⟨R, hzR, hR⟩ : ∃ R : ℝ, |z.re| < R ∧ ∀ w, |re w| = R → im w ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C :=
by
refine ((eventually_gt_atTop _).and ?_).exists
rcases hO.exists_pos with ⟨A, hA₀, hA⟩
simp only [isBigOWith_iff, eventually_inf_principal, eventually_comap, mem_Ioo, mem_preimage, (· ∘ ·),
Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] at hA
suffices Tendsto (fun R => expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
by
filter_upwards [this.eventually (ge_mem_nhds hC₀), hA] with R hR Hle w hre him
calc
‖g ε w • f w‖ ≤ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) := ?_
_ ≤ C := hR
rw [norm_smul, Real.exp_add, ← hre, Real.exp_add, Real.exp_log hA₀, mul_assoc, mul_comm _ A]
gcongr
exacts [hδ <| Ioo_subset_Icc_self him, Hle _ hre him]
refine Real.tendsto_exp_atBot.comp ?_
suffices H : Tendsto (fun R => δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0))
by
rw [mul_zero, add_zero] at H
refine Tendsto.atBot_add ?_ tendsto_const_nhds
simpa only [id, (· ∘ ·), add_mul, mul_assoc, ← div_eq_inv_mul, ← Real.exp_sub, ← sub_mul, sub_sub_cancel] using
H.neg_mul_atTop δ₀ <| Real.tendsto_exp_atTop.comp <| tendsto_id.const_mul_atTop hd₀
refine tendsto_const_nhds.add (tendsto_const_nhds.mul ?_)
exact tendsto_inv_atTop_zero.comp <| Real.tendsto_exp_atTop.comp <| tendsto_id.const_mul_atTop (sub_pos.2 hcd)
have hR₀ : 0 < R := (_root_.abs_nonneg _).trans_lt hzR
have hgd : Differentiable ℂ (g ε) :=
((((differentiable_id.sub_const _).const_mul _).cexp.add
((differentiable_id.sub_const _).const_mul _).neg.cexp).const_mul
_).cexp
replace hd : DiffContOnCl ℂ (fun w => g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b)) :=
(hgd.diffContOnCl.smul hfd).mono inter_subset_right
convert norm_le_of_forall_mem_frontier_norm_le ((isBounded_Ioo _ _).reProdIm (isBounded_Ioo _ _)) hd (fun w hw => _) _
· rw [frontier_reProdIm, closure_Ioo (neg_lt_self hR₀).ne, frontier_Ioo hab, closure_Ioo hab.ne,
frontier_Ioo (neg_lt_self hR₀)] at hw
by_cases him : w.im = a - b ∨ w.im = a + b
· rw [norm_smul, ← one_mul C]
exact mul_le_mul (hg₁ _ him) (him.by_cases (hle_a _) (hle_b _)) (norm_nonneg _) zero_le_one
· replace hw : w ∈ {-R, R} ×ℂ Icc (a - b) (a + b) := hw.resolve_left fun h ↦ him h.2
have hw' := eq_endpoints_or_mem_Ioo_of_mem_Icc hw.2; rw [← or_assoc] at hw'
exact hR _ ((abs_eq hR₀.le).2 hw.1.symm) (hw'.resolve_left him)
· rw [closure_reProdIm, closure_Ioo hab.ne, closure_Ioo (neg_lt_self hR₀).ne]
exact ⟨abs_le.1 hzR.le, ⟨hza.le, hzb.le⟩⟩
