FacetRobustness.lean

1 import KomorebiLSM.RobustFiniteDomains
2 import Mathlib.Analysis.Normed.Operator.Basic
3 
4 /-! P40 norm-ball certificate. Facets must describe the whole generated cone;
5 normalization is an additional exact condition, not a consequence of the margin. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RobustDomains
8 open PositiveLift
9 variable {E I J : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
10 
11 /-- Coefficient perturbation is controlled in the declared operator/dual norms. -/
12 theorem facet_error_bound (g : E →L[ℝ] ℝ) (B D : E →L[ℝ] E)
13     (ε : ℝ) (hε : ‖B-D‖ ≤ ε) (v : E) :
14     |g (B v)-g (D v)| ≤ ε * ‖g‖ * ‖v‖ := by
15   have he : g (B v)-g (D v) = g ((B-D) v) := by simp only [map_sub,sub_apply]
16   rw [he,← Real.norm_eq_abs]
17   calc
18     ‖g ((B-D) v)‖ ≤ ‖g‖ * ‖(B-D) v‖ := g.le_opNorm _
19     _ ≤ ‖g‖ * (‖B-D‖ * ‖v‖) :=
20       mul_le_mul_of_nonneg_left ((B-D).le_opNorm v) (norm_nonneg _)
21     _ ≤ ‖g‖ * (ε * ‖v‖) := mul_le_mul_of_nonneg_left
22       (mul_le_mul_of_nonneg_right hε (norm_nonneg _)) (norm_nonneg _)
23     _ = ε * ‖g‖ * ‖v‖ := by ring
24 
25 /-- Every perturbed generator image lies on the positive side of every facet. -/
26 theorem facet_margin_robust (g : E →L[ℝ] ℝ) (B D : E →L[ℝ] E)
27     (ε : ℝ) (hε : ‖B-D‖ ≤ ε) (v : E)
28     (hm : ε * ‖g‖ * ‖v‖ ≤ g (D v)) : 0 ≤ g (B v) := by
29   have he := (abs_le.mp (facet_error_bound g B D ε hε v)).1
30   linarith
31 
32 theorem facet_norm_ball_invariant [Fintype J] [DecidableEq J]
33     (V : (J → ℝ) →ₗ[ℝ] E) (g : I → E →L[ℝ] ℝ)
34     (hfacets : hull V = {x | ∀ i, 0 ≤ g i x})
35     (B D : E →L[ℝ] E) (ε : ℝ) (hε : ‖B-D‖ ≤ ε)
36     (hm : ∀ i j, ε * ‖g i‖ * ‖generator V j‖ ≤ g i (D (generator V j))) :
37     ∀ x ∈ hull V, B x ∈ hull V := by
38   apply (invariant_iff_generators V B.toLinearMap).mpr
39   intro j
40   rw [hfacets]
41   exact fun i => facet_margin_robust (g i) B D ε hε _ (hm i j)
42 
43 /-- The robust facet statement also constructs a nonnegative perturbed lift. -/
44 theorem facet_norm_ball_lift [Fintype J] [DecidableEq J]
45     (V : (J → ℝ) →ₗ[ℝ] E) (g : I → E →L[ℝ] ℝ)
46     (hfacets : hull V = {x | ∀ i, 0 ≤ g i x})
47     (B D : E →L[ℝ] E) (ε : ℝ) (hε : ‖B-D‖ ≤ ε)
48     (hm : ∀ i j, ε * ‖g i‖ * ‖generator V j‖ ≤ g i (D (generator V j))) :
49     ∃ M : Matrix J J ℝ, (∀ i j, 0 ≤ M i j) ∧ B.toLinearMap.comp V = V.comp M.mulVecLin :=
50   (positive_lift_iff V B.toLinearMap).mp (facet_norm_ball_invariant V g hfacets B D ε hε hm)
51 
52 end Komorebi.LSM.RobustDomains

Back to source controls