PO.ID.Partial.LP

theorem farkas {b : F} : b ∈ ProperCone.map P.A P.K ↔ ∀ y : F, (adjoint P.A) y ∈ innerDual (P.K : Set E) → 0 ≤ ⟪b, y⟫ := ProperCone.relative_hyperplane_separation

theorem strong_duality_primal_attained (hP : {x | P.PrimalFeasible x}.Nonempty) (hbdd : BddBelow ((fun x => ⟪P.c, x⟫) '' {x | P.PrimalFeasible x})) (hCQ : IsClosed P.augmentedImage) : ∃ x, P.PrimalFeasible x ∧ ⟪P.c, x⟫ = P.primalValue := by have hSeq : (fun x => ⟪P.c, x⟫) '' {x | P.PrimalFeasible x} = (fun r : ℝ => (P.b, r)) ⁻¹' P.augmentedImage := by ext r constructor · rintro ⟨x, hx, rfl⟩ exact ⟨x, hx.2, by simp only [hx.1]⟩ · rintro ⟨x, hxK, hxeq⟩ exact ⟨x, ⟨(Prod.ext_iff.mp hxeq).1, hxK⟩, (Prod.ext_iff.mp hxeq).2⟩ have hScl : IsClosed ((fun x => ⟪P.c, x⟫) '' {x | P.PrimalFeasible x}) := by rw [hSeq]; exact hCQ.preimage (by fun_prop) have hmem := hScl.csInf_mem (hP.image _) hbdd obtain ⟨x, hx, hxval⟩ := hmem exact ⟨x, hx, hxval⟩

