English
If boundary values of f and g match and the growth bounds hold, then f ≡ g on the horizontal strip closure.
Русский
Если значения на границе совпадают и существуют ростовые пределы, то f совпадает с g на замкнутой горизонтальной полосе.
LaTeX
$$EqOn f g (im ⁻¹' Icc a b)$$
Lean4
/-- An auxiliary lemma that combines two “exponential of a power” estimates into a similar estimate
on the difference of the functions. -/
theorem isBigO_sub_exp_rpow {a : ℝ} {f g : ℂ → E} {l : Filter ℂ}
(hBf : ∃ c < a, ∃ B, f =O[cobounded ℂ ⊓ l] fun z => expR (B * ‖z‖ ^ c))
(hBg : ∃ c < a, ∃ B, g =O[cobounded ℂ ⊓ l] fun z => expR (B * ‖z‖ ^ c)) :
∃ c < a, ∃ B, (f - g) =O[cobounded ℂ ⊓ l] fun z => expR (B * ‖z‖ ^ c) :=
by
have :
∀ {c₁ c₂ B₁ B₂ : ℝ},
c₁ ≤ c₂ →
0 ≤ B₂ → B₁ ≤ B₂ → (fun z : ℂ => expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z => expR (B₂ * ‖z‖ ^ c₂) :=
fun hc hB₀ hB ↦
.of_norm_eventuallyLE <|
by
filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
simp only [Real.norm_eq_abs, Real.abs_exp]
gcongr; assumption
rcases hBf with ⟨cf, hcf, Bf, hOf⟩; rcases hBg with ⟨cg, hcg, Bg, hOg⟩
refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩
refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)
exacts [le_max_left _ _, le_max_left _ _, (le_max_left _ _).trans (le_max_right _ _), le_max_right _ _,
le_max_left _ _, (le_max_right _ _).trans (le_max_right _ _)]
