quadrant_II — Mathlib

English

Let f satisfy a P-L growth bound in the open second quadrant, and assume ∥f(z)∥ ≤ C on the boundary of the second quadrant. Then ∥f(z)∥ ≤ C on the closed second quadrant.

Русский

Пусть f удовлетворяет ростовой условиП Линдельф в открытой второй четверти, а на границе второй четверти имеет верхнюю границу ∥f(z)∥ ≤ C. Тогда ∥f(z)∥ ≤ C на всей закрытой второй четверти.

LaTeX

$$$$\\forall z: \\Re z \\le 0, \\Im z \\ge 0, \\ ‖f(z)‖ ≤ C.$$$$

Lean4

/-- **Phragmen-Lindelöf principle** in the second quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open second quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open second quadrant
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the second quadrant.

Then `‖f z‖` is bounded from above by the same constant on the closed second quadrant. -/
theorem quadrant_II (hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0))
    (hB : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ‖z‖ ^ c))
    (hre : ∀ x : ℝ, x ≤ 0 → ‖f x‖ ≤ C) (him : ∀ x : ℝ, 0 ≤ x → ‖f (x * I)‖ ≤ C) (hz_re : z.re ≤ 0) (hz_im : 0 ≤ z.im) :
    ‖f z‖ ≤ C := by
  obtain ⟨z, rfl⟩ : ∃ z', z' * I = z := ⟨z / I, div_mul_cancel₀ _ I_ne_zero⟩
  simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im
  change ‖(f ∘ (· * I)) z‖ ≤ C
  have H : MapsTo (· * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using hw.symm
  rcases hB with ⟨c, hc, B, hO⟩
  refine
    quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him (fun x hx => ?_) hz_im hz_re
  ·
    simpa only [Function.comp_def, norm_mul, norm_I, mul_one] using
      hO.comp_tendsto ((tendsto_mul_right_cobounded I_ne_zero).inf H.tendsto)
  · rw [comp_apply, mul_assoc, I_mul_I, mul_neg_one, ← ofReal_neg]
    exact hre _ (neg_nonpos.2 hx)

Похожие утверждения