English
The Mellin transform of the combination f_modif − f + f0, evaluated at s, decomposes into a sum of two simple terms: (1/s) f0 plus ε/(k−s) g0, reflecting the pole structure at s = 0 and s = k.
Русский
Mp=Mellin(f_modif − f + f0) распадается на сумму двух простых членов: (1/s) f0 плюс ε/(k−s) g0, отражая полюсы в s=0 и s=k.
LaTeX
$$mellin (fun x => f_modif x - f x + f0) s = (1 / s) • f0 + (ε / (k - s)) • g0$$
Lean4
theorem f_modif_aux1 :
EqOn (fun x ↦ P.f_modif x - P.f x + P.f₀)
((Ioo 0 1).indicator (fun x : ℝ ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) +
({ 1 } : Set ℝ).indicator (fun _ ↦ P.f₀ - P.f 1))
(Ioi 0) :=
by
intro x (hx : 0 < x)
simp_rw [f_modif, Pi.add_apply]
rcases lt_trichotomy x 1 with hx' | rfl | hx'
· simp_rw [indicator_of_notMem (notMem_Ioi.mpr hx'.le), indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩),
indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne)]
abel
· simp [add_comm, sub_eq_add_neg]
· simp_rw [indicator_of_mem (mem_Ioi.mpr hx'), indicator_of_notMem (notMem_Ioo_of_ge hx'.le),
indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne')]
abel
