Lipschitz function. Given two metric spaces (X, dX ) and (Y, dY ), a function f : X → Y is
Lipschitz continuous if there exists K > 0 such that for all x1 , x2 ∈ X,
                                       dY (f (x2 ), f (x1 )) ≤ KdX (x2 , x1 ).                        (1)
The smallest such K satisfying Equation (1), denoted by Kf , is called the Lipschitz constant of
f . For neural networks, X is in general Rm equipped with the ℓp -norm. We will only consider
the case when Y = R. In actual applications such as a classification task, a neural network has
multiple outputs. The prediction is the class with the maximum score. One can then use the margin
between each pair of class predictions and its Lipschitz constant to certify the robustness of a given
prediction (Raghunathan et al., 2018; Leino et al., 2021). From Rademacher’s theorem, if f is
Lipschitz continuous, then f is is almost everywhere differentiable, and Kf = supx ||∇f (x)||q .
