English
From a weak FE-pair, we obtain a strong FE-pair by the explicit piecewise definitions of f and g via f_modif and g_modif with corrected asymptotics; the strong FE axioms follow.
Русский
Из слабой FE-пары получаем сильную FE-пару через явные кусочно-заданные функции f и g, заданные через f_modif и g_modif с поправленными асимптотиками; свойства сильной FE-пары следуют.
LaTeX
$$WeakFEPair.toStrongFEPair$$
Lean4
theorem hf_modif_FE (x : ℝ) (hx : 0 < x) : P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x :=
by
rcases lt_trichotomy 1 x with hx' | rfl | hx'
· have : 1 / x < 1 := by rwa [one_div_lt hx one_pos, div_one]
rw [f_modif, Pi.add_apply, indicator_of_notMem (notMem_Ioi.mpr this.le), zero_add,
indicator_of_mem (mem_Ioo.mpr ⟨div_pos one_pos hx, this⟩), g_modif, Pi.add_apply,
indicator_of_mem (mem_Ioi.mpr hx'), indicator_of_notMem (notMem_Ioo_of_ge hx'.le), add_zero, P.h_feq _ hx,
smul_sub]
simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]
· simp [f_modif, g_modif]
· have : 1 < 1 / x := by rwa [lt_one_div one_pos hx, div_one]
rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr this), indicator_of_notMem (notMem_Ioo_of_ge this.le),
g_modif, Pi.add_apply, indicator_of_notMem (notMem_Ioi.mpr hx'.le), indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩),
P.h_feq _ hx]
simp_rw [rpow_neg hx.le]
match_scalars <;> field_simp [(rpow_pos_of_pos hx P.k).ne', P.hε]
