Mathlib.Optimization

theorem exists_rational_optimal_primal_dual (P : Program ι n) (hne : ∃ x, P.PrimalFeasible x) (hbdd : ∃ l : ℚ, ∀ x, P.PrimalFeasible x → l ≤ P.objective x) : ∃ (xStar : Fin n → ℚ) (yStar : ι → ℚ), P.PrimalFeasible xStar ∧ P.DualFeasible yStar ∧ P.objective xStar = P.dualObjective yStar ∧ ∀ x, P.PrimalFeasible x → P.objective xStar ≤ P.objective x := by let rows := P.finalCertifiedRows.map FinalCertifiedIneq.row have hrowsne : ∃ t : ℚ, ∀ r ∈ rows, r.Holds elim0 t := by obtain ⟨x, hx⟩ := hne refine ⟨P.objective x, ?_⟩ intro r hr simp only [rows, List.mem_map] at hr obtain ⟨d, hd, rfl⟩ := hr exact (finalCertifiedRows_iff P _).1 ⟨x, hx, rfl⟩ d hd have hrowsbdd : ∃ l : ℚ, ∀ t : ℚ, (∀ r ∈ rows, r.Holds elim0 t) → l ≤ t := by obtain ⟨l, hl⟩ := hbdd refine ⟨l, ?_⟩ intro t ht have hfinal : ∀ d ∈ P.finalCertifiedRows, d.row.Holds elim0 t := by intro d hd exact ht d.row (by change d.row ∈ P.finalCertifiedRows.map FinalCertifiedIneq.row exact List.mem_map.mpr ⟨d, hd, rfl⟩) obtain ⟨x, hx, hxt⟩ := (finalCertifiedRows_iff P t).2 hfinal simpa [← hxt] using hl x hx obtain ⟨v, hvfeas, hvmin, r, hrrows, hrneg, hrv⟩ := scalar_endpoint rows hrowsne hrowsbdd obtain ⟨d, hd, hdr⟩ : ∃ d ∈ P.finalCertifiedRows, d.row = r := by simpa only [rows, List.mem_map] using hrrows subst r obtain ⟨xStar, hxStar, hxval⟩ := (finalCertifiedRows_iff P v).2 (by intro e he exact hvfeas e.row (by change e.row ∈ P.finalCertifiedRows.map FinalCertifiedIneq.row exact List.mem_map.mpr ⟨e, he, rfl⟩)) let denom : ℚ := -d.row.objCoeff have hdenom : 0 < denom := by dsimp [denom]; linarith let yStar : ι → ℚ := fun i => d.weight (.inl i) / denom have hobjcomb : d.row.objCoeff = d.weight (.inr false) - d.weight (.inr true) := by rw [d.objCoeff_eq] simp [Program.certificateBase, Fintype.sum_sum_type, Fintype.sum_bool, sub_eq_add_neg, add_comm] have hcoeff (x : Fin n → ℚ) : (∑ i, d.weight (.inl i) * dotProduct (P.A i) x) - d.weight (.inr false) * dotProduct P.c x + d.weight (.inr true) * dotProduct P.c x = 0 := by have hc0 := d.coeff_zero x simp [Program.certificateBase, Fintype.sum_sum_type, Fintype.sum_bool, neg_dot] at hc0 linarith have hrhs : d.row.rhs = ∑ i, d.weight (.inl i) * P.b i := by rw [d.rhs_eq] simp [Program.certificateBase, Fintype.sum_sum_type, Fintype.sum_bool] refine ⟨xStar, yStar, hxStar, ?_, ?_, ?_⟩ · constructor · intro i exact div_nonneg (d.weight_nonneg (.inl i)) hdenom.le · intro j have hc := hcoeff (fun k => if k = j then 1 else 0) simp only [dotProduct, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, if_true] at hc dsimp [yStar] simp_rw [div_mul_eq_mul_div] rw [← Finset.sum_div] apply (div_eq_iff hdenom.ne').2 dsimp [denom] rw [hobjcomb] ring_nf at hc ⊢ linarith · rw [hxval, ← hrv] dsimp [Program.dualObjective, yStar] simp_rw [div_mul_eq_mul_div] rw [← Finset.sum_div, ← hrhs] dsimp [denom] field_simp · intro x hx rw [hxval] apply hvmin (P.objective x) intro rr hrr simp only [rows, List.mem_map] at hrr obtain ⟨e, he, rfl⟩ := hrr exact (finalCertifiedRows_iff P _).1 ⟨x, hx, rfl⟩ e he

lemma weighted_simplex_active_set (M : ℝ) (hM : 0 < M) (α β : Fin 3 → ℝ) (kappa : ℝ) (hβ : ∀ i, 0 < β i) (hk0 : 0 ≤ kappa) : (0 < kappa → ∃! p : Finset (Fin 3) × ℝ, IsAdmissibleSupport α β kappa p.1 p.2 ∧ InSimplex M (activeSetPoint M α β p.1 p.2) ∧ (∀ s : Fin 3 → ℝ, InSimplex M s → s ≠ activeSetPoint M α β p.1 p.2 → wsObj α β kappa (activeSetPoint M α β p.1 p.2) < wsObj α β kappa s) ∧ wsObj α β kappa (activeSetPoint M α β p.1 p.2) = M * p.2) ∧ (kappa = 0 → ∀ t : Fin 3 → ℝ, (InSimplex M t ∧ ∀ s : Fin 3 → ℝ, InSimplex M s → wsObj α β kappa t ≤ wsObj α β kappa s) ↔ t ∈ exposedMinFace M α) := by refine ⟨fun hk => ?_, fun hk => ?_⟩ · -- κ > 0: unique admissible pair, active-set point is the strict minimizer, value M·λ. obtain ⟨S, lam, hadm⟩ := exists_admissible α β kappa hβ hk refine ⟨(S, lam), ⟨hadm, activeSetPoint_mem M α β S lam hM.le (fun i _ => hβ i) hadm.1 hadm.2.2.1, activeSetPoint_strict_min M α β kappa S lam hM hβ hk hadm, activeSetPoint_value M α β kappa S lam hM.le (fun i _ => hβ i) hk hadm.1 hadm.2.2.1 hadm.2.1⟩, ?_⟩ rintro ⟨S', lam'⟩ ⟨hadm', hmem', hmin', hval'⟩ -- The two active-set points coincide (each is the strict minimizer of the SOCP). set t := activeSetPoint M α β S lam with ht set t' := activeSetPoint M α β S' lam' with ht' have hmin : ∀ s : Fin 3 → ℝ, InSimplex M s → s ≠ t → wsObj α β kappa t < wsObj α β kappa s := activeSetPoint_strict_min M α β kappa S lam hM hβ hk hadm have htt' : t = t' := by by_contra hne have h1 : wsObj α β kappa t < wsObj α β kappa t' := hmin t' (activeSetPoint_mem M α β S' lam' hM.le (fun i _ => hβ i) hadm'.1 hadm'.2.2.1) (fun h => hne h.symm) have h2 : wsObj α β kappa t' < wsObj α β kappa t := hmin' t (activeSetPoint_mem M α β S lam hM.le (fun i _ => hβ i) hadm.1 hadm.2.2.1) (fun h => hne h) exact lt_irrefl _ (h1.trans h2) -- Supports agree: `i ∈ S ↔ 0 < tᵢ = t'ᵢ ↔ i ∈ S'`. have hSS' : S = S' := by ext i rw [← activeSetPoint_pos_iff M α β S lam hM (fun i _ => hβ i) hadm.1 hadm.2.2.1 i, ← activeSetPoint_pos_iff M α β S' lam' hM (fun i _ => hβ i) hadm'.1 hadm'.2.2.1 i, ← ht, ← ht', htt'] -- Multipliers agree via the value formula `M·λ = wsObj t = wsObj t' = M·λ'`. have hlam : lam = lam' := by have hv : M * lam = M * lam' := by rw [← activeSetPoint_value M α β kappa S lam hM.le (fun i _ => hβ i) hk hadm.1 hadm.2.2.1 hadm.2.1, ← ht, htt', ht', activeSetPoint_value M α β kappa S' lam' hM.le (fun i _ => hβ i) hk hadm'.1 hadm'.2.2.1 hadm'.2.1] exact mul_left_cancel₀ (ne_of_gt hM) hv exact Prod.ext hSS'.symm hlam.symm · -- κ = 0: minimizer set is the exposed α-minimizing face. subst hk intro t simpa [wsObj] using kappa_zero_face M α t

lemma trunc_from_minimizer (M d : ℝ) (hdM : d ≤ M) (α β : Fin 3 → ℝ) (kappa : ℝ) (hβ0 : 0 ≤ β 0) (hβy : β 1 = 1) (hβz : β 2 = 1) (hk : 0 ≤ kappa) (t_rel : Fin 3 → ℝ) (hrel : InSimplex M t_rel) (hmin : ∀ s, InSimplex M s → wsObj α β kappa t_rel ≤ wsObj α β kappa s) : (InTruncSimplex M d t_rel → ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa t_rel ≤ wsObj α β kappa s) ∧ (¬ (d ≤ t_rel 1 + t_rel 2) → InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧ ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa)) ≤ wsObj α β kappa s) := by have hβnn : ∀ i, 0 ≤ β i := by intro i fin_cases i · exact hβ0 · change 0 ≤ β 1 linarith [hβy] · change 0 ≤ β 2 linarith [hβz] refine ⟨fun _ s hs => hmin s hs.1, ?_⟩ intro hinf' have hinf : t_rel 1 + t_rel 2 < d := not_le.mp hinf' have hdpos : 0 < d := by have h1 := hrel.1 1; have h2 := hrel.1 2; linarith obtain ⟨hs0, hsd⟩ := truncSelector_mem M d α β kappa hdpos hβ0 hk set sStar := truncSelector M d α β kappa with hsStar have e0 : truncSegPoint M d sStar 0 = M - d := by simp [truncSegPoint] have e1 : truncSegPoint M d sStar 1 = sStar := by simp [truncSegPoint] have e2 : truncSegPoint M d sStar 2 = d - sStar := by simp [truncSegPoint] have n0 : 0 ≤ truncSegPoint M d sStar 0 := by rw [e0]; linarith have n1 : 0 ≤ truncSegPoint M d sStar 1 := by rw [e1]; linarith have n2 : 0 ≤ truncSegPoint M d sStar 2 := by rw [e2]; linarith have hfeas : InTruncSimplex M d (truncSegPoint M d sStar) := by refine ⟨⟨?_, ?_⟩, ?_⟩ · intro i fin_cases i · exact n0 · exact n1 · exact n2 · rw [Fin.sum_univ_three, e0, e1, e2]; ring · rw [e1, e2]; linarith refine ⟨hfeas, ?_⟩ intro s hs obtain ⟨σ, hσ0, hσd, hred⟩ := truncSeg_reduction M d kappa α β hβnn hk t_rel hrel hmin hinf s hs calc wsObj α β kappa (truncSegPoint M d sStar) ≤ wsObj α β kappa (truncSegPoint M d σ) := truncSeg_selector_le M d α β kappa hdpos hβ0 hβy hβz hk σ hσ0 hσd _ ≤ wsObj α β kappa s := hred

