theorem
Section10.liminf_div_lt_top_of_lipschitzRelativeTo_univ
{n : ℕ}
{g : EuclideanSpace ℝ (Fin n) → ℝ}
(hg : Function.LipschitzRelativeTo g Set.univ)
(y : EuclideanSpace ℝ (Fin n))
:
A Lipschitz function on univ has at most linear growth along rays, hence
liminf_{t → ∞} g (t • y) / t < ⊤.
theorem
Section10.liminf_div_lt_top_of_le_and_lipschitzRelativeTo_univ
{n : ℕ}
{f g : EuclideanSpace ℝ (Fin n) → ℝ}
(hglip : Function.LipschitzRelativeTo g Set.univ)
(hfg : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ≤ g x)
(y : EuclideanSpace ℝ (Fin n))
:
If f ≤ g and g is Lipschitz on univ, then the growth condition
liminf_{t → ∞} f (t • y) / t < ⊤ also holds for f.
theorem
convexOn_lipschitzRelativeTo_univ_of_le_of_lipschitzRelativeTo
{n : ℕ}
{f g : EuclideanSpace ℝ (Fin n) → ℝ}
(hgconv : ConvexOn ℝ Set.univ g)
(hglip : Function.LipschitzRelativeTo g Set.univ)
(hfconv : ConvexOn ℝ Set.univ f)
(hfg : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ≤ g x)
:
Corollary 10.5.2. Let g be any finite convex function Lipschitzian relative to ℝ^n
(for instance, g(x) = α ‖x‖ + β with α > 0). Then every finite convex function f such that
f ≤ g is likewise Lipschitzian relative to ℝ^n.
def
Function.EquiLipschitzRelativeTo
{n : ℕ}
{I : Type u_1}
(f : I → EuclideanSpace ℝ (Fin n) → ℝ)
(S : Set (EuclideanSpace ℝ (Fin n)))
:
Definition 10.5.3. Let S ⊆ ℝ^n and let {f i | i ∈ I} be a family of real-valued functions
defined on S. The family is equi-Lipschitzian relative to S if there exists a constant
α ≥ 0 such that
|f i y - f i x| ≤ α * ‖y - x‖ for all x ∈ S, y ∈ S, and all indices i.
Equations
- Function.EquiLipschitzRelativeTo f S = ∃ (K : NNReal), ∀ (i : I), LipschitzOnWith K (f i) S