quadrant_IV — Mathlib

English

Let f satisfy a P-L growth bound in the open fourth quadrant and be bounded on its boundary; then ∥f(z)∥ ≤ C on the closed fourth quadrant.

Русский

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

LaTeX

$$$$\\forall z \\in \\{ \\Re z \\ge 0, \\Im z \\le 0 \\}, \\ ∥f(z)∥ ≤ C.$$$$

Lean4

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

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

Then `‖f z‖` is bounded from above by the same constant on the closed fourth quadrant. -/
theorem quadrant_IV (hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0))
    (hB : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * ‖z‖ ^ c))
    (hre : ∀ x : ℝ, 0 ≤ x → ‖f x‖ ≤ C) (him : ∀ x : ℝ, x ≤ 0 → ‖f (x * I)‖ ≤ C) (hz_re : 0 ≤ z.re) (hz_im : z.im ≤ 0) :
    ‖f z‖ ≤ C := by
  obtain ⟨z, rfl⟩ : ∃ z', -z' = z := ⟨-z, neg_neg z⟩
  simp only [neg_re, neg_im, neg_nonpos, neg_nonneg] at hz_re hz_im
  change ‖(f ∘ Neg.neg) z‖ ≤ C
  have H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, neg_pos, mem_Ioi, mem_Iio] using hw
  refine quadrant_II (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_) hz_re hz_im
  · rcases hB with ⟨c, hc, B, hO⟩
    refine ⟨c, hc, B, ?_⟩
    simpa only [Function.comp_def, norm_neg] using hO.comp_tendsto (tendsto_neg_cobounded.inf H.tendsto)
  · rw [comp_apply, ← ofReal_neg]
    exact hre (-x) (neg_nonneg.2 hx)
  · rw [comp_apply, ← neg_mul, ← ofReal_neg]
    exact him (-x) (neg_nonpos.2 hx)

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