Lipschitz-based robustness lemmas

This file connects Lipschitz continuity assumptions to the robustness specifications from NN.MLTheory.Robustness.Spec.

Main results (over $\mathbb{R}$):

• An $L$-Lipschitz map is adversarially robust: $\varepsilon$ input perturbations imply $L\varepsilon$ output perturbations.
• If a logits vector has a positive logit margin, then its argmax classifier is stable under sufficiently small $\ell_\infty$ perturbations; combined with an output-$\ell_\infty$ Lipschitz bound, this yields certified robustness radii.

Lipschitz continuity implies adversarial robustness

theorem NN.MLTheory.Proofs.Verification.Robustness.is_adversarially_robust_of_lipschitz {s₁ s₂ : Spec.Shape} {f : Spec.Tensor ℝ s₁ → Spec.Tensor ℝ s₂} {norm₁ norm₂ : {s : Spec.Shape} → Spec.Tensor ℝ s → ℝ} {L : ℝ} (hL : 0 ≤ L) (hLip : Robustness.Spec.isLipschitzContinuous f (fun {s : Spec.Shape} => norm₁) (fun {s : Spec.Shape} => norm₂) L) (x₀ : Spec.Tensor ℝ s₁) (ε : ℝ) : Robustness.Spec.isAdversariallyRobust f (fun {s : Spec.Shape} => norm₁) (fun {s : Spec.Shape} => norm₂) x₀ ε (L * ε)

If $f$ is $L$-Lipschitz and $L\geq 0$, then $f$ is adversarially robust at $x_0$: every input within distance $\varepsilon$ of $x_0$ maps within distance $L\varepsilon$ of $f(x_0)$.

Bridging $\ell_2$ and $\ell_\infty$ Lipschitz predicates

theorem NN.MLTheory.Proofs.Verification.Robustness.is_lipschitz_continuous_linf_of_l2 {s₁ : Spec.Shape} {n : ℕ} {f : Spec.Tensor ℝ s₁ → Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)} {normIn : {s : Spec.Shape} → Spec.Tensor ℝ s → ℝ} {L : ℝ} (hLip2 : Robustness.Spec.isLipschitzContinuous f (fun {s : Spec.Shape} => normIn) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) L) : Robustness.Spec.isLipschitzContinuous f (fun {s : Spec.Shape} => normIn) (fun {s : Spec.Shape} => Robustness.Spec.tensorLinfNorm) L

$\ell_2$-Lipschitz implies $\ell_\infty$-Lipschitz into logits, with the same constant.

This is the standard norm comparison $\lVert v\rVert_\infty\leq\lVert v\rVert_2$ (proved as Proofs.tensor_linf_norm_le_tensor_l2_norm).

Argmax stability from a positive logit margin

noncomputable def NN.MLTheory.Proofs.Verification.Robustness.argmaxClassifier {n : ℕ} (y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) : ℕ

The argmax classifier on logits vectors, breaking ties by the earliest index.

When $n=0$, this returns $0$ by convention.

def NN.MLTheory.Proofs.Verification.Robustness.HasLogitMargin {n : ℕ} (y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (c : Fin n) (m : ℝ) : Prop

HasLogitMargin y c m means class $c$ beats every competitor by at least $m$ in logit value.

theorem NN.MLTheory.Proofs.Verification.Robustness.argmaxClassifier_eq_of_linf_distance_lt_half_margin {n : ℕ} {y₀ y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)} {c : Fin n} {m δ : ℝ} (hmargin : HasLogitMargin y₀ c m) (hδ : 2 * δ < m) (hdist : Robustness.Spec.tensorDistance (fun {s : Spec.Shape} => Robustness.Spec.tensorLinfNorm) y₀ y ≤ δ) : argmaxClassifier y = ↑c

If $y_0$ has a positive logit margin $m$ for class $c$, then any $y$ within $\ell_\infty$ distance $\delta$ with $2\delta<m$ has the same argmax class.

theorem NN.MLTheory.Proofs.Verification.Robustness.argmaxClassifier_eq_of_hasLogitMargin {n : ℕ} {y₀ : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)} {c : Fin n} {m : ℝ} (hm : 0 < m) (hmargin : HasLogitMargin y₀ c m) : argmaxClassifier y₀ = ↑c

If $y_0$ has margin $m>0$ for class $c$, then $c$ is the argmaxClassifier of $y_0$.

Certified robustness from a Lipschitz bound and a logit margin

theorem NN.MLTheory.Proofs.Verification.Robustness.is_certified_robust_of_lipschitz_of_logitMargin {s₁ : Spec.Shape} {n : ℕ} {f : Spec.Tensor ℝ s₁ → Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)} {normIn : {s : Spec.Shape} → Spec.Tensor ℝ s → ℝ} {L : ℝ} (hL : 0 ≤ L) (hLip : Robustness.Spec.isLipschitzContinuous f (fun {s : Spec.Shape} => normIn) (fun {s : Spec.Shape} => Robustness.Spec.tensorLinfNorm) L) {x₀ : Spec.Tensor ℝ s₁} {ε m : ℝ} {c : Fin n} (hm : 0 < m) (hmargin : HasLogitMargin (f x₀) c m) (hε : 2 * (L * ε) < m) : Robustness.Spec.isCertifiedRobust (fun (x : Spec.Tensor ℝ s₁) => argmaxClassifier (f x)) (fun {s : Spec.Shape} => normIn) x₀ ε

If $f$ is $L$-Lipschitz into $\ell_\infty$ logits and the reference logits $f(x_0)$ have margin $m$ for class $c$, then any input perturbation of radius $\varepsilon$ with $2L\varepsilon<m$ preserves the predicted class.

This is a standard “margin over Lipschitz constant” certified robustness lemma.

theorem NN.MLTheory.Proofs.Verification.Robustness.is_certified_robust_of_l2_lipschitz_of_logitMargin {s₁ : Spec.Shape} {n : ℕ} {f : Spec.Tensor ℝ s₁ → Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)} {normIn : {s : Spec.Shape} → Spec.Tensor ℝ s → ℝ} {L : ℝ} (hL : 0 ≤ L) (hLip2 : Robustness.Spec.isLipschitzContinuous f (fun {s : Spec.Shape} => normIn) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) L) {x₀ : Spec.Tensor ℝ s₁} {ε m : ℝ} {c : Fin n} (hm : 0 < m) (hmargin : HasLogitMargin (f x₀) c m) (hε : 2 * (L * ε) < m) : Robustness.Spec.isCertifiedRobust (fun (x : Spec.Tensor ℝ s₁) => argmaxClassifier (f x)) (fun {s : Spec.Shape} => normIn) x₀ ε

Certified robustness, but starting from an output-$\ell_2$ Lipschitz assumption.

This avoids requiring the user to manually insert the norm-equivalence step $\lVert\cdot\rVert_\infty\leq\lVert\cdot\rVert_2$.