IndisputableMonolith.Verification.CPT.EpsilonCertification

   1import Mathlib
   2
   3/-!
   4# CPT Epsilon Certification Layer
   5
   6Claim-honest Lean formalization of the epsilon/noise ranking layer used in the paper:
   7
   8- perturbation bound `|ĉ - c| ≤ ε`,
   9- minimizer/argmin transfer from `ĉ` to `c`,
  10- explicit `2ε`-suboptimality guarantee.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Verification
  15namespace CPT
  16namespace EpsilonCertification
  17
  18open scoped Classical
  19
  20variable {O : Type}
  21
  22/-- `ε`-meaning set for a scalar objective on candidates. -/
  23def MeanEps (c : O → ℝ) (ε : ℝ) : Set O :=
  24  {o | ∀ o', c o ≤ c o' + ε}
  25
  26/-- If `oHat` minimizes perturbed costs `cHat` and `|cHat-c| ≤ ε`, then `oHat`
  27is `2ε`-optimal for the true cost `c`. -/
  28theorem approx_argmin_stability
  29    (c cHat : O → ℝ) (ε : ℝ)
  30    (hErr : ∀ o, |cHat o - c o| ≤ ε)
  31    (oHat : O)
  32    (hMin : ∀ o, cHat oHat ≤ cHat o) :
  33    ∀ o, c oHat ≤ c o + 2 * ε := by
  34  intro o
  35  have hHat_ge_true : c oHat ≤ cHat oHat + ε := by
  36    have h := (abs_le.mp (hErr oHat)).1
  37    linarith
  38  have hMin' : cHat oHat ≤ cHat o := hMin o
  39  have hHat_le_true : cHat o ≤ c o + ε := by
  40    have h := (abs_le.mp (hErr o)).2
  41    linarith
  42  linarith
  43
  44/-- Set-level form: the perturbed minimizer belongs to the `2ε`-meaning set of `c`. -/
  45theorem approx_argmin_mem_meanEps
  46    (c cHat : O → ℝ) (ε : ℝ)
  47    (hErr : ∀ o, |cHat o - c o| ≤ ε)
  48    (oHat : O)
  49    (hMin : ∀ o, cHat oHat ≤ cHat o) :
  50    oHat ∈ MeanEps c (2 * ε) := by
  51  intro o
  52  exact approx_argmin_stability c cHat ε hErr oHat hMin o
  53
  54end EpsilonCertification
  55end CPT
  56end Verification
  57end IndisputableMonolith
  58