lemma weighted_simplex_truncation (M d : ℝ) (hM : 0 < M) (hdM : d ≤ M) (α β : Fin 3 → ℝ) (kappa : ℝ) (hβ : ∀ i, 0 < β i) (hβy : β 1 = 1) (hβz : β 2 = 1) (hk : 0 ≤ kappa) : (0 < kappa → ∀ (S : Finset (Fin 3)) (lam : ℝ), IsAdmissibleSupport α β kappa S lam → (InTruncSimplex M d (activeSetPoint M α β S lam) → ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (activeSetPoint M α β S lam) ≤ wsObj α β kappa s) ∧ (¬ (d ≤ activeSetPoint M α β S lam 1 + activeSetPoint M α β S lam 2) → InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧ ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa)) ≤ wsObj α β kappa s)) ∧ (kappa = 0 → ∀ t_rel : Fin 3 → ℝ, t_rel ∈ exposedMinFace M α → (InTruncSimplex M d t_rel → ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa t_rel ≤ wsObj α β kappa s) ∧ (¬ (d ≤ t_rel 1 + t_rel 2) → InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧ ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa)) ≤ wsObj α β kappa s)) := by constructor · -- κ > 0 intro hkpos S lam hadm obtain ⟨hsimp, hmin⟩ := activeSetPoint_isMinimizer M hM α β kappa hβ hkpos S lam hadm exact trunc_from_minimizer M d hdM α β kappa (hβ 0).le hβy hβz hk _ hsimp hmin · -- κ = 0 intro hk0 t_rel hface subst hk0 have hsimp : InSimplex M t_rel := hface.1 have hmin : ∀ s, InSimplex M s → wsObj α β 0 t_rel ≤ wsObj α β 0 s := exposedMinFace_isMinimizer M α β t_rel hface exact trunc_from_minimizer M d hdM α β 0 (hβ 0).le hβy hβz le_rfl _ hsimp hmin

lemma wsObj_segment_le (α β : Fin 3 → ℝ) (kappa : ℝ) (hβ : ∀ i, 0 ≤ β i) (hk : 0 ≤ kappa) (u v : Fin 3 → ℝ) (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) : wsObj α β kappa (fun i => (1 - θ) * u i + θ * v i) ≤ (1 - θ) * wsObj α β kappa u + θ * wsObj α β kappa v := by unfold wsObj have hlin : (∑ i, α i * ((1 - θ) * u i + θ * v i)) = (1 - θ) * (∑ i, α i * u i) + θ * (∑ i, α i * v i) := by repeat rw [Fin.sum_univ_three] ring have hsqrt := weighted_sqrt_segment_le β hβ u v θ hθ0 hθ1 calc (∑ i, α i * ((1 - θ) * u i + θ * v i)) + kappa * sqrt (∑ i, β i * ((1 - θ) * u i + θ * v i) ^ 2) ≤ (1 - θ) * (∑ i, α i * u i) + θ * (∑ i, α i * v i) + kappa * ((1 - θ) * sqrt (∑ i, β i * u i ^ 2) + θ * sqrt (∑ i, β i * v i ^ 2)) := by rw [hlin] exact add_le_add (le_refl _) (mul_le_mul_of_nonneg_left hsqrt hk) _ = (1 - θ) * ((∑ i, α i * u i) + kappa * sqrt (∑ i, β i * u i ^ 2)) + θ * ((∑ i, α i * v i) + kappa * sqrt (∑ i, β i * v i ^ 2)) := by ring

