Lipschitz-based robustness lemmas

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

Main results (over ℝ):

• An L-Lipschitz map is adversarially robust: ε input perturbations imply L*ε output perturbations.
• If a logits vector has a positive logit margin, then its argmax classifier is stable under sufficiently small L∞ perturbations; combined with an output-L∞ 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 ≥ 0, then f is adversarially robust at x₀: every input within distance ε of x₀ maps within distance L*ε of f x₀.

Bridging L2 and L∞ 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

L2-Lipschitz implies L∞-Lipschitz into logits, with the same constant.

This is the standard norm comparison ‖v‖∞ ≤ ‖v‖₂ (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₀ has a positive logit margin m for class c, then any y within L∞ distance δ with 2*δ < 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₀ has margin m > 0 for class c, then c is the argmaxClassifier of y₀.

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 L∞ logits and the reference logits f x₀ have margin m for class c, then any input perturbation of radius ε with 2*(L*ε) < 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-L2 Lipschitz assumption.

This avoids requiring the user to manually insert the norm-equivalence step ‖·‖∞ ≤ ‖·‖₂.