English
Given a Frechet derivative along a filter, a reversed subtraction bound holds on the product space.
Русский
Если есть производная Фреше вдоль фильтра, выполняется обратное bound-отношение разности на произведённом пространстве.
LaTeX
$$HasFDerivAtFilter f f' x L → ∀ {C : NNReal}, AntilipschitzWith C f' → (fun p => p.1 - p.2) =O[L] (fun p => f p.1 - f p.2)$$
Lean4
theorem isBigO_sub_rev (hf : HasFDerivAtFilter f f' x L) {C} (hf' : AntilipschitzWith C f') :
(fun x' => x' - x) =O[L] fun x' => f x' - f x :=
have : (fun x' => x' - x) =O[L] fun x' => f' (x' - x) :=
isBigO_iff.2 ⟨C, Eventually.of_forall fun _ => ZeroHomClass.bound_of_antilipschitz f' hf' _⟩
(this.trans (hf.isLittleO.trans_isBigO this).right_isBigO_add).congr (fun _ => rfl) fun _ => sub_add_cancel _ _
