English
If hf is a superpolynomial decay for f and f and g agree at every point, then g also has superpolynomial decay with the same k and l.
Русский
Если hf задаёт сверхполиномиальное затухание для f и если для всех x выполняется f(x) = g(x), то и g имеет сверхполиномиальное затухание.
LaTeX
$$$\mathrm{SuperpolynomialDecay}(l,k,f) \wedge (\forall x, f(x)=g(x)) \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,g)$$$
Lean4
theorem congr (hf : SuperpolynomialDecay l k f) (hfg : ∀ x, f x = g x) : SuperpolynomialDecay l k g := fun z =>
(hf z).congr fun x => (congr_arg fun a => k x ^ z * a) <| hfg x