eqOn_horizontal_strip — Mathlib

English

If f and g admit two double-exponential bounds with exponents c and B, then f−g satisfies a similar bound.

Русский

Если f и g имеют два двойно экспоненциальных ограничения с показателями c и B, то f−g удовлетворяет сходному пределу.

LaTeX

$$$\exists c

Lean4

/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`.
Let `f g : ℂ → E` be functions such that

* `f` and `g` are differentiable on `U` and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * exp(c * |re z|))` on `U` for some
  `c < π / (b - a)`;
* `f z = g z` on the boundary of `U`.

Then `f` is equal to `g` on the closed strip `{z : ℂ | a ≤ im z ≤ b}`.
-/
theorem eqOn_horizontal_strip {g : ℂ → E} (hdf : DiffContOnCl ℂ f (im ⁻¹' Ioo a b))
    (hBf :
      ∃ c < π / (b - a),
        ∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|)))
    (hdg : DiffContOnCl ℂ g (im ⁻¹' Ioo a b))
    (hBg :
      ∃ c < π / (b - a),
        ∃ B, g =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|)))
    (ha : ∀ z : ℂ, z.im = a → f z = g z) (hb : ∀ z : ℂ, z.im = b → f z = g z) : EqOn f g (im ⁻¹' Icc a b) :=
  fun _z hz =>
  sub_eq_zero.1
    (eq_zero_on_horizontal_strip (hdf.sub hdg) (isBigO_sub_exp_exp hBf hBg) (fun w hw => sub_eq_zero.2 (ha w hw))
      (fun w hw => sub_eq_zero.2 (hb w hw)) hz)

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