lemma truncSeg_reduction (M d kappa : ℝ) (α β : Fin 3 → ℝ) (hβ : ∀ i, 0 ≤ β i) (hk : 0 ≤ kappa) (t_rel : Fin 3 → ℝ) (hrel : InSimplex M t_rel) (hmin : ∀ s, InSimplex M s → wsObj α β kappa t_rel ≤ wsObj α β kappa s) (hinf : t_rel 1 + t_rel 2 < d) (t : Fin 3 → ℝ) (ht : InTruncSimplex M d t) : ∃ σ, 0 ≤ σ ∧ σ ≤ d ∧ wsObj α β kappa (truncSegPoint M d σ) ≤ wsObj α β kappa t := by set S : ℝ := t 1 + t 2 set P : ℝ := t_rel 1 + t_rel 2 have hS_ge : d ≤ S := by simpa [S] using ht.2 have hP_lt_d : P < d := by simpa [P] using hinf rcases eq_or_lt_of_le hS_ge with hS_eq | hd_lt_S · refine ⟨t 1, ht.1.1 1, ?_, ?_⟩ · have ht2 := ht.1.1 2 have hface : t 1 + t 2 = d := by simpa [S] using hS_eq.symm linarith · have hface : t 1 + t 2 = d := by simpa [S] using hS_eq.symm have ht_eq := eq_truncSegPoint_of_simplex_face M d t ht.1 hface rw [← ht_eq] · set θ : ℝ := (S - d) / (S - P) with hθ_def set t_b : Fin 3 → ℝ := fun i => (1 - θ) * t i + θ * t_rel i have hden_pos : 0 < S - P := by linarith have hden_ne : S - P ≠ 0 := by linarith have hθ0 : 0 ≤ θ := by have hnum : 0 ≤ S - d := by linarith exact div_nonneg hnum hden_pos.le have hθmul : θ * (S - P) = S - d := by rw [hθ_def] field_simp [hden_ne] have hθ1 : θ ≤ 1 := by have hnum_le : S - d ≤ S - P := by linarith nlinarith have hθc : 0 ≤ 1 - θ := by linarith have ht_b12 : t_b 1 + t_b 2 = d := by simp [t_b] nlinarith have ht_b_simplex : InSimplex M t_b := by refine ⟨?_, ?_⟩ · intro i have hti := ht.1.1 i have hri := hrel.1 i nlinarith [mul_nonneg hθc hti, mul_nonneg hθ0 hri] · have hsumt := ht.1.2 have hsumr := hrel.2 rw [Fin.sum_univ_three] at hsumt hsumr rw [Fin.sum_univ_three] simp [t_b] nlinarith refine ⟨t_b 1, ht_b_simplex.1 1, ?_, ?_⟩ · have ht_b2 := ht_b_simplex.1 2 linarith · have ht_b_eq := eq_truncSegPoint_of_simplex_face M d t_b ht_b_simplex ht_b12 have hconv : wsObj α β kappa t_b ≤ (1 - θ) * wsObj α β kappa t + θ * wsObj α β kappa t_rel := by simpa [t_b] using wsObj_segment_le α β kappa hβ hk t t_rel θ hθ0 hθ1 have hrel_le_t : wsObj α β kappa t_rel ≤ wsObj α β kappa t := hmin t ht.1 have hcomb_le : (1 - θ) * wsObj α β kappa t + θ * wsObj α β kappa t_rel ≤ wsObj α β kappa t := by nlinarith [mul_le_mul_of_nonneg_left hrel_le_t hθ0] calc wsObj α β kappa (truncSegPoint M d (t_b 1)) = wsObj α β kappa t_b := by rw [← ht_b_eq] _ ≤ (1 - θ) * wsObj α β kappa t + θ * wsObj α β kappa t_rel := hconv _ ≤ wsObj α β kappa t := hcomb_le