theorem strong_duality_zero_gap (hP : {x | P.PrimalFeasible x}.Nonempty) (hbdd : BddBelow ((fun x => ⟪P.c, x⟫) '' {x | P.PrimalFeasible x})) (hCQ : IsClosed P.augmentedImage) : P.primalValue = P.dualValue := by -- The augmented operator `à x = (A x, ⟪c, x⟫)`. set à : E →L[ℝ] (F × ℝ) := (P.A).prod (innerSL ℝ P.c) with hÃdef have hÃapp : ∀ x : E, à x = (P.A x, ⟪P.c, x⟫) := fun x => rfl -- The underlying `PointedCone.map` image set is exactly the augmented image. have hpcimg : ((PointedCone.map (à : E →ₗ[ℝ] (F × ℝ)) (P.K : PointedCone ℝ E)) : Set (F × ℝ)) = P.augmentedImage := by rw [PointedCone.coe_map] ext z simp only [augmentedImage, Set.mem_image] constructor · rintro ⟨x, hx, rfl⟩; exact ⟨x, hx, (hÃapp x).symm⟩ · rintro ⟨x, hx, rfl⟩; exact ⟨x, hx, hÃapp x⟩ -- `p* := primalValue` is a finite lower bound for the feasible objective values. set S : Set ℝ := (fun x => ⟪P.c, x⟫) '' {x | P.PrimalFeasible x} with hSdef have hSne : S.Nonempty := hP.image _ have hlb : ∀ x : E, P.PrimalFeasible x → P.primalValue ≤ ⟪P.c, x⟫ := by intro x hx exact csInf_le hbdd ⟨x, hx, rfl⟩ -- (A) dualValue ≤ primalValue: every dual-feasible value is ≤ every feasible objective, -- hence ≤ the infimum p*. have hA : ∀ y : F, P.DualFeasible y → ⟪P.b, y⟫ ≤ P.primalValue := by intro y hy refine le_csInf hSne ?_ rintro _ ⟨x, hx, rfl⟩ exact P.weak_duality hx hy -- (B) primalValue ≤ dualValue, via separation. -- First: for every ε > 0 there is a dual-feasible ȳ with ⟪b, ȳ⟫ > p* - ε. have hB : ∀ ε : ℝ, 0 < ε → ∃ y : F, P.DualFeasible y ∧ P.primalValue - ε < ⟪P.b, y⟫ := by intro ε hε -- The point (b, p* - ε) is not in the map cone. have hnotmem : (P.b, P.primalValue - ε) ∉ map à P.K := by intro hmem have hcl : (P.b, P.primalValue - ε) ∈ (PointedCone.map (à : E →ₗ[ℝ] (F × ℝ)) (P.K : PointedCone ℝ E)).closure := ProperCone.mem_map.mp hmem rw [PointedCone.mem_closure] at hcl -- closure of the augmented image is itself, since it is closed. have : (P.b, P.primalValue - ε) ∈ P.augmentedImage := by have hset : closure ((PointedCone.map (à : E →ₗ[ℝ] (F × ℝ)) (P.K : PointedCone ℝ E)) : Set (F × ℝ)) = P.augmentedImage := by rw [hpcimg]; exact hCQ.closure_eq rwa [hset] at hcl obtain ⟨x, hxK, hxeq⟩ := this have h1 : P.A x = P.b := (Prod.ext_iff.mp hxeq).1 have h2 : ⟪P.c, x⟫ = P.primalValue - ε := (Prod.ext_iff.mp hxeq).2 have hfeas : P.PrimalFeasible x := ⟨h1, hxK⟩ have := hlb x hfeas rw [h2] at this linarith -- Separate. obtain ⟨g, hgpos, hgneg⟩ := ProperCone.hyperplane_separation_point (map à P.K) hnotmem -- Decompose g into the F-part (Riesz) and the ℝ-part s := g(0,1). set s : ℝ := g (0, 1) with hsdef set φ : F →L[ℝ] ℝ := g.comp ((ContinuousLinearMap.inl ℝ F ℝ)) with hφdef -- φ v = g (v, 0); Riesz representative y₀. set y₀ : F := (InnerProductSpace.toDual ℝ F).symm φ with hy₀def have hφapp : ∀ v : F, φ v = ⟪y₀, v⟫ := by intro v rw [hy₀def] rw [InnerProductSpace.toDual_symm_apply] -- g decomposes: g (v, t) = ⟪y₀, v⟫ + t * s. have hgdecomp : ∀ (v : F) (t : ℝ), g (v, t) = ⟪y₀, v⟫ + s * t := by intro v t have hvt : ((v, t) : F × ℝ) = (v, 0) + t • (0, 1) := by simp rw [hvt, map_add, map_smul] have hv : g (v, 0) = ⟪y₀, v⟫ := by rw [← hφapp v]; rfl rw [hv] simp only [hsdef, smul_eq_mul] ring -- (i): ∀ x ∈ K, 0 ≤ ⟪y₀, A x⟫ + s * ⟪c, x⟫. have hi : ∀ x : E, x ∈ P.K → 0 ≤ ⟪y₀, P.A x⟫ + s * ⟪P.c, x⟫ := by intro x hx have hxmem : à x ∈ map à P.K := by apply ProperCone.mem_map.mpr rw [PointedCone.mem_closure] apply subset_closure -- à x ∈ (PointedCone.map ↑à ↑P.K : Set _) = augmentedImage rw [hpcimg] exact ⟨x, hx, rfl⟩ have := hgpos (à x) hxmem rw [hÃapp x, hgdecomp] at this exact this -- (ii): ⟪y₀, b⟫ + (p* - ε) * s < 0. have hii : ⟪y₀, P.b⟫ + s * (P.primalValue - ε) < 0 := by have := hgneg rw [hgdecomp] at this exact this -- Get a feasible point x₀. obtain ⟨x₀, hx₀⟩ := hP have hx₀K : x₀ ∈ P.K := hx₀.2 have hx₀A : P.A x₀ = P.b := hx₀.1 have hx₀val : P.primalValue ≤ ⟪P.c, x₀⟫ := hlb x₀ hx₀ -- Case on s. rcases lt_trichotomy s 0 with hs | hs | hs · -- s < 0 impossible. exfalso have h1 := hi x₀ hx₀K rw [hx₀A] at h1 -- 0 ≤ ⟪y₀, b⟫ + s * ⟪c, x₀⟫ -- since s < 0 and ⟪c,x₀⟫ ≥ p*: s * ⟪c,x₀⟫ ≤ s * p* have hmul : s * ⟪P.c, x₀⟫ ≤ s * P.primalValue := by apply mul_le_mul_of_nonpos_left hx₀val (le_of_lt hs) -- (ii): ⟪y₀,b⟫ + (p*-ε)*s < 0, i.e. ⟪y₀,b⟫ + s*p* - s*ε < 0 nlinarith [hii, h1, hmul, hε, hs] · -- s = 0 impossible. exfalso have h1 := hi x₀ hx₀K rw [hx₀A, hs] at h1 simp only [zero_mul, add_zero] at h1 -- h1 : 0 ≤ ⟪y₀, b⟫ have h2 := hii rw [hs] at h2 simp only [zero_mul, add_zero] at h2 -- h2 : ⟪y₀, b⟫ < 0 linarith · -- s > 0: ȳ := -(1/s) • y₀ is dual feasible with ⟪b, ȳ⟫ > p* - ε. refine ⟨-(1/s) • y₀, ?_, ?_⟩ · -- dual feasibility rw [DualFeasible, ProperCone.mem_innerDual] intro x hx have hred : ⟪x, P.c - (adjoint P.A) (-(1/s) • y₀)⟫ = (1/s) * (⟪y₀, P.A x⟫ + s * ⟪P.c, x⟫) := by rw [inner_sub_right] rw [map_smul, inner_smul_right] rw [ContinuousLinearMap.adjoint_inner_right] rw [real_inner_comm x P.c, real_inner_comm (P.A x) y₀] field_simp ring rw [hred] have hpos : (0 : ℝ) ≤ 1/s := le_of_lt (by positivity) exact mul_nonneg hpos (hi x hx) · -- value bound have hval : ⟪P.b, -(1/s) • y₀⟫ = -(1/s) * ⟪y₀, P.b⟫ := by rw [inner_smul_right, real_inner_comm P.b y₀] rw [hval] -- from (ii): ⟪y₀, b⟫ + s*(p*-ε) < 0; multiply by 1/s > 0. have hsinv : (0:ℝ) < 1 / s := by positivity have key : (1/s) * (⟪y₀, P.b⟫ + s * (P.primalValue - ε)) < (1/s) * 0 := mul_lt_mul_of_pos_left hii hsinv have hexp : (1/s) * (⟪y₀, P.b⟫ + s * (P.primalValue - ε)) = (1/s) * ⟪y₀, P.b⟫ + (P.primalValue - ε) := by field_simp rw [hexp, mul_zero] at key linarith [key] -- Assemble: dualValue ≥ p* and dualValue ≤ p*. have hDne : {y | P.DualFeasible y}.Nonempty := by obtain ⟨y, hy, _⟩ := hB 1 (by norm_num) exact ⟨y, hy⟩ -- dualValue ≤ primalValue have hle : P.dualValue ≤ P.primalValue := by rw [dualValue] refine csSup_le (hDne.image _) ?_ rintro _ ⟨y, hy, rfl⟩ exact hA y hy -- primalValue ≤ dualValue have hge : P.primalValue ≤ P.dualValue := by refine le_of_forall_pos_lt_add ?_ intro ε hε obtain ⟨y, hy, hyval⟩ := hB ε hε have hbdd' : BddAbove ((fun y => ⟪P.b, y⟫) '' {y | P.DualFeasible y}) := by refine ⟨P.primalValue, ?_⟩ rintro _ ⟨z, hz, rfl⟩ exact hA z hz have : ⟪P.b, y⟫ ≤ P.dualValue := le_csSup hbdd' ⟨y, hy, rfl⟩ linarith linarith