Mathlib.Optimization.Quadratic­Saddle

theorem value_eq_extended_maxMin (P : Polytope ι κ) (Q : Quadratics Θ ι) (θ : Θ) (α : EuclideanSpace ℝ ι) (t : ℝ) (h : IsSaddle P Q θ α t) : (value P Q θ : EReal) = ⨆ (β : {β : EuclideanSpace ℝ ι // β ∈ P.weights}), ⨅ (u : ℝ), (Q.objective θ β.1 u : EReal) := by rw [value_eq_of_isSaddle P Q θ α t h] apply le_antisymm · calc (Q.objective θ α t : EReal) ≤ ⨅ (u : ℝ), (Q.objective θ α u : EReal) := le_iInf fun u => by exact_mod_cast h.2.1 u _ ≤ ⨆ (β : {β : EuclideanSpace ℝ ι // β ∈ P.weights}), ⨅ (u : ℝ), (Q.objective θ β.1 u : EReal) := le_iSup (fun β : {β : EuclideanSpace ℝ ι // β ∈ P.weights} => ⨅ (u : ℝ), (Q.objective θ β.1 u : EReal)) ⟨α, h.1⟩ · refine iSup_le fun β => ?_ calc (⨅ (u : ℝ), (Q.objective θ β.1 u : EReal)) ≤ (Q.objective θ β.1 t : EReal) := iInf_le _ t _ ≤ (Q.objective θ α t : EReal) := by exact_mod_cast h.2.2 β.1 β.2

theorem continuousAt_quadratic_value (P : Polytope ι κ) (Q : Quadratics Θ ι) (K : Set ℝ) (hK : IsCompact K) (hKne : K.Nonempty) (θ₀ : Θ) (U : Set Θ) (hUopen : IsOpen U) (hθU : θ₀ ∈ U) (hobj : ContinuousOn (fun x : (Θ × ℝ) × EuclideanSpace ℝ ι => Q.objective x.1.1 x.2 x.1.2) {x | x.1.1 ∈ U}) (hatt : ∀ᶠ θ in nhds θ₀, ∃ α : EuclideanSpace ℝ ι, ∃ t ∈ K, IsSaddle P Q θ α t) : ContinuousAt (value P Q) θ₀ := by have hatt' : ∀ᶠ θ in nhds θ₀, ∃ t ∈ K, ∀ u : ℝ, envelope P.weights Q.objective θ t ≤ envelope P.weights Q.objective θ u := by filter_upwards [hatt] with θ ⟨α, t, ht, hs⟩ exact ⟨t, ht, (quadratic_value_eq_envelope_min_of_isSaddle P Q θ α t hs).2⟩ have hcont := continuousAt_value_of_continuousOn P.weights P.compact P.nonempty Q.objective K hK hKne θ₀ U hUopen hθU hobj hatt' apply hcont.congr filter_upwards [hatt] with θ ⟨α, t, ht, hs⟩ exact (quadratic_value_eq_envelope_min_of_isSaddle P Q θ α t hs).1.symm

theorem measurable_value_on (P : Polytope ι κ) (Q : Quadratics Θ ι) (D : Set Θ) (hAttains : ∀ θ ∈ D, ∃ α t, IsSaddle P Q θ α t) : Measurable (fun θ : D => value P Q θ.1) := by classical letI : Nonempty P.weights := Set.nonempty_coe_sort.mpr P.nonempty let d : ℕ → P.weights := TopologicalSpace.denseSeq P.weights have hd : Dense (range d) := by simpa only [DenseRange, d] using TopologicalSpace.denseRange_denseSeq P.weights let M : Θ → ℝ → ℝ := fun θ t => sSup ((fun β : EuclideanSpace ℝ ι => Q.objective θ β t) '' P.weights) have hM : Measurable (fun x : Θ × ℝ => M x.1 x.2) := by have hn : Measurable (fun x : Θ × ℝ => ⨆ n : ℕ, Q.objective x.1 (d n).1 x.2) := by apply Measurable.iSup intro n exact Q.measurable_objective.comp (measurable_fst.prodMk (measurable_const.prodMk measurable_snd)) convert hn using 1 ext x change sSup ((fun β : EuclideanSpace ℝ ι => Q.objective x.1 β x.2) '' P.weights) = ⨆ n : ℕ, Q.objective x.1 (d n).1 x.2 rw [sSup_image'] have hc : Continuous (fun β : P.weights => Q.objective x.1 β.1 x.2) := by unfold Quadratics.objective fun_prop rw [← hd.ciSup' hc] have he : Surjective (fun n : ℕ => (⟨d n, Set.mem_range_self n⟩ : range d)) := by rintro ⟨z, n, rfl⟩ exact ⟨n, rfl⟩ exact (he.iSup_comp (fun s : range d => Q.objective x.1 s.1.1 x.2)).symm have hMc : ∀ θ : Θ, Continuous (M θ) := by intro θ apply P.compact.continuous_sSup change Continuous (fun p : ℝ × EuclideanSpace ℝ ι => Q.objective θ p.2 p.1) unfold Quadratics.objective fun_prop have hEq : ∀ θ : D, (⨅ q : ℚ, M θ.1 q) = value P Q θ.1 := by intro θ obtain ⟨α, t, hs⟩ := hAttains θ.1 θ.2 have hc : Continuous (fun β : EuclideanSpace ℝ ι => Q.objective θ.1 β t) := by unfold Quadratics.objective fun_prop have hbdd : BddAbove ((fun β : EuclideanSpace ℝ ι => Q.objective θ.1 β t) '' P.weights) := P.compact.bddAbove_image hc.continuousOn have hMt : M θ.1 t = Q.objective θ.1 α t := by apply le_antisymm · apply csSup_le (P.nonempty.image _) rintro y ⟨β, hβ, rfl⟩ exact hs.2.2 β hβ · exact le_csSup hbdd ⟨α, hs.1, rfl⟩ have hmin : IsMinOn (M θ.1) univ t := by intro u hu have hcu : Continuous (fun β : EuclideanSpace ℝ ι => Q.objective θ.1 β u) := by unfold Quadratics.objective fun_prop have hbu : BddAbove ((fun β : EuclideanSpace ℝ ι => Q.objective θ.1 β u) '' P.weights) := P.compact.bddAbove_image hcu.continuousOn rw [hMt] exact (hs.2.1 u).trans (le_csSup hbu ⟨α, hs.1, rfl⟩) have hr : Dense (range (fun q : ℚ => (q : ℝ))) := Rat.denseRange_cast have hi := hr.ciInf' (hMc θ.1) have he : Surjective (fun q : ℚ => (⟨(q : ℝ), Set.mem_range_self q⟩ : range (fun q : ℚ => (q : ℝ)))) := by rintro ⟨z, q, rfl⟩ exact ⟨q, rfl⟩ rw [← he.iInf_comp (fun s : range (fun q : ℚ => (q : ℝ)) => M θ.1 s.1)] at hi change (⨅ q : ℚ, M θ.1 (q : ℝ)) = ⨅ u : ℝ, M θ.1 u at hi rw [hi] have hlower : BddBelow (range (M θ.1)) := by refine ⟨M θ.1 t, ?_⟩ rintro y ⟨u, rfl⟩ exact hmin (Set.mem_univ u) have hminEq : (⨅ u : ℝ, M θ.1 u) = M θ.1 t := le_antisymm (ciInf_le hlower t) (le_ciInf fun u => hmin (Set.mem_univ u)) rw [hminEq, hMt, value_eq_of_isSaddle P Q θ.1 α t hs] have hresult : Measurable (fun θ : D => ⨅ q : ℚ, M θ.1 q) := by apply Measurable.iInf intro q have hp : Measurable (fun θ : D => ((θ.1, (q : ℝ)) : Θ × ℝ)) := measurable_subtype_coe.prodMk measurable_const simpa only [Function.comp_def] using hM.comp hp convert hresult using 1 ext θ exact (hEq θ).symm

theorem exists_measurable_saddle_with_fallback (P : Polytope ι κ) (Q : Quadratics Θ ι) (D : Set Θ) (hD : MeasurableSet D) (hAttains : ∀ θ ∈ D, ∃ α t, IsSaddle P Q θ α t) (fallback : EuclideanSpace ℝ ι × ℝ × ℝ) : ∃ policy : Θ → EuclideanSpace ℝ ι × ℝ × ℝ, Measurable policy ∧ (∀ θ ∉ D, policy θ = fallback) ∧ (∀ θ ∈ D, IsSaddle P Q θ (policy θ).1 (policy θ).2.1 ∧ (policy θ).2.2 = Q.objective θ (policy θ).1 (policy θ).2.1 ∧ (policy θ).2.2 = value P Q θ) := by classical obtain ⟨α, t, hα, ht, hs⟩ := exists_measurable_saddle_on P Q D hD hAttains let policy : Θ → EuclideanSpace ℝ ι × ℝ × ℝ := fun θ => if hθ : θ ∈ D then (α ⟨θ, hθ⟩, t ⟨θ, hθ⟩, value P Q θ) else fallback have hv : Measurable (fun θ : D => value P Q θ.1) := measurable_value_on P Q D hAttains have hp : Measurable policy := by change Measurable (fun θ : Θ => if hθ : θ ∈ D then (α ⟨θ, hθ⟩, t ⟨θ, hθ⟩, value P Q θ) else fallback) exact Measurable.dite (hα.prodMk (ht.prodMk hv)) measurable_const hD refine ⟨policy, hp, ?_, ?_⟩ · intro θ hθ simp [policy, hθ] · intro θ hθ have h := hs (⟨θ, hθ⟩ : D) have heq := value_eq_of_isSaddle P Q θ (α ⟨θ, hθ⟩) (t ⟨θ, hθ⟩) h simpa [policy, hθ] using intro h heq