lemma activeSetPoint_isMinimizer (M : ℝ) (hM : 0 < M) (α β : Fin 3 → ℝ) (kappa : ℝ) (hβ : ∀ i, 0 < β i) (hkpos : 0 < kappa) (S : Finset (Fin 3)) (lam : ℝ) (hadm : IsAdmissibleSupport α β kappa S lam) : InSimplex M (activeSetPoint M α β S lam) ∧ ∀ s : Fin 3 → ℝ, InSimplex M s → wsObj α β kappa (activeSetPoint M α β S lam) ≤ wsObj α β kappa s := by classical rcases hadm with ⟨hSne, hsum, hact, hoff⟩ let t : Fin 3 → ℝ := activeSetPoint M α β S lam let D : ℝ := ∑ h ∈ S, (lam - α h) / β h have hDpos : 0 < D := by dsimp [D] exact Finset.sum_pos (fun i hi => div_pos (sub_pos.mpr (hact i hi)) (hβ i)) hSne have htS : ∀ i, i ∈ S → t i = M * ((lam - α i) / β i) / D := by intro i hi simp [t, activeSetPoint, hi, D] have htOff : ∀ i, i ∉ S → t i = 0 := by intro i hi simp [t, activeSetPoint, hi] have htpos : ∀ i, i ∈ S → 0 < t i := by intro i hi rw [htS i hi] exact div_pos (mul_pos hM (div_pos (sub_pos.mpr (hact i hi)) (hβ i))) hDpos have ht_nonneg : ∀ i, 0 ≤ t i := by intro i by_cases hi : i ∈ S · exact (htpos i hi).le · rw [htOff i hi] have hsum_t_support : (∑ i, t i) = ∑ i ∈ S, M * ((lam - α i) / β i) / D := by calc (∑ i, t i) = ∑ i, if i ∈ S then M * ((lam - α i) / β i) / D else 0 := by apply Finset.sum_congr rfl intro i _ by_cases hi : i ∈ S · simp [hi, htS i hi] · simp [hi, htOff i hi] _ = ∑ i ∈ S, M * ((lam - α i) / β i) / D := by simp have hsum_t : ∑ i, t i = M := by rw [hsum_t_support] calc (∑ i ∈ S, M * ((lam - α i) / β i) / D) = ∑ i ∈ S, (M / D) * ((lam - α i) / β i) := by apply Finset.sum_congr rfl intro i _ field_simp [hDpos.ne'] _ = (M / D) * ∑ i ∈ S, (lam - α i) / β i := by rw [Finset.mul_sum] _ = (M / D) * D := by rfl _ = M := by field_simp [hDpos.ne'] have ht_simplex : InSimplex M t := ⟨ht_nonneg, hsum_t⟩ refine ⟨ht_simplex, ?_⟩ intro s hs let Nt : ℝ := sqrt (∑ i, β i * t i ^ 2) let Ns : ℝ := sqrt (∑ i, β i * s i ^ 2) have ht_sq_nonneg : 0 ≤ ∑ i, β i * t i ^ 2 := by exact sum_nonneg (fun i _ => mul_nonneg (hβ i).le (sq_nonneg (t i))) have hs_sq_nonneg : 0 ≤ ∑ i, β i * s i ^ 2 := by exact sum_nonneg (fun i _ => mul_nonneg (hβ i).le (sq_nonneg (s i))) have hNt_sq : Nt ^ 2 = ∑ i, β i * t i ^ 2 := by dsimp [Nt] rw [Real.sq_sqrt ht_sq_nonneg] have hNs_sq : Ns ^ 2 = ∑ i, β i * s i ^ 2 := by dsimp [Ns] rw [Real.sq_sqrt hs_sq_nonneg] have hquad_support : (∑ i, β i * t i ^ 2) = ∑ i ∈ S, β i * (M * ((lam - α i) / β i) / D) ^ 2 := by calc (∑ i, β i * t i ^ 2) = ∑ i, if i ∈ S then β i * (M * ((lam - α i) / β i) / D) ^ 2 else 0 := by apply Finset.sum_congr rfl intro i _ by_cases hi : i ∈ S · simp [hi, htS i hi] · simp [hi, htOff i hi] _ = ∑ i ∈ S, β i * (M * ((lam - α i) / β i) / D) ^ 2 := by simp have hquad : (∑ i, β i * t i ^ 2) = M ^ 2 * kappa ^ 2 / D ^ 2 := by rw [hquad_support] calc (∑ i ∈ S, β i * (M * ((lam - α i) / β i) / D) ^ 2) = ∑ i ∈ S, (M ^ 2 / D ^ 2) * ((lam - α i) ^ 2 / β i) := by apply Finset.sum_congr rfl intro i _ field_simp [(hβ i).ne', hDpos.ne'] _ = (M ^ 2 / D ^ 2) * ∑ i ∈ S, (lam - α i) ^ 2 / β i := by rw [Finset.mul_sum] _ = (M ^ 2 / D ^ 2) * kappa ^ 2 := by rw [hsum] _ = M ^ 2 * kappa ^ 2 / D ^ 2 := by field_simp [hDpos.ne'] have hNt_nonneg : 0 ≤ Nt := by dsimp [Nt] exact Real.sqrt_nonneg _ have hNt_formula : Nt = M * kappa / D := by have hright_nonneg : 0 ≤ M * kappa / D := by positivity apply (Real.sqrt_eq_iff_mul_self_eq ht_sq_nonneg hright_nonneg).2 rw [hquad] field_simp [hDpos.ne'] have hNtpos : 0 < Nt := by rw [hNt_formula] positivity have hcoord : ∀ i, i ∈ S → kappa * (β i * t i) = (lam - α i) * Nt := by intro i hi rw [htS i hi, hNt_formula] field_simp [(hβ i).ne', hDpos.ne'] have hCS : (∑ i, β i * t i * s i) ≤ Nt * Ns := by exact (le_abs_self _).trans (by simpa [Nt, Ns, mul_assoc] using abs_weighted_inner_le (Finset.univ : Finset (Fin 3)) β t s (fun i _ => (hβ i).le)) have hcross_eq : ∀ y : Fin 3 → ℝ, kappa * (∑ i, β i * t i * y i) = Nt * ∑ i ∈ S, (lam - α i) * y i := by intro y calc kappa * (∑ i, β i * t i * y i) = ∑ i, (kappa * (β i * t i)) * y i := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i _ ring _ = ∑ i, if i ∈ S then ((lam - α i) * Nt) * y i else 0 := by apply Finset.sum_congr rfl intro i _ by_cases hi : i ∈ S · simp [hi, hcoord i hi] · simp [hi, htOff i hi] _ = ∑ i ∈ S, ((lam - α i) * Nt) * y i := by simp _ = Nt * ∑ i ∈ S, (lam - α i) * y i := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i _ ring have hsupport_s_bound : (∑ i ∈ S, (lam - α i) * s i) ≤ kappa * Ns := by have hmul := mul_le_mul_of_nonneg_left hCS hkpos.le rw [hcross_eq s] at hmul have hmul' : Nt * (∑ i ∈ S, (lam - α i) * s i) ≤ Nt * (kappa * Ns) := by simpa [mul_assoc, mul_left_comm, mul_comm] using hmul exact le_of_mul_le_mul_left hmul' hNtpos have hcross_tt : (∑ i, β i * t i * t i) = Nt ^ 2 := by calc (∑ i, β i * t i * t i) = ∑ i, β i * t i ^ 2 := by apply Finset.sum_congr rfl intro i _ ring _ = Nt ^ 2 := hNt_sq.symm have hsupport_t_eq : (∑ i ∈ S, (lam - α i) * t i) = kappa * Nt := by have h := hcross_eq t rw [hcross_tt] at h have h' : Nt * (∑ i ∈ S, (lam - α i) * t i) = Nt * (kappa * Nt) := by calc Nt * (∑ i ∈ S, (lam - α i) * t i) = kappa * Nt ^ 2 := h.symm _ = Nt * (kappa * Nt) := by ring exact mul_left_cancel₀ hNtpos.ne' h' have hsum_t_compl : (∑ i ∈ Sᶜ, t i) = 0 := by apply Finset.sum_eq_zero intro i hi exact htOff i (by simpa using hi) have hsum_t_S : (∑ i ∈ S, t i) = M := by calc (∑ i ∈ S, t i) = (∑ i, t i) := by rw [← Finset.sum_add_sum_compl S t, hsum_t_compl, add_zero] _ = M := hsum_t have halpha_t_compl : (∑ i ∈ Sᶜ, α i * t i) = 0 := by apply Finset.sum_eq_zero intro i hi simp [htOff i (by simpa using hi)] have halpha_t_support : (∑ i, α i * t i) = ∑ i ∈ S, α i * t i := by rw [← Finset.sum_add_sum_compl S (fun i => α i * t i), halpha_t_compl, add_zero] have hvalue_t : wsObj α β kappa t = lam * M := by calc wsObj α β kappa t = (∑ i, α i * t i) + kappa * Nt := by simp [wsObj, Nt] _ = (∑ i ∈ S, α i * t i) + ∑ i ∈ S, (lam - α i) * t i := by rw [halpha_t_support, hsupport_t_eq] _ = ∑ i ∈ S, lam * t i := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i _ ring _ = lam * ∑ i ∈ S, t i := by rw [Finset.mul_sum] _ = lam * M := by rw [hsum_t_S] have hoff_s_bound : (∑ i ∈ Sᶜ, lam * s i) ≤ ∑ i ∈ Sᶜ, α i * s i := by apply Finset.sum_le_sum intro i hi exact mul_le_mul_of_nonneg_right (hoff i (by simpa using hi)) (hs.1 i) have hlinear_s_bound : lam * M ≤ (∑ i, α i * s i) + ∑ i ∈ S, (lam - α i) * s i := by have hsplit_lam := Finset.sum_add_sum_compl S (fun i => lam * s i) have hsplit_alpha := Finset.sum_add_sum_compl S (fun i => α i * s i) have hactive : (∑ i ∈ S, α i * s i) + ∑ i ∈ S, (lam - α i) * s i = ∑ i ∈ S, lam * s i := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i _ ring have hfull_lam : (∑ i, lam * s i) = lam * M := by calc (∑ i, lam * s i) = lam * ∑ i, s i := by rw [Finset.mul_sum] _ = lam * M := by rw [hs.2] calc lam * M = ∑ i, lam * s i := hfull_lam.symm _ = (∑ i ∈ S, lam * s i) + ∑ i ∈ Sᶜ, lam * s i := hsplit_lam.symm _ ≤ (∑ i ∈ S, lam * s i) + ∑ i ∈ Sᶜ, α i * s i := by simpa [add_comm, add_left_comm, add_assoc] using add_le_add_left hoff_s_bound (∑ i ∈ S, lam * s i) _ = (∑ i, α i * s i) + ∑ i ∈ S, (lam - α i) * s i := by rw [← hactive, ← hsplit_alpha] ring have hvalue_s : lam * M ≤ wsObj α β kappa s := by calc lam * M ≤ (∑ i, α i * s i) + ∑ i ∈ S, (lam - α i) * s i := hlinear_s_bound _ ≤ (∑ i, α i * s i) + kappa * Ns := by simpa [add_comm, add_left_comm, add_assoc] using add_le_add_left hsupport_s_bound (∑ i, α i * s i) _ = wsObj α β kappa s := by simp [wsObj, Ns] calc wsObj α β kappa (activeSetPoint M α β S lam) = wsObj α β kappa t := by simp [t] _ = lam * M := hvalue_t _ ≤ wsObj α β kappa s := hvalue_s

lemma exposedMinFace_isMinimizer (M : ℝ) (α β : Fin 3 → ℝ) (t_rel : Fin 3 → ℝ) (hface : t_rel ∈ exposedMinFace M α) : ∀ s : Fin 3 → ℝ, InSimplex M s → wsObj α β 0 t_rel ≤ wsObj α β 0 s := by simpa [wsObj] using ((kappa_zero_face M α t_rel).2 hface).2

