← Visual paper

HardnessBilevel/Convex/Lemma219.lean

d1032f4c70da9b037605c2f444ce2450900e5a76 · GitHub

  1. import HardnessBilevel.Convex.Toolkit
  3. /-!
  4. # Lemma 2.19 (simplified gadget, blueprint §4.G.2) — id `t219.main`
  6. For a basic set `S = {x | P(x) = 0 ∧ ∀ j, 0 < Q_j(x)}` (`basicSet P Q`), lower variable `y : Unit ⊕ J → ℝ`
  7. (`t = y (inl ())`, `u j = y (inr j)`), box `gadY J = ℝ × [0,∞)^J` and
  8. * `gadQ P Q x y = (1 - t P(x))^2 + ∑ j (1 - Q_j(x) u_j)^2`,
  9. * `gadP P Q x y = (1 - t P(x)) * ∏ j (Q_j(x) u_j)`,
  11. the lower level is polynomial and convex, the box is unbounded (because of the free coordinate `t`, even if
  12. `J = ∅`), every argmin is nonempty, and `gadP` is **constant** on the argmin with value `1_S x`; hence
  13. `valueFun = pvalueFun = ↑(1_S x)` (`lemma219`, `lemma219_exists`).
  14. -/
  16. namespace Bilevel
  18. open Set MvPolynomial
  20. section Lemma219
  22. variable {n : ℕ} {J : Type*} [Fintype J]
  24. /-- The basic semialgebraic set `{x | P(x) = 0 ∧ ∀ j, 0 < Q_j(x)}`. -/
  25. def basicSet (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) : Set (Fin n → ℝ) :=
  26. {x | eval x P = 0 ∧ ∀ j, 0 < eval x (Q j)}
  28. /-- Lower-level objective `Q'` of the Lemma 2.19 gadget. -/
  29. noncomputable def gadQ (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) :
  30. (Fin n → ℝ) → (Unit ⊕ J → ℝ) → ℝ :=
  31. fun x y => (1 - y (Sum.inl ()) * eval x P) ^ 2 + ∑ j, (1 - eval x (Q j) * y (Sum.inr j)) ^ 2
  33. /-- Upper-level objective `P'` of the Lemma 2.19 gadget. -/
  34. noncomputable def gadP (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) :
  35. (Fin n → ℝ) → (Unit ⊕ J → ℝ) → ℝ :=
  36. fun x y => (1 - y (Sum.inl ()) * eval x P) * ∏ j, (eval x (Q j) * y (Sum.inr j))
  38. /-- The box `ℝ × [0,∞)^J` of the Lemma 2.19 gadget. -/
  39. def gadY (J : Type*) : Set (Unit ⊕ J → ℝ) :=
  40. Set.pi Set.univ (Sum.elim (fun _ => Set.univ) (fun _ => Set.Ici 0))
  42. theorem mem_argminSet_gadQ_iff (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ)
  43. (x : Fin n → ℝ) (y : Unit ⊕ J → ℝ) :
  44. y ∈ argminSet (gadQ P Q) (gadY J) x ↔
  45. (∀ t, (1 - eval x P * y (Sum.inl ())) ^ 2 ≤ (1 - eval x P * t) ^ 2) ∧
  46. ∀ j, 0 ≤ y (Sum.inr j) ∧
  47. ∀ u, 0 ≤ u → (1 - eval x (Q j) * y (Sum.inr j)) ^ 2 ≤ (1 - eval x (Q j) * u) ^ 2 := by
  48. let g : (Fin n → ℝ) → (Unit ⊕ J) → ℝ → ℝ := fun x =>
  49. Sum.elim (fun _ v => (1 - eval x P * v) ^ 2) (fun j v => (1 - eval x (Q j) * v) ^ 2)
  50. have hQ : gadQ P Q = fun x y => ∑ c, g x c (y c) := by
  51. funext x y
  52. simp [gadQ, g, Fintype.sum_sum_type, mul_comm]
  53. rw [hQ, gadY, argminSet_pi_sum]
  54. simp only [Set.mem_pi, Set.mem_univ, true_implies, Sum.forall, argminSet, Set.mem_ofPred_eq,
  55. Sum.elim_inl, Sum.elim_inr, g, Set.mem_Ici, true_and]
  56. exact ⟨fun ⟨h1, h2⟩ => ⟨h1 (), h2⟩, fun ⟨h1, h2⟩ => ⟨fun _ => h1, h2⟩⟩
  58. /-- Witness of a minimiser of the gadget. -/
  59. noncomputable def gadMin (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ)
  60. (x : Fin n → ℝ) : Unit ⊕ J → ℝ :=
  61. Sum.elim (fun _ => if eval x P = 0 then 0 else (eval x P)⁻¹)
  62. (fun j => if 0 < eval x (Q j) then (eval x (Q j))⁻¹ else 0)
  64. theorem gadMin_mem (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) (x : Fin n → ℝ) :
  65. gadMin P Q x ∈ argminSet (gadQ P Q) (gadY J) x := by
  66. rw [mem_argminSet_gadQ_iff]
  67. exact ⟨isMin_univ_witness _, fun j => isMin_Ici_witness _⟩
  69. theorem argminSet_gadQ_nonempty (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ)
  70. (x : Fin n → ℝ) : (argminSet (gadQ P Q) (gadY J) x).Nonempty :=
  71. ⟨_, gadMin_mem P Q x⟩
  73. /-- `t219.main`, core: `P'` is constant on the argmin, equal to `1_S x`. -/
  74. theorem gadP_eq_indicator (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ)
  75. {x : Fin n → ℝ} {y : Unit ⊕ J → ℝ} (hy : y ∈ argminSet (gadQ P Q) (gadY J) x) :
  76. gadP P Q x y = (basicSet P Q).indicator 1 x := by
  77. classical
  78. rw [mem_argminSet_gadQ_iff] at hy
  79. obtain ⟨h1, h2⟩ := hy
  80. have e1 := mul_eq_of_isMin_univ h1
  81. have e2 : ∀ j, eval x (Q j) * y (Sum.inr j) = if 0 < eval x (Q j) then 1 else 0 :=
  82. fun j => mul_eq_of_isMin_Ici (h2 j).1 (h2 j).2
  83. have hP : gadP P Q x y = (1 - (if eval x P = 0 then 0 else 1)) *
  84. ∏ j, (if 0 < eval x (Q j) then (1 : ℝ) else 0) := by
  85. simp only [gadP, e2, mul_comm (y (Sum.inl ())), e1]
  86. rw [hP]
  87. by_cases hx : x ∈ basicSet P Q
  88. · rw [Set.indicator_of_mem hx]
  89. obtain ⟨hx1, hx2⟩ := hx
  90. simp [hx1, hx2]
  91. · rw [Set.indicator_of_notMem hx]
  92. simp only [basicSet, Set.mem_ofPred_eq, not_and_or, not_forall] at hx
  93. rcases hx with hx | ⟨j, hj⟩
  94. · simp [hx]
  95. · rw [Finset.prod_eq_zero (Finset.mem_univ j) (by simp [hj]), mul_zero]
  97. theorem isPolyFun_gadQ (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) :
  98. IsPolyFun (gadQ P Q) := by
  99. unfold gadQ
  100. exact (((isPolyFun_const 1).sub ((isPolyFun_y (Sum.inl ())).mul
  101. (IsPolyFun.of_upper_only P))).pow 2).add
  102. (isPolyFun_finset_sum Finset.univ fun j _ => ((isPolyFun_const 1).sub
  103. ((IsPolyFun.of_upper_only (Q j)).mul (isPolyFun_y (Sum.inr j)))).pow 2)
  105. theorem isPolyFun_gadP (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) :
  106. IsPolyFun (gadP P Q) := by
  107. unfold gadP
  108. exact ((isPolyFun_const 1).sub ((isPolyFun_y (Sum.inl ())).mul
  109. (IsPolyFun.of_upper_only P))).mul
  110. (isPolyFun_finset_prod Finset.univ fun j _ =>
  111. (IsPolyFun.of_upper_only (Q j)).mul (isPolyFun_y (Sum.inr j)))
  113. theorem convexLower_gadQ (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) :
  114. ConvexLower (gadQ P Q) := fun x =>
  115. ((convexOn_sq_one_sub_mul_coord (eval x P) (Sum.inl ())).add
  116. (convexOn_finset_sum convex_univ Finset.univ fun j _ =>
  117. convexOn_sq_one_sub_mul_coord (eval x (Q j)) (Sum.inr j))).congr
  118. (fun y _ => by simp [gadQ, mul_comm])
  120. theorem isUnboundedBox_gadY (J : Type*) : IsUnboundedBox (gadY J) :=
  121. isUnboundedBox_sum_univ_Ici
  123. /-- **Lemma 2.19** (`t219.main`, simplified gadget). -/
  124. theorem lemma219 (P : MvPolynomial (Fin n) ℝ) (Q : J → MvPolynomial (Fin n) ℝ) :
  125. IsPolyFun (gadP P Q) ∧ IsPolyFun (gadQ P Q) ∧ ConvexLower (gadQ P Q) ∧ IsUnboundedBox (gadY J) ∧
  126. (∀ x, (argminSet (gadQ P Q) (gadY J) x).Nonempty ∧
  127. ∀ y ∈ argminSet (gadQ P Q) (gadY J) x, gadP P Q x y = (basicSet P Q).indicator 1 x) ∧
  128. valueFun (gadP P Q) (gadQ P Q) (gadY J) = (fun x => (((basicSet P Q).indicator 1 x : ℝ) : EReal)) ∧
  129. pvalueFun (gadP P Q) (gadQ P Q) (gadY J) = (fun x => (((basicSet P Q).indicator 1 x : ℝ) : EReal)) :=
  130. ⟨isPolyFun_gadP P Q, isPolyFun_gadQ P Q, convexLower_gadQ P Q, isUnboundedBox_gadY J,
  131. fun x => ⟨argminSet_gadQ_nonempty P Q x, fun _ hy => gadP_eq_indicator P Q hy⟩,
  132. funext fun x => valueFun_eq_of_const (argminSet_gadQ_nonempty P Q x)
  133. (fun _ hy => gadP_eq_indicator P Q hy),
  134. funext fun x => pvalueFun_eq_of_const (argminSet_gadQ_nonempty P Q x)
  135. (fun _ hy => gadP_eq_indicator P Q hy)⟩
  137. /-- **Lemma 2.19**, existential form (paper statement, with constancy of `P'` on the argmin). -/
  138. theorem lemma219_exists {J : Type} [Fintype J] (P : MvPolynomial (Fin n) ℝ)
  139. (Q : J → MvPolynomial (Fin n) ℝ) :
  140. ∃ (ι : Type) (_ : Fintype ι) (P' Q' : (Fin n → ℝ) → (ι → ℝ) → ℝ) (Y : Set (ι → ℝ)),
  141. IsPolyFun P' ∧ IsPolyFun Q' ∧ ConvexLower Q' ∧ IsUnboundedBox Y ∧
  142. (∀ x, (argminSet Q' Y x).Nonempty ∧
  143. ∀ y ∈ argminSet Q' Y x, P' x y = (basicSet P Q).indicator 1 x) ∧
  144. valueFun P' Q' Y = (fun x => (((basicSet P Q).indicator 1 x : ℝ) : EReal)) ∧
  145. pvalueFun P' Q' Y = (fun x => (((basicSet P Q).indicator 1 x : ℝ) : EReal)) :=
  146. ⟨Unit ⊕ J, inferInstance, gadP P Q, gadQ P Q, gadY J, lemma219 P Q⟩
  148. end Lemma219
  150. end Bilevel