FiniteSelection.lean

1 import Mathlib.Basic.Real.Basic
2 import Mathlib.Tactic
3 
4 /-!
5 Author: Komorebi P.
6 Checked source. Finite objective selection with an explicit
7 singleton case. PruningSums connects these statements to arbitrary complete
8 covering antichains, including the attained positive gap.
9 -/
10 
11 namespace KomorebiPaperV
12 section Selection
13 variable {A : Type*}
14 
15 theorem finite_minimum (f : A → ℝ) :
16     ∀ s : Finset A, s.Nonempty → ∃ m ∈ s, ∀ a ∈ s, f m ≤ f a := by
17   classical
18   intro s
19   induction s using Finset.induction_on with
20   | empty =>
21     intro hs
22     simp at hs
23   | @insert a s ha ih =>
24     intro _
25     by_cases hs : s.Nonempty
26     · obtain ⟨m, hm, hmin⟩ := ih hs
27       by_cases h : f a ≤ f m
28       · refine ⟨a, Finset.mem_insert_self _ _, ?_⟩
29         intro b hb
30         rcases Finset.mem_insert.mp hb with hba | hbs
31         · subst b
32           exact le_rfl
33         · exact h.trans (hmin b hbs)
34       · refine ⟨m, Finset.mem_insert_of_mem hm, ?_⟩
35         intro b hb
36         rcases Finset.mem_insert.mp hb with hba | hbs
37         · subst b
38           linarith
39         · exact hmin b hbs
40     · have hempty : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs
41       subst s
42       refine ⟨a, by simp, ?_⟩
43       intro b hb
44       have hba : b = a := by simpa using hb
45       subst b
46       exact le_rfl
47 
48 theorem positive_gap [DecidableEq A] (s : Finset A) (f : A → ℝ) (m : A)
49     (hcompetitors : (s.erase m).Nonempty)
50     (hstrict : ∀ a ∈ s, a ≠ m → f m < f a) :
51     ∃ γ : ℝ, 0 < γ ∧ ∀ a ∈ s, a ≠ m → γ ≤ f a - f m := by
52   obtain ⟨r, hr, hmin⟩ := finite_minimum (fun a => f a - f m) (s.erase m) hcompetitors
53   have hr' := Finset.mem_erase.mp hr
54   refine ⟨f r - f m, sub_pos.mpr (hstrict r hr'.2 hr'.1), ?_⟩
55   intro a ha hne
56   exact hmin a (Finset.mem_erase.mpr ⟨hne, ha⟩)
57 
58 theorem gap_stability (s : Finset A) (f g : A → ℝ) (m : A)
59     (hm : m ∈ s) (γ ε : ℝ)
60     (hgap : ∀ a ∈ s, a ≠ m → γ ≤ f a - f m)
61     (hpert : ∀ a ∈ s, |g a - f a| ≤ ε) (hmargin : 2 * ε < γ) :
62     ∀ a ∈ s, a ≠ m → g m < g a := by
63   intro a ha hne
64   have hmerr := abs_le.mp (hpert m hm)
65   have haerr := abs_le.mp (hpert a ha)
66   have hsep := hgap a ha hne
67   linarith
68 
69 theorem singleton_minimum [DecidableEq A] (f : A → ℝ) (m : A) :
70     ∀ a ∈ ({m} : Finset A), f m ≤ f a := by
71   intro a ha
72   have h : a = m := by simpa using ha
73   subst a
74   exact le_rfl
75 
76 theorem singleton_selection_unchanged [DecidableEq A] (m a : A)
77     (ha : a ∈ ({m} : Finset A)) : a = m := by
78   simpa using ha
79 end Selection
80 end KomorebiPaperV

Back to source controls