lemma wsObj_truncSeg_eq (M d : ℝ) (α β : Fin 3 → ℝ) (kappa σ : ℝ) : wsObj α β kappa (truncSegPoint M d σ) = α 0 * (M - d) + α 1 * σ + α 2 * (d - σ) + kappa * sqrt (β 0 * (M - d) ^ 2 + β 1 * σ ^ 2 + β 2 * (d - σ) ^ 2) := by unfold wsObj truncSegPoint rw [Fin.sum_univ_three, Fin.sum_univ_three] simp [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two]

lemma truncSeg_selector_le (M d : ℝ) (α β : Fin 3 → ℝ) (kappa : ℝ) (hd : 0 < d) (hβ0 : 0 ≤ β 0) (hβy : β 1 = 1) (hβz : β 2 = 1) (hk : 0 ≤ kappa) (σ : ℝ) (hσ0 : 0 ≤ σ) (hσd : σ ≤ d) : wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa)) ≤ wsObj α β kappa (truncSegPoint M d σ) := by set s := truncSelector M d α β kappa with hs rw [wsObj_truncSeg_eq M d α β kappa s, wsObj_truncSeg_eq M d α β kappa σ] simp only [hβy, hβz, one_mul] set A := β 0 * (M - d) ^ 2 with hAdef set δ := α 1 - α 2 with hδdef let Rs := A + s ^ 2 + (d - s) ^ 2 let Rσ := A + σ ^ 2 + (d - σ) ^ 2 let rs := Real.sqrt Rs let rσ := Real.sqrt Rσ have hA : 0 ≤ A := by dsimp [A] exact mul_nonneg hβ0 (sq_nonneg _) have hRs_pos : 0 < Rs := by dsimp [Rs] exact truncSeg_radicand_pos hA hd have hRσ_pos : 0 < Rσ := by dsimp [Rσ] exact truncSeg_radicand_pos hA hd have hrs_pos : 0 < rs := by exact Real.sqrt_pos.2 hRs_pos have hrs_sq : rs ^ 2 = Rs := by simp [rs, Real.sq_sqrt (le_of_lt hRs_pos)] have hCS : A + s * σ + (d - s) * (d - σ) ≤ rs * rσ := by simpa [rs, rσ, Rs, Rσ] using truncSeg_cs_sqrt (A := A) (d := d) (s := s) (σ := σ) hA have hcross_id : A + s * σ + (d - s) * (d - σ) - Rs = (σ - s) * (2 * s - d) := by dsimp [Rs] ring have hdiff : (σ - s) * (2 * s - d) ≤ rs * rσ - rs * rs := by nlinarith [hCS, hcross_id, hrs_sq] have hkdiff : kappa * ((σ - s) * (2 * s - d)) ≤ kappa * (rs * rσ - rs * rs) := mul_le_mul_of_nonneg_left hdiff hk have hs_core : s = if kappa * d / Real.sqrt (A + d ^ 2) ≤ δ then 0 else if δ ≤ -(kappa * d / Real.sqrt (A + d ^ 2)) then d else (d - δ * Real.sqrt ((A + d ^ 2 / 2) / (kappa ^ 2 - δ ^ 2 / 2))) / 2 := by rw [hs] simp [truncSelector, A, δ] have hsign : 0 ≤ (σ - s) * (rs * δ + kappa * (2 * s - d)) := by have hsign_core := truncSelector_sign_core (A := A) (d := d) (kappa := kappa) (δ := δ) (σ := σ) hd hA hk hσ0 hσd dsimp only at hsign_core rw [← hs_core] at hsign_core simpa [rs, Rs] using hsign_core have hmul_nonneg : 0 ≤ rs * (δ * (σ - s) + kappa * (rσ - rs)) := by nlinarith [hsign, hkdiff] have hnonneg : 0 ≤ δ * (σ - s) + kappa * (rσ - rs) := by have hmul' : 0 ≤ (δ * (σ - s) + kappa * (rσ - rs)) * rs := by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul_nonneg exact nonneg_of_mul_nonneg_left hmul' hrs_pos have hslice_delta : δ * s + kappa * rs ≤ δ * σ + kappa * rσ := by nlinarith have hslice : α 1 * s + α 2 * (d - s) + kappa * rs ≤ α 1 * σ + α 2 * (d - σ) + kappa * rσ := by nlinarith [hslice_delta] dsimp [rs, rσ, Rs, Rσ, A] nlinarith [hslice]

lemma weighted_cs_sq {ι : Type*} [Fintype ι] (β s t : ι → ℝ) (hβ : ∀ i, 0 ≤ β i) : (∑ i, β i * (s i * t i)) ^ 2 ≤ (∑ i, β i * s i ^ 2) * (∑ i, β i * t i ^ 2) := by simpa using Analysis.weighted_inner_sq_le (Finset.univ : Finset ι) β s t (fun i _ => hβ i)

