HardPareto.lean

1 import Mathlib.Order.Preorder.Finite
2 import Mathlib.Data.Finset.Lattice.Fold
3 import Mathlib.Data.Fintype.Pi
4 import Mathlib.Algebra.Order.BigOperators.Group.Finset
5 
6 /-!
7 # Finite Pareto reduction
8 
9 Only nondominated profiles are retained. The lower cofinality theorem, rather
10 than independent minimization of coordinates, is the preservation invariant.
11 -/
12 namespace Komorebi.MachineTheory.HardPareto
13 
14 variable {P : Type*} [PartialOrder P]
15 
16 noncomputable def frontier (s : Finset P) : Finset P := by
17   classical
18   exact s.filter (fun p => ∀ q ∈ s, q ≤ p → p ≤ q)
19 
20 @[simp] theorem mem_frontier (s : Finset P) (p : P) :
21     p ∈ frontier s ↔ p ∈ s ∧ ∀ q ∈ s, q ≤ p → p ≤ q := by
22   classical
23   simp [frontier]
24 
25 theorem frontier_subset (s : Finset P) : frontier s ⊆ s :=
26   fun p hp => ((mem_frontier s p).mp hp).1
27 
28 /-- Every discarded profile is weakly dominated by a retained one. -/
29 theorem exists_frontier_le (s : Finset P) {p : P} (hp : p ∈ s) :
30     ∃ q ∈ frontier s, q ≤ p := by
31   obtain ⟨q, hqp, hq, hmin⟩ := s.exists_le_minimal hp
32   exact ⟨q, (mem_frontier s q).mpr ⟨hq, hmin⟩, hqp⟩
33 
34 theorem budget_iff (s : Finset P) (b : P) :
35     (∃ p ∈ s, p ≤ b) ↔ ∃ p ∈ frontier s, p ≤ b := by
36   constructor
37   · rintro ⟨p, hp, hb⟩
38     obtain ⟨q, hq, hqp⟩ := exists_frontier_le s hp
39     exact ⟨q, hq, hqp.trans hb⟩
40   · rintro ⟨p, hp, hb⟩
41     exact ⟨p, frontier_subset s hp, hb⟩
42 
43 /-- A finite sound lower-cofinal subset has exactly the same minimal profiles. -/
44 theorem frontier_characterization (s : Finset P) (T : Set P)
45     (sound : ∀ p ∈ s, p ∈ T)
46     (complete : ∀ p ∈ T, ∃ q ∈ s, q ≤ p) (p : P) :
47     p ∈ frontier s ↔ p ∈ T ∧ ∀ q ∈ T, q ≤ p → p ≤ q := by
48   constructor
49   · intro hp
50     obtain ⟨hs, hm⟩ := (mem_frontier s p).mp hp
51     refine ⟨sound p hs, ?_⟩
52     intro q hq hqp
53     obtain ⟨r, hr, hrq⟩ := complete q hq
54     exact (hm r hr (hrq.trans hqp)).trans hrq
55   · rintro ⟨hp, hm⟩
56     obtain ⟨q, hq, hqp⟩ := complete p hp
57     have he : p = q := le_antisymm (hm q (sound q hq) hqp) hqp
58     refine (mem_frontier s p).mpr ⟨he ▸ hq, ?_⟩
59     intro r hr hrp
60     exact hm r (sound r hr) hrp
61 
62 end Komorebi.MachineTheory.HardPareto

Back to source controls