English
Under suitable exponential growth bounds, two periodic-ish functions f and g that agree on the boundary are equal on the horizontal strip.
Русский
При условиях экспоненциального роста две функции f и g, сходные к периоду, совпадающие на границе, равны внутри горизонтальной полосы.
LaTeX
$$EqOn f g (im ⁻¹' Ioo a b) under appropriate growth bounds$$
Lean4
/-- An auxiliary lemma that combines two double exponential estimates into a similar estimate
on the difference of the functions. -/
theorem isBigO_sub_exp_exp {a : ℝ} {f g : ℂ → E} {l : Filter ℂ} {u : ℂ → ℝ}
(hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|)))
(hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))) :
∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|)) :=
by
have :
∀ {c₁ c₂ B₁ B₂},
c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ z, ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖ :=
fun hc hB₀ hB z ↦ by simp only [Real.norm_eq_abs, Real.abs_exp]; gcongr
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_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| 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 _ _)]
