PolynomialStrip.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial strip growth from finite order and polynomial boundary bounds. The finite-order hypothesis is much weaker than the conclusion; the proof uses the Phragmén–Lindelöf theorem in mathlib.

def OAI.CubicFirstMoment.FiniteVerticalOrder line 15
Source documentation
A finite-order bound restricted to a closed vertical strip.
```
def FiniteVerticalOrder (f : ℂ → ℂ) (a b : ℝ) : Prop :=
…
```
lemma OAI.CubicFirstMoment.finiteVerticalOrder_double_exp line 19
lemma OAI.CubicFirstMoment.strip_shift_norm_lower line 48
lemma OAI.CubicFirstMoment.strip_shift_norm_upper line 54

theorem OAI.CubicFirstMoment.polynomial_strip_of_finite_order line 64

Source documentation

A finite-order holomorphic function with polynomial bounds on both vertical edges has polynomial growth throughout the strip.

theorem polynomial_strip_of_finite_order {f : ℂ → ℂ} {a b C : ℝ}
    (hab : a < b) (hfd : Differentiable ℂ f) (hf : FiniteVerticalOrder f a b)
    (hC : 0 ≤ C) (n : ℕ)
    (ha : ∀ z : ℂ, z.re = a → ‖f z‖ ≤ C*(1+|z.im|)^n)
    (hb : ∀ z : ℂ, z.re = b → ‖f z‖ ≤ C*(1+|z.im|)^n) :
    ∀ z : ℂ, z.re ∈ Icc a b →
      ‖f z‖ ≤ (C*2^n*(b-a+1)^n)*(1+|z.im|)^n := by
…

Mentions: OAI.CubicFirstMoment.FiniteVerticalOrder