Dual certificate existence

Existence of a dual certificate for best l∞ approximation from the additive subspace, using geometric Hahn-Banach separation.

Indicator function and basic properties

def Finset.indicator' {U : Type u_1} [DecidableEq U] (S : Finset U) : U → ℝ

Indicator function of a finset as a vector in U → ℝ.

Equations

• S.indicator' i = if i ∈ S then 1 else 0

@[simp]

theorem Finset.indicator'_apply {U : Type u_1} [DecidableEq U] (S : Finset U) (i : U) : S.indicator' i = if i ∈ S then 1 else 0

theorem KaltonRoberts.clm_decompose {U : Type u_1} [DecidableEq U] [Fintype U] (Λ : (U → ℝ) →L[ℝ] ℝ) (h : U → ℝ) : Λ h = ∑ i : U, h i * Λ (Function.update 0 i 1)

A continuous linear map on U → ℝ decomposes via basis vectors.

theorem KaltonRoberts.clm_indicator'_eq_additiveFunction {U : Type u_1} [DecidableEq U] (Λ : (U → ℝ) →L[ℝ] ℝ) (S : Finset U) : Λ S.indicator' = additiveFunction (fun (i : U) => Λ (Function.update 0 i 1)) S

Applying a CLinearMap to an indicator equals additiveFunction.

M = 0 case

theorem KaltonRoberts.dual_cert_zero_case {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (_hf : IsApproxAdditive f 1) (hMbound : ∀ (S : Finset U), |f S| ≤ distToAdditive f) (hM0 : distToAdditive f = 0) : Nonempty (DualCertificate f (distToAdditive f))

M > 0 case: the Hahn–Banach argument

noncomputable def KaltonRoberts.activeGenerators {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (M : ℝ) : Set (U → ℝ)

The set of "signed indicator generators" at active sets.

Equations

• KaltonRoberts.activeGenerators f M = (fun (S : Finset U) => S.indicator') '' {S : Finset U | f S = M} ∪ (fun (S : Finset U) => -S.indicator') '' {S : Finset U | f S = -M}

theorem KaltonRoberts.activeGenerators_finite {U : Type u_1} [DecidableEq U] [Finite U] (f : Finset U → ℝ) (M : ℝ) : (activeGenerators f M).Finite

theorem KaltonRoberts.zero_mem_convexHull_of_best_approx {U : Type u_1} [DecidableEq U] [Finite U] (f : Finset U → ℝ) (M : ℝ) (hM_pos : 0 < M) (hMbound : ∀ (S : Finset U), |f S| ≤ M) (hbest : ∀ (a : U → ℝ), ∃ (S : Finset U), |f S - additiveFunction a S| ≥ M) : 0 ∈ (convexHull ℝ) (activeGenerators f M)

theorem KaltonRoberts.indicator'_injective {U : Type u_1} [DecidableEq U] : Function.Injective Finset.indicator'

indicator' is injective: different finsets give different indicator functions.

theorem KaltonRoberts.dual_cert_from_convexHull {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (M : ℝ) (hM_pos : 0 < M) (hMbound : ∀ (S : Finset U), |f S| ≤ M) (h0 : 0 ∈ (convexHull ℝ) (activeGenerators f M)) : Nonempty (DualCertificate f M)

theorem KaltonRoberts.dual_cert_pos_case {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (_hf : IsApproxAdditive f 1) (hMbound : ∀ (S : Finset U), |f S| ≤ distToAdditive f) (hbest : ∀ (a : U → ℝ), ∃ (S : Finset U), |f S - additiveFunction a S| ≥ distToAdditive f) (hM_pos : 0 < distToAdditive f) : Nonempty (DualCertificate f (distToAdditive f))

When M > 0, construct the dual certificate via Hahn–Banach.

theorem KaltonRoberts.distToAdditive_nonneg {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (hM : ∀ (S : Finset U), |f S| ≤ distToAdditive f) : 0 ≤ distToAdditive f

distToAdditive f ≥ 0 for any function f.

theorem KaltonRoberts.dual_certificate_exists_proof {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (hM : ∀ (S : Finset U), |f S| ≤ distToAdditive f) (hbest : ∀ (a : U → ℝ), ∃ (S : Finset U), |f S - additiveFunction a S| ≥ distToAdditive f) : Nonempty (DualCertificate f (distToAdditive f))

Lemma 2.1 (Dual certificate existence). Combines the M = 0 and M > 0 cases.