lemma weighted_cs_simplex_strict (M : ℝ) (hM : M ≠ 0) (β s t : Fin 3 → ℝ) (hβ : ∀ i, 0 < β i) (hs : ∑ i, s i = M) (ht : ∑ i, t i = M) (hne : s ≠ t) : (∑ i, β i * (s i * t i)) < sqrt (∑ i, β i * s i ^ 2) * sqrt (∑ i, β i * t i ^ 2) := by let P : ℝ := ∑ i, β i * s i ^ 2 let Q : ℝ := ∑ i, β i * t i ^ 2 let R : ℝ := ∑ i, β i * (s i * t i) have hP_nonneg : 0 ≤ P := by simp only [P, Fin.sum_univ_three] nlinarith [mul_nonneg (hβ 0).le (sq_nonneg (s 0)), mul_nonneg (hβ 1).le (sq_nonneg (s 1)), mul_nonneg (hβ 2).le (sq_nonneg (s 2))] have hle : R ^ 2 ≤ P * Q := by simpa [P, Q, R] using weighted_cs_sq β s t (fun i => (hβ i).le) have hlt : R ^ 2 < P * Q := by refine lt_of_le_of_ne hle ?_ intro heq have hgap_id : P * Q - R ^ 2 = β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 + β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 + β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 := by simp only [P, Q, R, Fin.sum_univ_three] ring have hgap_zero : P * Q - R ^ 2 = 0 := by nlinarith have hsum_zero : β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 + β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 + β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 = 0 := by nlinarith have h01_nonneg : 0 ≤ β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 := mul_nonneg (mul_nonneg (hβ 0).le (hβ 1).le) (sq_nonneg (s 0 * t 1 - s 1 * t 0)) have h02_nonneg : 0 ≤ β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 := mul_nonneg (mul_nonneg (hβ 0).le (hβ 2).le) (sq_nonneg (s 0 * t 2 - s 2 * t 0)) have h12_nonneg : 0 ≤ β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 := mul_nonneg (mul_nonneg (hβ 1).le (hβ 2).le) (sq_nonneg (s 1 * t 2 - s 2 * t 1)) have h01_zero : β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 = 0 := by nlinarith have h02_zero : β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 = 0 := by nlinarith have h12_zero : β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 = 0 := by nlinarith have h01 : s 0 * t 1 - s 1 * t 0 = 0 := by have hpos : 0 < β 0 * β 1 := mul_pos (hβ 0) (hβ 1) have hsquare : (s 0 * t 1 - s 1 * t 0) ^ 2 = 0 := resolve_left (mul_eq_zero.mp h01_zero) (ne_of_gt hpos) exact sq_eq_zero_iff.mp hsquare have h02 : s 0 * t 2 - s 2 * t 0 = 0 := by have hpos : 0 < β 0 * β 2 := mul_pos (hβ 0) (hβ 2) have hsquare : (s 0 * t 2 - s 2 * t 0) ^ 2 = 0 := resolve_left (mul_eq_zero.mp h02_zero) (ne_of_gt hpos) exact sq_eq_zero_iff.mp hsquare have h12 : s 1 * t 2 - s 2 * t 1 = 0 := by have hpos : 0 < β 1 * β 2 := mul_pos (hβ 1) (hβ 2) have hsquare : (s 1 * t 2 - s 2 * t 1) ^ 2 = 0 := resolve_left (mul_eq_zero.mp h12_zero) (ne_of_gt hpos) exact sq_eq_zero_iff.mp hsquare have h01eq : s 0 * t 1 = s 1 * t 0 := sub_eq_zero.mp h01 have h02eq : s 0 * t 2 = s 2 * t 0 := sub_eq_zero.mp h02 have h12eq : s 1 * t 2 = s 2 * t 1 := sub_eq_zero.mp h12 have hs3 : s 0 + s 1 + s 2 = M := by simpa only [Fin.sum_univ_three] using hs have ht3 : t 0 + t 1 + t 2 = M := by simpa only [Fin.sum_univ_three] using ht have hst : s = t := by by_cases ht0 : t 0 = 0 · by_cases ht1 : t 1 = 0 · by_cases ht2 : t 2 = 0 · exfalso exact hM (by linarith only [ht3, ht0, ht1, ht2]) · have hs2 : s 2 = t 2 := by have hscale : M * s 2 = M * t 2 := by calc M * s 2 = s 2 * M := by ring _ = s 2 * (t 0 + t 1 + t 2) := by rw [ht3] _ = (s 0 + s 1 + s 2) * t 2 := by nlinarith only [h02, h12] _ = M * t 2 := by rw [hs3] exact mul_left_cancel₀ hM hscale have hs0 : s 0 = t 0 := by have hs0_zero : s 0 = 0 := by have hmul : s 0 * t 2 = 0 := by rw [h02eq, ht0, mul_zero] exact (mul_eq_zero.mp hmul).resolve_right ht2 rw [hs0_zero, ht0] have hs1 : s 1 = t 1 := by have hs1_zero : s 1 = 0 := by have hmul : s 1 * t 2 = 0 := by rw [h12eq, ht1, mul_zero] exact (mul_eq_zero.mp hmul).resolve_right ht2 rw [hs1_zero, ht1] funext i fin_cases i <;> assumption · have hs1 : s 1 = t 1 := by have hscale : M * s 1 = M * t 1 := by calc M * s 1 = s 1 * M := by ring _ = s 1 * (t 0 + t 1 + t 2) := by rw [ht3] _ = (s 0 + s 1 + s 2) * t 1 := by nlinarith only [h01, h12] _ = M * t 1 := by rw [hs3] exact mul_left_cancel₀ hM hscale have hs0 : s 0 = t 0 := by have hs0_zero : s 0 = 0 := by have hmul : s 0 * t 1 = 0 := by rw [h01eq, ht0, mul_zero] exact (mul_eq_zero.mp hmul).resolve_right ht1 rw [hs0_zero, ht0] have hs2 : s 2 = t 2 := by have hmul : t 1 * t 2 = t 1 * s 2 := by calc t 1 * t 2 = s 1 * t 2 := by rw [hs1] _ = s 2 * t 1 := h12eq _ = t 1 * s 2 := by ring exact (mul_left_cancel₀ ht1 hmul).symm funext i fin_cases i <;> assumption · have hs0 : s 0 = t 0 := by have hscale : M * s 0 = M * t 0 := by calc M * s 0 = s 0 * M := by ring _ = s 0 * (t 0 + t 1 + t 2) := by rw [ht3] _ = (s 0 + s 1 + s 2) * t 0 := by nlinarith only [h01, h02] _ = M * t 0 := by rw [hs3] exact mul_left_cancel₀ hM hscale have hs1 : s 1 = t 1 := by have hmul : t 0 * t 1 = t 0 * s 1 := by calc t 0 * t 1 = s 0 * t 1 := by rw [hs0] _ = s 1 * t 0 := h01eq _ = t 0 * s 1 := by ring exact (mul_left_cancel₀ ht0 hmul).symm have hs2 : s 2 = t 2 := by have hmul : t 0 * t 2 = t 0 * s 2 := by calc t 0 * t 2 = s 0 * t 2 := by rw [hs0] _ = s 2 * t 0 := h02eq _ = t 0 * s 2 := by ring exact (mul_left_cancel₀ ht0 hmul).symm funext i fin_cases i <;> assumption exact hne hst have hsqrt_lt : sqrt (R ^ 2) < sqrt (P * Q) := Real.sqrt_lt_sqrt (sq_nonneg R) hlt have hR_le_sqrt : R ≤ sqrt (R ^ 2) := by rw [Real.sqrt_sq_eq_abs] exact le_abs_self R calc (∑ i, β i * (s i * t i)) = R := by rfl _ ≤ sqrt (R ^ 2) := hR_le_sqrt _ < sqrt (P * Q) := hsqrt_lt _ = sqrt P * sqrt Q := by rw [Real.sqrt_mul hP_nonneg] _ = sqrt (∑ i, β i * s i ^ 2) * sqrt (∑ i, β i * t i ^ 2) := by rfl

