English
Let f and g be differentiable on the open first quadrant and continuous on its closure, with the same growth control as above. If f and g agree on the boundary of the first quadrant, then they agree on the closed first quadrant.
Русский
Пусть f и g дифференцируемы на открытой первой четверти и непрерывны на её границе, с той же ростовой оценкой. Если f и g совпадают на границе, то они совпадают и на всей замкнутой первой четверти.
LaTeX
$$$$\\forall z \\in \\{w : \\Re w \\ge 0, \\Im w \\ge 0\\}, \\ f(z) = g(z).$$$$
Lean4
/-- **Phragmen-Lindelöf principle** in the first quadrant. Let `f g : ℂ → E` be functions such that
* `f` and `g` are differentiable in the open first quadrant and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open first
quadrant for some `A`, `B`, and `c < 2`;
* `f` is equal to `g` on the boundary of the first quadrant.
Then `f` is equal to `g` on the closed first quadrant. -/
theorem eqOn_quadrant_I (hdf : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0))
(hBf : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * ‖z‖ ^ c))
(hdg : DiffContOnCl ℂ g (Ioi 0 ×ℂ Ioi 0))
(hBg : ∃ c < (2 : ℝ), ∃ B, g =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * ‖z‖ ^ c))
(hre : ∀ x : ℝ, 0 ≤ x → f x = g x) (him : ∀ x : ℝ, 0 ≤ x → f (x * I) = g (x * I)) :
EqOn f g {z | 0 ≤ z.re ∧ 0 ≤ z.im} := fun _z hz =>
sub_eq_zero.1 <|
eq_zero_on_quadrant_I (hdf.sub hdg) (isBigO_sub_exp_rpow hBf hBg) (fun x hx => sub_eq_zero.2 <| hre x hx)
(fun x hx => sub_eq_zero.2 <| him x hx) hz
