← Visual paper

HardnessBilevelUnconditional/Main.lean

d1032f4c70da9b037605c2f444ce2450900e5a76 · GitHub

  1. /-
  2. Copyright: HardnessBilevel project.
  4. # Assumption-free forms of the main theorems
  6. Every theorem of the core library `HardnessBilevel` that takes one of the assumption classes
  7. `HasSemialgebraicProjections` (A1), `HasFinitenessTheorem` (A2), `HasGrowthBound` (A3) as a binder is restated here
  8. with no binder, in the namespace `Bilevel.Unconditional`, under the same name. Each proof is the core theorem
  9. itself: the binders are filled by the proved instances of `HardnessBilevelUnconditional/Instances.lean`.
  11. Covered: Proposition 2.6, Theorems 2.12, 2.15, 2.18, 2.20, 2.21 and their pessimistic counterparts (paper §2.4).
  12. The statements are copied from the core library with the class binders removed and nothing else changed.
  14. `scripts/CheckAxiomsUnconditional.lean` prints the axioms of every theorem of this file; they are exactly
  15. `propext`, `Classical.choice`, `Quot.sound`.
  16. -/
  17. import HardnessBilevel
  18. import HardnessBilevelUnconditional.Instances
  20. namespace Bilevel.Unconditional
  22. /-! ### Proposition 2.6 -/
  24. /-- Proposition 2.6 (corrected), for any semialgebraic lower-level set `Y`: the optimistic value function of a
  25. polynomial bilevel problem is extended-real semialgebraic. -/
  26. theorem valueFun_isExtSemialgebraic
  27. {n : ℕ} {ι : Type} [Fintype ι] {P Q : (Fin n → ℝ) → (ι → ℝ) → ℝ} {Y : Set (ι → ℝ)}
  28. (hP : IsPolyFun P) (hQ : IsPolyFun Q) (hY : IsSemialgebraic Y) :
  29. IsExtSemialgebraic (valueFun P Q Y) :=
  30. _root_.Bilevel.valueFun_isExtSemialgebraic hP hQ hY
  32. /-- Proposition 2.6, pessimistic twin. -/
  33. theorem pvalueFun_isExtSemialgebraic
  34. {n : ℕ} {ι : Type} [Fintype ι] {P Q : (Fin n → ℝ) → (ι → ℝ) → ℝ} {Y : Set (ι → ℝ)}
  35. (hP : IsPolyFun P) (hQ : IsPolyFun Q) (hY : IsSemialgebraic Y) :
  36. IsExtSemialgebraic (pvalueFun P Q Y) :=
  37. _root_.Bilevel.pvalueFun_isExtSemialgebraic hP hQ hY
  39. /-! ### Theorem 2.12 -/
  41. /-- Theorem 2.12: `𝒫_unbound = SA`. -/
  42. theorem thm212_eq_SA {n : ℕ} : P_unbound n = SA n :=
  43. _root_.Bilevel.thm212_eq_SA
  45. /-- Theorem 2.12, pessimistic: `𝒫^p_unbound = SA`. -/
  46. theorem pess_thm212 {n : ℕ} : Pp_unbound n = SA n :=
  47. _root_.Bilevel.pess_thm212
  49. /-! ### Theorem 2.15 -/
  51. /-- Theorem 2.15 (`⊇`, construction): every real semialgebraic, lower semicontinuous function bounded on compacts
  52. is the value function of a polynomial bilevel problem over a bounded box. -/
  53. theorem thm215_supset
  54. {n : ℕ} (f : (Fin n → ℝ) → ℝ)
  55. (hsa : IsSemialgebraicMap f)
  56. (hlsc : LowerSemicontinuous f)
  57. (hcb : ∀ K : Set (Fin n → ℝ), IsCompact K → ∃ B, ∀ x ∈ K, |f x| ≤ B) :
  58. ∃ (ι : Type) (_ : Fintype ι) (P Q : (Fin n → ℝ) → (ι → ℝ) → ℝ) (a b : ι → ℝ),
  59. IsPolyFun P ∧ IsPolyFun Q ∧ (∀ k, a k ≤ b k) ∧
  60. ∀ x, valueFun P Q (boundedBox a b) x = ((f x : ℝ) : EReal) :=
  61. _root_.Bilevel.thm215_supset f hsa hlsc hcb
  63. /-- Theorem 2.15: `𝒫_bounded = SA ∩ LSC ∩ CB`. -/
  64. theorem thm215_eq {n : ℕ} : P_bounded n = SA n ∩ LSC n ∩ CB n :=
  65. _root_.Bilevel.thm215_eq
  67. /-- Theorem 2.15, pessimistic: `𝒫^p_bounded = SA ∩ USC ∩ CB`. -/
  68. theorem pess_thm215 {n : ℕ} : Pp_bounded n = SA n ∩ USC n ∩ CB n :=
  69. _root_.Bilevel.pess_thm215
  71. /-! ### Theorem 2.18 -/
  73. /-- Theorem 2.18: `PP ⊆ 𝒞_unbound ⊆ SA`. -/
  74. theorem thm218_main {n : ℕ} : PPe n ⊆ C_unbound n ∧ C_unbound n ⊆ SA n :=
  75. _root_.Bilevel.thm218_main
  77. /-- Theorem 2.18, pessimistic: `PP ⊆ 𝒞^p_unbound ⊆ SA`. -/
  78. theorem pess_thm218 {n : ℕ} : PPe n ⊆ Cp_unbound n ∧ Cp_unbound n ⊆ SA n :=
  79. _root_.Bilevel.pess_thm218
  81. /-! ### Theorem 2.20 -/
  83. /-- Theorem 2.20 (first inclusion, construction): a lower semicontinuous piecewise polynomial function is the
  84. value function of a polynomial bilevel problem with convex lower level over a bounded box. -/
  85. theorem thm220_supset {n : ℕ} (f : (Fin n → ℝ) → ℝ) (hPP : f ∈ PP n)
  86. (hlsc : LowerSemicontinuous f) : coeFun f ∈ C_bounded n :=
  87. _root_.Bilevel.thm220_supset f hPP hlsc
  89. /-- Theorem 2.20: `PP ∩ LSC ⊆ 𝒞_bounded ⊆ SA ∩ LSC ∩ CB`. -/
  90. theorem thm220_main {n : ℕ} :
  91. coeFun '' (PP n ∩ {f | LowerSemicontinuous f}) ⊆ C_bounded n ∧
  92. C_bounded n ⊆ SA n ∩ LSC n ∩ CB n :=
  93. _root_.Bilevel.thm220_main
  95. /-- Theorem 2.20, pessimistic: `PP ∩ USC ⊆ 𝒞^p_bounded ⊆ SA ∩ USC ∩ CB`. -/
  96. theorem pess_thm220 {n : ℕ} :
  97. coeFun '' (PP n ∩ {f | UpperSemicontinuous f}) ⊆ Cp_bounded n ∧
  98. Cp_bounded n ⊆ SA n ∩ USC n ∩ CB n :=
  99. _root_.Bilevel.pess_thm220
  101. /-! ### Theorem 2.21 -/
  103. /-- A polynomial bilevel problem with nonempty compact semialgebraic lower set has its optimistic value function
  104. in `𝒞_cc`. -/
  105. theorem thm221_compact_sa_incl {n : ℕ} {ι : Type} [Fintype ι]
  106. {P Q : (Fin n → ℝ) → (ι → ℝ) → ℝ} (hP : IsPolyFun P) (hQ : IsPolyFun Q) {Y : Set (ι → ℝ)}
  107. (hYc : IsCompact Y) (hYn : Y.Nonempty) (hYs : IsSemialgebraic Y) :
  108. valueFun P Q Y ∈ C_cc n :=
  109. _root_.Bilevel.thm221_compact_sa_incl hP hQ hYc hYn hYs
  111. /-- Pessimistic twin of `thm221_compact_sa_incl`. -/
  112. theorem thm221_compact_sa_incl_pess {n : ℕ} {ι : Type} [Fintype ι]
  113. {P Q : (Fin n → ℝ) → (ι → ℝ) → ℝ} (hP : IsPolyFun P) (hQ : IsPolyFun Q) {Y : Set (ι → ℝ)}
  114. (hYc : IsCompact Y) (hYn : Y.Nonempty) (hYs : IsSemialgebraic Y) :
  115. pvalueFun P Q Y ∈ Cp_cc n :=
  116. _root_.Bilevel.thm221_compact_sa_incl_pess hP hQ hYc hYn hYs
  118. /-- Theorem 2.21: `𝒞_cc = SA ∩ LSC ∩ CB`. -/
  119. theorem thm221_eq {n : ℕ} : C_cc n = SA n ∩ LSC n ∩ CB n :=
  120. _root_.Bilevel.thm221_eq
  122. /-- Theorem 2.21, pessimistic: `𝒞^p_cc = SA ∩ USC ∩ CB`. -/
  123. theorem pess_thm221 {n : ℕ} : Cp_cc n = SA n ∩ USC n ∩ CB n :=
  124. _root_.Bilevel.pess_thm221
  126. end Bilevel.Unconditional