English
If for every b, f a b is Kα-Lipschitz in a and for every a, f a is Kβ-Lipschitz in b, then the uncurry f is Lipschitz with Kα + Kβ.
Русский
Если для каждого b отображение a ↦ f a b липшицево с константой Kα, а для каждого a отображение b ↦ f a b липшицево с константой Kβ, то функция uncurry f: (a,b) ↦ f a b липшицева с константой Kα + Kβ.
LaTeX
$$$\\text{LipschitzWith } (K_\\alpha + K_\\beta) (\\mathrm{Function.uncurry} f)$$$
Lean4
protected theorem uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, LipschitzWith Kα fun a => f a b)
(hβ : ∀ a, LipschitzWith Kβ (f a)) : LipschitzWith (Kα + Kβ) (Function.uncurry f) :=
by
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
simp only [Function.uncurry, ENNReal.coe_add, add_mul]
apply le_trans (edist_triangle _ (f a₂ b₁) _)
exact
add_le_add (le_trans (hα _ _ _) <| mul_right_mono <| le_max_left _ _)
(le_trans (hβ _ _ _) <| mul_right_mono <| le_max_right _ _)