lemma exists_admissible (α β : Fin 3 → ℝ) (kappa : ℝ) (hβ : ∀ i, 0 < β i) (hk : 0 < kappa) : ∃ (S : Finset (Fin 3)) (lam : ℝ), IsAdmissibleSupport α β kappa S lam := by classical obtain ⟨kmin, hmin⟩ := (Finite.exists_min α : ∃ k : Fin 3, ∀ i, α k ≤ α i) obtain ⟨kmax, hmax⟩ := (Finite.exists_max α : ∃ k : Fin 3, ∀ i, α i ≤ α k) let lo : ℝ := α kmin let hi : ℝ := α kmax + kappa * sqrt (β kmax) have hlo_zero : kktThreshold α β lo = 0 := by exact kktThreshold_eq_zero_of_le α β lo (by intro i; exact hmin i) have hhi_summand : (max (hi - α kmax) 0) ^ 2 / β kmax = kappa ^ 2 := by have hβpos : 0 < β kmax := hβ kmax have hβnonneg : 0 ≤ β kmax := le_of_lt hβpos have hsqrt_sq : sqrt (β kmax) ^ 2 = β kmax := Real.sq_sqrt hβnonneg have hdiff : hi - α kmax = kappa * sqrt (β kmax) := by simp [hi] have hdiff_nonneg : 0 ≤ hi - α kmax := by rw [hdiff] exact mul_nonneg (le_of_lt hk) (Real.sqrt_nonneg _) rw [max_eq_left hdiff_nonneg, hdiff] field_simp [ne_of_gt hβpos] rw [hsqrt_sq] have hhi_ge : kappa ^ 2 ≤ kktThreshold α β hi := by calc kappa ^ 2 = (max (hi - α kmax) 0) ^ 2 / β kmax := by exact hhi_summand.symm _ ≤ kktThreshold α β hi := by unfold kktThreshold exact Finset.single_le_sum (s := univ) (f := fun i => (max (hi - α i) 0) ^ 2 / β i) (fun i _ => div_nonneg (sq_nonneg _) (le_of_lt (hβ i))) (Finset.mem_univ kmax) have hlohi : lo ≤ hi := by have hmul_nonneg : 0 ≤ kappa * sqrt (β kmax) := mul_nonneg (le_of_lt hk) (Real.sqrt_nonneg _) have hle_max : α kmin ≤ α kmax := hmin kmax dsimp [lo, hi] linarith have htarget : kappa ^ 2 ∈ Icc (kktThreshold α β lo) (kktThreshold α β hi) := by constructor · rw [hlo_zero] exact sq_nonneg kappa · exact hhi_ge have hcontOn : ContinuousOn (kktThreshold α β) (Icc lo hi) := (continuous_kktThreshold α β).continuousOn obtain ⟨lam, -, hlam⟩ := intermediate_value_Icc hlohi hcontOn htarget let S : Finset (Fin 3) := Finset.univ.filter (fun i : Fin 3 => α i < lam) refine ⟨S, lam, ?_⟩ have hsum_eq : (∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2 := by calc (∑ i ∈ S, (lam - α i) ^ 2 / β i) = kktThreshold α β lam := by simpa [S] using support_sum_eq_kktThreshold α β lam _ = kappa ^ 2 := hlam refine ⟨?_, hsum_eq, ?_, ?_⟩ · by_contra hnonempty have hSempty : S = ∅ := by exact Finset.not_nonempty_iff_eq_empty.mp hnonempty have hzero : (∑ i ∈ S, (lam - α i) ^ 2 / β i) = 0 := by simp [hSempty] have hsquare_zero : kappa ^ 2 = 0 := by simpa [hzero] using hsum_eq.symm exact (ne_of_gt (sq_pos_of_pos hk)) hsquare_zero · intro i hi simpa [S] using hi · intro j hj have hnot : ¬ α j < lam := by intro hlt exact hj (by simp [S, hlt]) exact not_lt.mp hnot

lemma kappa_zero_face (M : ℝ) (α : Fin 3 → ℝ) (t : Fin 3 → ℝ) : (InSimplex M t ∧ ∀ s : Fin 3 → ℝ, InSimplex M s → (∑ i, α i * t i) ≤ ∑ i, α i * s i) ↔ t ∈ exposedMinFace M α := by classical obtain ⟨k, hk⟩ := (Finite.exists_min α : ∃ k, ∀ i, α k ≤ α i) constructor · rintro ⟨htS, hmin⟩ refine ⟨htS, ?_⟩ intro i hti j let v : Fin 3 → ℝ := fun i => if i = k then M else 0 have hM_nonneg : 0 ≤ M := by rw [← htS.2] exact sum_nonneg (fun i _ => htS.1 i) have hv : InSimplex M v := by constructor · intro i dsimp [v] by_cases hi : i = k · simp [hi, hM_nonneg] · simp [hi] · dsimp [v] fin_cases k <;> simp [Fin.sum_univ_three] have hv_sum : ∑ i, α i * v i = α k * M := by dsimp [v] fin_cases k <;> simp have ht_le : ∑ i, α i * t i ≤ α k * M := by have h := hmin v hv simpa [hv_sum] using h have hsum_diff_le : ∑ i, (α i - α k) * t i ≤ 0 := by have hconst : ∑ i, α k * t i = α k * M := by rw [← Finset.mul_sum, htS.2] calc ∑ i, (α i - α k) * t i = ∑ i, α i * t i - ∑ i, α k * t i := by simp_rw [sub_mul] rw [Finset.sum_sub_distrib] _ = ∑ i, α i * t i - α k * M := by rw [hconst] _ ≤ 0 := by linarith have hterm_nonneg (i : Fin 3) : 0 ≤ (α i - α k) * t i := by exact mul_nonneg (sub_nonneg.mpr (hk i)) (htS.1 i) have hsum_three : (α 0 - α k) * t 0 + (α 1 - α k) * t 1 + (α 2 - α k) * t 2 ≤ 0 := by simpa [Fin.sum_univ_three] using hsum_diff_le have hterm0 : (α 0 - α k) * t 0 = 0 := by have h0 := hterm_nonneg 0 have h1 := hterm_nonneg 1 have h2 := hterm_nonneg 2 nlinarith have hterm1 : (α 1 - α k) * t 1 = 0 := by have h0 := hterm_nonneg 0 have h1 := hterm_nonneg 1 have h2 := hterm_nonneg 2 nlinarith have hterm2 : (α 2 - α k) * t 2 = 0 := by have h0 := hterm_nonneg 0 have h1 := hterm_nonneg 1 have h2 := hterm_nonneg 2 nlinarith have hterm_zero (i : Fin 3) : (α i - α k) * t i = 0 := by fin_cases i <;> simp [hterm0, hterm1, hterm2] have hai : α i = α k := by exact sub_eq_zero.mp ((mul_eq_zero.mp (hterm_zero i)).resolve_right hti) rw [hai] exact hk j · intro htFace rcases htFace with ⟨htS, hface⟩ refine ⟨htS, ?_⟩ intro s hsS have ht_term_eq (i : Fin 3) : α i * t i = α k * t i := by by_cases hti : t i = 0 · simp [hti] · have hik : α i ≤ α k := hface i hti k have hki : α k ≤ α i := hk i rw [le_antisymm hik hki] have ht_sum : ∑ i, α i * t i = α k * M := by calc ∑ i, α i * t i = ∑ i, α k * t i := by exact Finset.sum_congr rfl (by intro i _; exact ht_term_eq i) _ = α k * M := by rw [← Finset.mul_sum, htS.2] have hs_term_le (i : Fin 3) : α k * s i ≤ α i * s i := by have hnonneg : 0 ≤ (α i - α k) * s i := mul_nonneg (sub_nonneg.mpr (hk i)) (hsS.1 i) nlinarith have hs_sum : α k * M ≤ ∑ i, α i * s i := by calc α k * M = ∑ i, α k * s i := by rw [← hsS.2, Finset.mul_sum] _ ≤ ∑ i, α i * s i := by exact Finset.sum_le_sum (by intro i _; exact hs_term_le i) linarith

lemma activeSetPoint_value (hM : 0 ≤ M) (hβ : ∀ i ∈ S, 0 < β i) (hk : 0 < kappa) (hS : S.Nonempty) (hactive : ∀ i ∈ S, α i < lam) (hsq : (∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2) : wsObj α β kappa (activeSetPoint M α β S lam) = M * lam := by let D := ∑ h ∈ S, (lam - α h) / β h have hDpos : 0 < D := activeSet_denom_pos α β S lam hβ hS hactive have hD : D ≠ 0 := ne_of_gt hDpos have hnorm : (∑ i, β i * activeSetPoint M α β S lam i ^ 2) = (M * kappa) ^ 2 / D ^ 2 := by simpa [D] using activeSetPoint_normSq M α β kappa S lam hβ hS hactive hsq have hsqrt : sqrt (∑ i, β i * activeSetPoint M α β S lam i ^ 2) = M * kappa / D := by rw [hnorm] rw [div_eq_mul_inv] rw [show (M * kappa) ^ 2 * (D ^ 2)⁻¹ = (M * kappa / D) ^ 2 by field_simp [hD]] exact Real.sqrt_sq (div_nonneg (mul_nonneg hM (le_of_lt hk)) hDpos.le) have hlin : (∑ i, α i * activeSetPoint M α β S lam i) = M * lam - M * kappa ^ 2 / D := by have hcore : (∑ i ∈ S, α i * ((lam - α i) / β i)) = lam * D - kappa ^ 2 := by calc (∑ i ∈ S, α i * ((lam - α i) / β i)) = ∑ i ∈ S, (lam * ((lam - α i) / β i) - (lam - α i) ^ 2 / β i) := by apply Finset.sum_congr rfl intro i hi have hb : β i ≠ 0 := ne_of_gt (hβ i hi) field_simp [hb] ring _ = lam * D - kappa ^ 2 := by rw [Finset.sum_sub_distrib, ← Finset.mul_sum] rw [show (∑ x ∈ S, (lam - α x) / β x) = D by rfl, hsq] calc (∑ i, α i * activeSetPoint M α β S lam i) = ∑ i ∈ S, α i * (M * ((lam - α i) / β i) / D) := by simp [activeSetPoint, D] _ = M / D * (∑ i ∈ S, α i * ((lam - α i) / β i)) := by rw [Finset.mul_sum] simp [mul_assoc, mul_comm, mul_left_comm, div_eq_mul_inv] _ = M * lam - M * kappa ^ 2 / D := by rw [hcore] field_simp [hD] calc wsObj α β kappa (activeSetPoint M α β S lam) = (∑ i, α i * activeSetPoint M α β S lam i) + kappa * sqrt (∑ i, β i * activeSetPoint M α β S lam i ^ 2) := rfl _ = M * lam := by rw [hlin, hsqrt] field_simp [hD] ring

lemma activeSetPoint_strict_min (hM : 0 < M) (hβ : ∀ i, 0 < β i) (hk : 0 < kappa) (hadm : IsAdmissibleSupport α β kappa S lam) : ∀ s : Fin 3 → ℝ, InSimplex M s → s ≠ activeSetPoint M α β S lam → wsObj α β kappa (activeSetPoint M α β S lam) < wsObj α β kappa s := by intro s hs hne let t := activeSetPoint M α β S lam let D := ∑ h ∈ S, (lam - α h) / β h let Q := ∑ i, β i * t i ^ 2 let N := sqrt Q let Ns := sqrt (∑ i, β i * s i ^ 2) let R := ∑ i, β i * (t i * s i) have htmem : InSimplex M t := by simpa [t] using activeSetPoint_mem M α β S lam hM.le (fun i _ => hβ i) hadm.1 hadm.2.2.1 have ht_sum : ∑ i, t i = M := htmem.2 have hDpos : 0 < D := activeSet_denom_pos α β S lam (fun i _ => hβ i) hadm.1 hadm.2.2.1 have hD : D ≠ 0 := ne_of_gt hDpos have hQnorm : Q = (M * kappa) ^ 2 / D ^ 2 := by simpa [Q, t, D] using activeSetPoint_normSq M α β kappa S lam (fun i _ => hβ i) hadm.1 hadm.2.2.1 hadm.2.1 have hQnonneg : 0 ≤ Q := by rw [hQnorm] exact div_nonneg (sq_nonneg (M * kappa)) (sq_nonneg D) have hQeq : Q = N ^ 2 := by rw [Real.sq_sqrt hQnonneg] have hNval : N = M * kappa / D := by dsimp [N] rw [hQnorm] rw [div_eq_mul_inv] rw [show (M * kappa) ^ 2 * (D ^ 2)⁻¹ = (M * kappa / D) ^ 2 by field_simp [hD]] exact Real.sqrt_sq (le_of_lt (div_pos (mul_pos hM hk) hDpos)) have hNpos : 0 < N := by rw [hNval] exact div_pos (mul_pos hM hk) hDpos have hcs : R < N * Ns := by simpa [R, N, Ns, t] using weighted_cs_simplex_strict M hM.ne' β t s hβ ht_sum hs.2 (Ne.symm hne) have hRdiff : (∑ i, β i * (t i * (s i - t i))) = R - Q := by dsimp [R, Q] rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro i hi ring have hnorm_strict : (kappa / N) * (∑ i, β i * (t i * (s i - t i))) < kappa * (Ns - N) := by rw [hRdiff, hQeq] field_simp [ne_of_gt hNpos] nlinarith [mul_pos hk hNpos] have hstationary : (kappa / N) * (∑ i, β i * (t i * (s i - t i))) = ∑ i ∈ S, (lam - α i) * (s i - t i) := by subst t calc (kappa / N) * (∑ i, β i * (activeSetPoint M α β S lam i * (s i - activeSetPoint M α β S lam i))) = ∑ i ∈ S, (kappa / N) * (β i * (M * ((lam - α i) / β i) / D * (s i - activeSetPoint M α β S lam i))) := by rw [Finset.mul_sum] simp [activeSetPoint, D] _ = ∑ i ∈ S, (lam - α i) * (s i - activeSetPoint M α β S lam i) := by apply Finset.sum_congr rfl intro i hi simp [activeSetPoint, hi, D] rw [hNval] rw [show (∑ h ∈ S, (lam - α h) / β h) = D by rfl] field_simp [ne_of_gt hM, ne_of_gt hk, hD, ne_of_gt (hβ i)] have hgap_formula : wsObj α β kappa s - wsObj α β kappa t = (∑ i, α i * (s i - t i)) + kappa * (Ns - N) := by subst t dsimp [wsObj, Ns, N, Q] have hsumdiff : (∑ i, α i * (s i - activeSetPoint M α β S lam i)) = (∑ i, α i * s i) - ∑ i, α i * activeSetPoint M α β S lam i := by rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro i hi ring rw [hsumdiff] ring have hremainder_eq : (∑ i, α i * (s i - t i)) + (∑ i ∈ S, (lam - α i) * (s i - t i)) = (∑ i, (if i ∈ S then lam else α i) * s i) - lam * M := by subst t have hcoeff : (∑ i, α i * (s i - activeSetPoint M α β S lam i)) + (∑ i ∈ S, (lam - α i) * (s i - activeSetPoint M α β S lam i)) = ∑ i, (if i ∈ S then lam else α i) * (s i - activeSetPoint M α β S lam i) := by rw [show (∑ i ∈ S, (lam - α i) * (s i - activeSetPoint M α β S lam i)) = ∑ i, if i ∈ S then (lam - α i) * (s i - activeSetPoint M α β S lam i) else 0 by simp] rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i hi by_cases his : i ∈ S · simp [his] ring · simp [his] have hmass : (∑ i, (if i ∈ S then lam else α i) * activeSetPoint M α β S lam i) = lam * M := by calc (∑ i, (if i ∈ S then lam else α i) * activeSetPoint M α β S lam i) = ∑ i, lam * activeSetPoint M α β S lam i := by apply Finset.sum_congr rfl intro i hi by_cases his : i ∈ S · simp [his] · simp [activeSetPoint, his] _ = lam * M := by rw [← Finset.mul_sum, ht_sum] rw [hcoeff] rw [show (∑ i, (if i ∈ S then lam else α i) * (s i - activeSetPoint M α β S lam i)) = (∑ i, (if i ∈ S then lam else α i) * s i) - ∑ i, (if i ∈ S then lam else α i) * activeSetPoint M α β S lam i by rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro i hi ring] rw [hmass] have hremainder_nonneg : 0 ≤ (∑ i, α i * (s i - t i)) + (∑ i ∈ S, (lam - α i) * (s i - t i)) := by rw [hremainder_eq] have hpoint : ∀ i, lam * s i ≤ (if i ∈ S then lam else α i) * s i := by intro i by_cases hi : i ∈ S · simp [hi] · exact mul_le_mul_of_nonneg_right (by simpa [hi] using hadm.2.2.2 i hi) (hs.1 i) have hsum : (∑ i, lam * s i) ≤ ∑ i, (if i ∈ S then lam else α i) * s i := by exact Finset.sum_le_sum (fun i hi => hpoint i) rw [← Finset.mul_sum, hs.2] at hsum linarith have hgap_pos : 0 < wsObj α β kappa s - wsObj α β kappa t := by have hstrict : (∑ i, α i * (s i - t i)) + (∑ i ∈ S, (lam - α i) * (s i - t i)) < wsObj α β kappa s - wsObj α β kappa t := by rw [hgap_formula] rw [hstationary] at hnorm_strict linarith linarith have ht_value : wsObj α β kappa t = M * lam := by simpa [t] using activeSetPoint_value M α β kappa S lam hM.le (fun i _ => hβ i) hk hadm.1 hadm.2.2.1 hadm.2.1 linarith