English
A precise EqOn identity expresses that the difference f_modif − f + f0 equals a combination of the two indicator-modified pieces on (0,1) and at 1, i.e., the adjustment aligns with f and g₀ on (0,∞).
Русский
Точная идентичность EqOn выражает, что разность f_modif − f + f0 равна сумме двух индикаторно-модифицированных частей на (0,1) и в точке 1, что согласуется с f и g₀ на (0,∞).
LaTeX
$$f_modif_aux1 : EqOn (fun x => f_modif x − f x + f0) ( (Ioo 0 1).indicator (fun x => f0 − (ε * x^(−k)) • g0) + {1}.indicator (fun _ => f0 − f 1) ) (Ioi 0)$$
Lean4
/-- Piecewise modified version of `f` with optimal asymptotics. We deliberately choose intervals
which don't quite join up, so the function is `0` at `x = 1`, in order to maintain symmetry;
there is no "good" choice of value at `1`. -/
def f_modif : ℝ → E :=
(Ioi 1).indicator (fun x ↦ P.f x - P.f₀) + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀)
