English
From a weak FE-pair, one constructs a strong FE-pair by taking f_modif and g_modif as the new f and g, with zero f0 and g0, and preserving integral and asymptotic properties; the resulting object satisfies the strong FE axioms.
Русский
Из слабой FE-пары строят сильную FE-пару, взяв f_modif и g_modif в качестве новых f и g, нулевые f0 и g0 и сохранив интегрируемость и асимптотические свойства; полученный объект удовлетворяет условиям сильной FE-пары.
LaTeX
$$toStrongFEPair : WeakFEPair E → StrongFEPair E$$
Lean4
/-- Piecewise modified version of `g` with optimal asymptotics. -/
def g_modif : ℝ → E :=
(Ioi 1).indicator (fun x ↦ P.g x - P.g₀) + (Ioo 0 1).indicator (fun x ↦ P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀)
