Convex Analysis (Rockafellar, 1970) -- Chapter 05 -- Section 24 -- Part 15

section Chap05section Section24open scoped ConvexAnalysisopen scoped Topologyopen scoped Pointwiseattribute [local instance] Classical.propDecidable

Helper for Theorem 5.24.9: the Euclideanized subdifferential of the iterated upper directional derivative at Unknown identifier `y`y lies in the normal face of selected by Unknown identifier `y`y.

lemma helperForTheorem_5_24_9_iteratedSubdifferential_subset_normalFace {n : ℕ} {f : (Fin n → ℝ) → EReal} (hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f) {x y : Fin n → ℝ} (hx : x ∈ effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) (hfiniteDir : upperDirectionalDerivativeAt f x y ≠ (⊥ : EReal)) : ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (upperDirectionalDerivativeAt f x) y) ⊆ subdifferentialNormalFaceAt f x y := by intro v hv rcases helperForTheorem_5_24_9_iteratedSubgradient_mem_subdifferential_and_supportEq (f := f) hproper hx hfiniteDir hv with ⟨hvSub, hvEq⟩ have hf : ConvexFunction f := by simpa [ConvexFunction] using hproper.1 have hxFinite : f x ≠ (⊤ : EReal) ∧ f x ≠ (⊥ : EReal) := by refine ⟨?_, ?_⟩ · exact mem_effectiveDomain_imp_ne_top (S := (Set.univ : Set _)) (f := f) hx · exact hproper.2.2 x (by simp) refine ⟨hvSub, ?_⟩ intro zStar hzStar -- Theorem 23.2 bounds every subgradient pairing by `f'(x; y)`, while `v` attains that value. have hzLe : (((dotProduct y zStar : ℝ)) : EReal) ≤ upperDirectionalDerivativeAt f x y := by exact (helperForTheorem_23_2_subgradient_iff_vector_linear_minorant f hf x hxFinite zStar).1 hzStar y rw [← hvEq] at hzLe have hzLeReal : dotProduct y zStar ≤ dotProduct y v := by simpa [dotProduct_comm] using (show dotProduct y zStar ≤ dotProduct v y from by exact_mod_cast hzLe) have hsplit : dotProduct y (zStar - v) = dotProduct y zStar - dotProduct y v := by -- Expand the normal-face displacement pairing coordinatewise. unfold dotProduct have hterm : ∀ i, y i * (zStar - v) i = y i * zStar i - y i * v i := by intro i simp [sub_eq_add_neg] ring simp_rw [hterm] rw [Finset.sum_sub_distrib] rw [hsplit] linarith
-- Proof sketch: apply Theorem 5.24.8 to the translated difference-quotient functions generated by -- the secants from `x` to `xᵢ`, using the directional convergence -- `‖xᵢ - x‖⁻¹ • (xᵢ - x) → y` and the assumption that the ray `x + λ y` meets `int (dom f)` to -- place the comparison on interior-domain points. The limiting upper directional derivative is -- then the iterated derivative `f'(x; y; z)`, and the approximate-subgradient inclusion sharpens -- to the normal-face inclusion selected by `y`.

Theorem 5.24.9: let Unknown identifier `f`f be a closed proper convex function, let Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `dom`dom f, and let Unknown identifier `xᵢ`sorry ∈ sorry : Propxᵢ ∈ Unknown identifier `dom`dom f be a sequence converging to Unknown identifier `x`x with Unknown identifier `xᵢ`sorry ≠ sorry : Propxᵢ ≠ Unknown identifier `x`x and normalized directions ‖sorry - sorry‖⁻¹ • (sorry - sorry) → sorry : Sort (imax u_2 u_8)‖Unknown identifier `xᵢ`xᵢ - Unknown identifier `x`x‖⁻¹ • (Unknown identifier `xᵢ`xᵢ - Unknown identifier `x`x) → Unknown identifier `y`y. If and the half-line meets Unknown identifier `int`int (dom f), then for every Unknown identifier `z`z. Moreover, for every Unknown identifier `ε`sorry > 0 : Propε > 0, the Euclideanized subdifferentials are eventually contained in subdifferentialNormalFaceAt sorry sorry sorry + sorry : ?m.5subdifferentialNormalFaceAt Unknown identifier `f`f Unknown identifier `x`x Unknown identifier `y`y + Unknown identifier `ε`ε B, where Unknown identifier `B`B is the Euclidean unit ball.

theorem closedProperConvex_limsup_upperDirectionalDerivative_le_iterated_and_eventual_subdifferential_subset_normalFace {n : ℕ} (f : (Fin n → ℝ) → EReal) (unused variable `hclosed` Note: This linter can be disabled with `set_option linter.unusedVariables false`hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f) {x y : Fin n → ℝ} (hx : x ∈ effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) (xSeq : ℕ → Fin n → ℝ) (unused variable `hxSeq` Note: This linter can be disabled with `set_option linter.unusedVariables false`hxSeq : ∀ i : ℕ, xSeq i ∈ effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) (hxSeq_tendsto : Filter.Tendsto xSeq Filter.atTop (nhds x)) (hxSeq_ne : ∀ i : ℕ, xSeq i ≠ x) (hdir : Filter.Tendsto (fun i : ℕ => ‖xSeq i - x‖⁻¹ • (xSeq i - x)) Filter.atTop (nhds y)) (hfiniteDir : upperDirectionalDerivativeAt f x y ≠ (⊥ : EReal)) (hray : ∃ t : ℝ, 0 ≤ t ∧ x + t • y ∈ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f)) : (∀ z : Fin n → ℝ, Filter.limsup (fun i => upperDirectionalDerivativeAt f (xSeq i) z) Filter.atTop ≤ upperDirectionalDerivativeAt (upperDirectionalDerivativeAt f x) y z) ∧ ∀ ε : ℝ, 0 < ε → ∃ i0 : ℕ, ∀ i ≥ i0, ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f (xSeq i)) ⊆ Set.image2 (fun u v : Fin n → ℝ => u + v) (subdifferentialNormalFaceAt f x y) (Metric.closedBall (0 : Fin n → ℝ) ε) := by have hf : ConvexFunction f := by simpa [ConvexFunction] using hproper.1 have hxFinite : f x ≠ (⊤ : EReal) ∧ f x ≠ (⊥ : EReal) := by refine ⟨?_, ?_⟩ · exact mem_effectiveDomain_imp_ne_top (S := (Set.univ : Set _)) (f := f) hx · exact hproper.2.2 x (by simp) rcases convex_directionalDerivative_monotone_exists_and_sublinear f hf x hxFinite with ⟨_hdirData, _hposD, hconvD, _hzeroD, _hsymmD⟩ -- Choose a positive interior point on the ray through `y`. rcases helperForTheorem_5_24_9_positiveRayScale (f := f) (x := x) (y := y) hray with ⟨s, hs_pos, hsy_mem⟩ let tSeq : ℕ → ℝ := fun i => ‖xSeq i - x‖ let uSeq : ℕ → Fin n → ℝ := fun i => ‖xSeq i - x‖⁻¹ • (xSeq i - x) rcases helperForTheorem_5_24_9_normalizedSecantData (x := x) (y := y) xSeq hxSeq_tendsto hxSeq_ne hdir with ⟨ht_tendsto, ht_pos, hx_reconstruct, hu_tendsto⟩ let C : Set (Fin n → ℝ) := {u : Fin n → ℝ | x + s • u ∈ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f)} rcases helperForTheorem_5_24_9_rayNeighborhood_geometry (f := f) hproper hx hs_pos hsy_mem with ⟨hCopen, hCconv, hy_mem, hshort_mem⟩ rcases helperForTheorem_5_24_9_eventually_mem_rayNeighborhood_and_le_scale (f := f) hproper hx hs_pos hsy_mem tSeq uSeq ht_tendsto hu_tendsto with ⟨i0, hi0⟩ let gTail : ℕ → (Fin n → ℝ) → EReal := fun i u => directionalDifferenceQuotientAt f x u (tSeq (i + i0)) have hgTail : gTail = fun i u => directionalDifferenceQuotientAt f x u (tSeq (i + i0)) := rfl rcases helperForTheorem_5_24_9_secantQuotient_tailHypotheses (f := f) hproper hx hs_pos hshort_mem (tSeq := tSeq) (uSeq := uSeq) (i0 := i0) ht_pos (fun i hi => (hi0 i hi).2) (fun i hi => (hi0 i hi).1) ht_tendsto hgTail with ⟨hgConv, hgFinite, hgPoint⟩ have hDfFinite : ∀ u ∈ C, upperDirectionalDerivativeAt f x u ≠ (⊤ : EReal) ∧ upperDirectionalDerivativeAt f x u ≠ (⊥ : EReal) := by -- The limit function `u ↦ f'(x; u)` is finite on the fixed ray-neighborhood. exact helperForTheorem_5_24_9_limitFunction_finite_on_rayNeighborhood (f := f) hproper hx hs_pos hy_mem hfiniteDir hshort_mem -- Route correction: we apply Theorem 5.24.8 to the tail secant-quotient family on `C`, -- then transport its conclusions back to `f` using the proved derivative and subgradient -- transport lemmas. have hmainTail := convexOn_pointwiseLimit_limsup_upperDirectionalDerivative_le_and_eventual_subdifferential_subset (C := C) hCopen hCconv hconvD hDfFinite gTail hgConv hgFinite hy_mem (fun i => uSeq (i + i0)) (fun i => (hi0 (i + i0) (Nat.le_add_left i0 i)).1) (hu_tendsto.comp (Filter.tendsto_add_atTop_nat i0)) hgPoint rcases hmainTail with ⟨hlimTail, hsubTail⟩ refine ⟨?_, ?_⟩ · intro z have htail : Filter.limsup (fun i => upperDirectionalDerivativeAt (gTail i) (uSeq (i + i0)) z) Filter.atTop ≤ upperDirectionalDerivativeAt (upperDirectionalDerivativeAt f x) y z := by -- Theorem 5.24.8 gives the limsup control for the tail family at the limit point `y`. simpa using hlimTail z (fun _ => z) tendsto_const_nhds have hrewriteTail : (fun i => upperDirectionalDerivativeAt (gTail i) (uSeq (i + i0)) z) =ᶠ[Filter.atTop] (fun i => upperDirectionalDerivativeAt f (xSeq (i + i0)) z) := by refine Filter.Eventually.of_forall ?_ intro i have htailStep := hi0 (i + i0) (Nat.le_add_left i0 i) have hfiniteStep := hshort_mem htailStep.1 (ht_pos (i + i0)) htailStep.2 rw [hgTail] calc upperDirectionalDerivativeAt (fun v => directionalDifferenceQuotientAt f x v (tSeq (i + i0))) (uSeq (i + i0)) z = upperDirectionalDerivativeAt f (x + tSeq (i + i0) • uSeq (i + i0)) z := by -- Differentiate the fixed-step quotient and transport back to the translated base point. exact helperForTheorem_5_24_9_secantQuotient_derivative_transport (f := f) hproper hf (x := x) (u := uSeq (i + i0)) (z := z) (t := tSeq (i + i0)) hxFinite ⟨hfiniteStep.2.1, hfiniteStep.2.2⟩ (ht_pos (i + i0)) _ = upperDirectionalDerivativeAt f (xSeq (i + i0)) z := by rw [hx_reconstruct (i + i0)] have htail' : Filter.limsup (fun i => upperDirectionalDerivativeAt f (xSeq (i + i0)) z) Filter.atTop ≤ upperDirectionalDerivativeAt (upperDirectionalDerivativeAt f x) y z := by rw [← Filter.limsup_congr hrewriteTail] exact htail have hshiftLimsup : Filter.limsup (fun i => upperDirectionalDerivativeAt f (xSeq (i + i0)) z) Filter.atTop = Filter.limsup (fun i => upperDirectionalDerivativeAt f (xSeq i) z) Filter.atTop := by -- Passing to a tail does not change the `atTop` limsup. rw [Filter.limsup_eq, Filter.limsup_eq] congr 1 ext a constructor · intro h rcases Filter.eventually_atTop.1 h with ⟨N, hN⟩ refine Filter.eventually_atTop.2 ⟨N + i0, ?_⟩ intro b hb have hb' : N ≤ b - i0 := by omega have htmp := hN (b - i0) hb' have hEq : b - i0 + i0 = b := by omega simpa [hEq] using htmp · intro h rcases Filter.eventually_atTop.1 h with ⟨N, hN⟩ refine Filter.eventually_atTop.2 ⟨N, ?_⟩ intro b hb exact hN (b + i0) (by omega) rw [hshiftLimsup] at htail' exact htail' · intro ε hε rcases hsubTail ε hε with ⟨i1, hi1⟩ have hface : ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (upperDirectionalDerivativeAt f x) y) ⊆ subdifferentialNormalFaceAt f x y := by -- The iterated subdifferential already lies in the normal face singled out by `y`. exact helperForTheorem_5_24_9_iteratedSubdifferential_subset_normalFace (f := f) hproper hx hfiniteDir have hball_eq : ({v : Fin n → ℝ | ‖v‖ ≤ ε} : Set (Fin n → ℝ)) = Metric.closedBall (0 : Fin n → ℝ) ε := by ext v simp refine ⟨i0 + i1, ?_⟩ intro k hk let j : ℕ := k - i0 have hk_ge_i0 : i0 ≤ k := by omega have hj_ge_i1 : i1 ≤ j := by dsimp [j] omega have hjk : j + i0 = k := by dsimp [j] omega have htailIncl := hi1 j hj_ge_i1 have htailStep := hi0 (j + i0) (by omega) have hfiniteStep := hshort_mem htailStep.1 (ht_pos (j + i0)) htailStep.2 have hleftEq : ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (gTail j) (uSeq (j + i0))) = ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f (xSeq k)) := by rw [hgTail] calc ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (fun v => directionalDifferenceQuotientAt f x v (tSeq (j + i0))) (uSeq (j + i0))) = ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f (x + tSeq (j + i0) • uSeq (j + i0))) := by -- Transport the fixed-step subdifferential back to the translated point of `f`. exact helperForTheorem_5_24_9_secantQuotient_subdifferential_transport (f := f) hproper hf (x := x) (u := uSeq (j + i0)) (t := tSeq (j + i0)) hxFinite ⟨hfiniteStep.2.1, hfiniteStep.2.2⟩ (ht_pos (j + i0)) _ = ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f (xSeq (j + i0))) := by rw [hx_reconstruct (j + i0)] _ = ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f (xSeq k)) := by rw [hjk] have hrightSubset : Set.image2 (fun u v : Fin n → ℝ => u + v) (((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (upperDirectionalDerivativeAt f x) y)) {v : Fin n → ℝ | ‖v‖ ≤ ε} ⊆ Set.image2 (fun u v : Fin n → ℝ => u + v) (subdifferentialNormalFaceAt f x y) (Metric.closedBall (0 : Fin n → ℝ) ε) := by rw [← hball_eq] intro w hw rcases hw with ⟨u0, hu0, v0, hv0, rfl⟩ exact ⟨u0, hface hu0, v0, hv0, rfl⟩ have : ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f (xSeq k)) ⊆ Set.image2 (fun u v : Fin n → ℝ => u + v) (subdifferentialNormalFaceAt f x y) (Metric.closedBall (0 : Fin n → ℝ) ε) := by rw [← hleftEq] exact Set.Subset.trans htailIncl hrightSubset exact this

The Euclideanized union of the subdifferentials over points Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `S`S.

def subdifferentialImageOn {n : ℕ} (f : (Fin n → ℝ) → EReal) (S : Set (Fin n → ℝ)) : Set (Fin n → ℝ) := ⋃ x ∈ S, ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x)

Helper for Theorem 5.24.10: the second-coordinate projection of the subdifferential graph over Unknown identifier `S`S is exactly the Euclideanized union .

lemma helperForTheorem_5_24_10_subdifferentialGraphOn_projection_eq_imageOn {n : ℕ} {f : (Fin n → ℝ) → EReal} {S : Set (Fin n → ℝ)} : Prod.snd '' {p : (Fin n → ℝ) × (Fin n → ℝ) | p.1 ∈ S ∧ p.2 ∈ ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f p.1)} = subdifferentialImageOn f S := by ext xStar constructor · intro hxStar -- Unpack a graph point and read off its second coordinate as an element of the union. rcases hxStar with ⟨p, hp, rfl⟩ exact Set.mem_iUnion.2 ⟨p.1, Set.mem_iUnion.2 ⟨hp.1, hp.2⟩⟩ · intro hxStar -- Conversely, every element of the union comes from the graph point `(x, xStar)`. simp only [subdifferentialImageOn, Set.mem_iUnion] at hxStar rcases hxStar with ⟨x, hxS, hxSub⟩ exact ⟨(x, xStar), ⟨hxS, hxSub⟩, rfl⟩

Helper for Theorem 5.24.10: compactness of Unknown identifier `S`S and Corollary 5.24.2 give a uniform bound on the Euclideanized subdifferentials over Unknown identifier `S`S.

lemma helperForTheorem_5_24_10_subdifferentialImageOn_isBounded {n : ℕ} (f : (Fin n → ℝ) → EReal) (hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f) {S : Set (Fin n → ℝ)} (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) (hSint : S ⊆ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f)) : Bornology.IsBounded (subdifferentialImageOn f S) := by classical let K : (Fin n → ℝ) → Set (Fin n → ℝ) := fun x => Set.image2 (fun u v : Fin n → ℝ => u + v) (((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x)) (Metric.closedBall (0 : Fin n → ℝ) 1) have hScompact : IsCompact S := by -- Closed and bounded subsets of `ℝⁿ` are compact. exact (Metric.isCompact_iff_isClosed_bounded).2 ⟨hSclosed, hSbdd⟩ have hlocal : ∀ x : S, ∃ δ : ℝ, 0 < δ ∧ Bornology.IsBounded (K x.1) ∧ ∀ ⦃z : Fin n → ℝ⦄, z ∈ Metric.ball x.1 δ → ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f z) ⊆ K x.1 := by intro x have hxS : x.1 ∈ S := x.2 have hxInt : x.1 ∈ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) := hSint hxS have hxSub : Set.Nonempty (subdifferentialAt f x.1) ∧ Bornology.IsBounded ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x.1) := by exact ((subdifferential_empty_off_effectiveDomain_nonempty_on_relativeInterior_and_bounded_iff_mem_interior f hproper x.1).2.2.1).2 hxInt rcases (properConvex_upperSemicontinuousOn_upperDirectionalDerivative_and_subdifferential_subset (f := f) hproper).2 hxInt 1 (by norm_num) with ⟨δ, hδpos, hδsub⟩ have hKbdd : Bornology.IsBounded (K x.1) := by -- Each local model is a bounded fiber translated by the bounded unit ball. simpa [K, Set.image2_add] using (isBounded_add hxSub.2 (Metric.isBounded_closedBall (x := (0 : Fin n → ℝ)) (r := 1))) refine ⟨δ, hδpos, hKbdd, ?_⟩ intro z hz exact hδsub (Metric.ball_subset_closedBall hz) choose δ hδpos hKbdd hsub using hlocal have hcoverAll : S ⊆ ⋃ x : S, Metric.ball x.1 (δ x) := by intro z hzS -- The center `z` itself belongs to its own local ball because `δ z > 0`. refine Set.mem_iUnion.2 ⟨⟨z, hzS⟩, ?_⟩ simpa [Metric.mem_ball] using hδpos ⟨z, hzS⟩ rcases hScompact.elim_finite_subcover (fun x : S => Metric.ball x.1 (δ x)) (fun _x => by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using Metric.isOpen_ball) hcoverAll with ⟨T, hcover⟩ have hKbUnion : Bornology.IsBounded (⋃ x ∈ T, K x.1) := by -- A finite union of bounded local models is bounded. rw [Bornology.isBounded_biUnion_finset] intro x hxT exact hKbdd x refine hKbUnion.subset ?_ intro xStar hxStar simp only [subdifferentialImageOn, Set.mem_iUnion] at hxStar rcases hxStar with ⟨z, hzS, hzSub⟩ have hzCover : z ∈ ⋃ x ∈ T, Metric.ball x.1 (δ x) := hcover hzS rcases Set.mem_iUnion₂.1 hzCover with ⟨x, hxT, hzBall⟩ -- The finite subcover moves `z` into one of the bounded local models. exact Set.mem_iUnion.2 ⟨x, Set.mem_iUnion.2 ⟨hxT, hsub x hzBall hzSub⟩⟩

Helper for Theorem 5.24.10: the Euclideanized union is compact because it is the continuous image of the closed subdifferential graph over the compact base set Unknown identifier `S`S.

lemma helperForTheorem_5_24_10_subdifferentialImageOn_isCompact {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f) {S : Set (Fin n → ℝ)} (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) (hSint : S ⊆ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f)) : IsCompact (subdifferentialImageOn f S) := by classical let G : Set ((Fin n → ℝ) × (Fin n → ℝ)) := {p | p.1 ∈ S ∧ p.2 ∈ ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f p.1)} have hImageBdd : Bornology.IsBounded (subdifferentialImageOn f S) := helperForTheorem_5_24_10_subdifferentialImageOn_isBounded (f := f) hproper hSclosed hSbdd hSint have hGraphClosed : IsClosed {p : (Fin n → ℝ) × (Fin n → ℝ) | dotProductEquiv ℝ (Fin n) p.2 ∈ ∂ f p.1} := (subdifferential_limit_mem_and_isClosed_graph (f := f) hclosed hproper).2 have hBaseClosed : IsClosed {p : (Fin n → ℝ) × (Fin n → ℝ) | p.1 ∈ S} := hSclosed.preimage continuous_fst have hGclosed : IsClosed G := by -- The graph over `S` is the intersection of the closed full graph with the closed base slice. simpa [G, Set.setOf_and] using hBaseClosed.inter hGraphClosed have hGbdd : Bornology.IsBounded G := by have hprod : Bornology.IsBounded (S ×ˢ subdifferentialImageOn f S) := Bornology.IsBounded.prod hSbdd hImageBdd refine hprod.subset ?_ intro p hp refine ⟨hp.1, ?_⟩ exact Set.mem_iUnion.2 ⟨p.1, Set.mem_iUnion.2 ⟨hp.1, hp.2⟩⟩ have hGcompact : IsCompact G := by -- In finite dimensions, closed and bounded subsets of the product space are compact. exact (Metric.isCompact_iff_isClosed_bounded).2 ⟨hGclosed, hGbdd⟩ have hprojEq : Prod.snd '' G = subdifferentialImageOn f S := helperForTheorem_5_24_10_subdifferentialGraphOn_projection_eq_imageOn (f := f) (S := S) -- Project the compact graph to recover compactness of the union. simpa [hprojEq] using hGcompact.image continuous_snd
-- Proof sketch: combine the local boundedness and upper-semicontinuity of the subdifferential -- mapping from Corollary 5.24.2 with compactness of the closed bounded set `S ⊆ int (dom f)` to -- obtain a uniform bound and closedness for the Euclideanized union of subdifferentials over `S`. -- Then estimate each directional derivative by the support of that uniformly bounded set, and use -- the directional-derivative bound on the segment between `x` and `y` to derive the Lipschitz -- estimate for `f` on `S`.

Theorem 5.24.10: if Unknown identifier `f`f is a closed proper convex function and Unknown identifier `S`S is a nonempty closed bounded subset of Unknown identifier `int`int (dom f), then the Euclideanized union subdifferentialImageOn sorry sorry : Set (Fin ?m.1 → ℝ)subdifferentialImageOn Unknown identifier `f`f Unknown identifier `S`S of the subdifferentials for Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `S`S is nonempty, closed, and bounded. Writing Unknown identifier `α`sorry = sorry : Propα = Unknown identifier `sup`sup {euclideanNorm xStar | xStar ∈ subdifferentialImageOn f S}, one has for every Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `S`S and every direction Unknown identifier `z`z, and for all , where Unknown identifier `f`f x and Unknown identifier `f`f y are read as real values on Unknown identifier `int`int (dom f). This is the book's Euclidean-norm statement; later uses can convert back to the ambient sup norm by finite-dimensional norm equivalence.

theorem closedProperConvex_subdifferentialImageOn_nonempty_closed_bounded_and_lipschitzOn {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f) {S : Set (Fin n → ℝ)} (hSne : S.Nonempty) (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) (hSint : S ⊆ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f)) : Set.Nonempty (subdifferentialImageOn f S) ∧ IsClosed (subdifferentialImageOn f S) ∧ Bornology.IsBounded (subdifferentialImageOn f S) ∧ let α : ℝ := sSup ((fun xStar : Fin n → ℝ => euclideanNorm xStar) '' subdifferentialImageOn f S) (∀ x ∈ S, ∀ z : Fin n → ℝ, upperDirectionalDerivativeAt f x z ≤ ((α * euclideanNorm z : ℝ) : EReal)) ∧ ∀ x ∈ S, ∀ y ∈ S, |(f y).toReal - (f x).toReal| ≤ α * euclideanNorm (y - x) := by have hImageNonempty : Set.Nonempty (subdifferentialImageOn f S) := by rcases hSne with ⟨x, hxS⟩ have hxInt : x ∈ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) := hSint hxS have hxSub : Set.Nonempty (subdifferentialAt f x) ∧ Bornology.IsBounded ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) := by exact ((subdifferential_empty_off_effectiveDomain_nonempty_on_relativeInterior_and_bounded_iff_mem_interior f hproper x).2.2.1).2 hxInt rcases hxSub.1 with ⟨xDual, hxDual⟩ -- An interior-domain point contributes at least one subgradient to the union. refine ⟨(dotProductEquiv ℝ (Fin n)).symm xDual, ?_⟩ exact Set.mem_iUnion.2 ⟨x, Set.mem_iUnion.2 ⟨hxS, by simpa using hxDual⟩⟩ have hImageCompact : IsCompact (subdifferentialImageOn f S) := helperForTheorem_5_24_10_subdifferentialImageOn_isCompact (f := f) hclosed hproper hSclosed hSbdd hSint have hImageClosed : IsClosed (subdifferentialImageOn f S) := hImageCompact.isClosed have hImageBdd : Bornology.IsBounded (subdifferentialImageOn f S) := hImageCompact.isBounded refine ⟨hImageNonempty, hImageClosed, hImageBdd, ?_⟩ dsimp let α : ℝ := sSup ((fun xStar : Fin n → ℝ => euclideanNorm xStar) '' subdifferentialImageOn f S) have hContEuclideanNorm : Continuous (fun xStar : Fin n → ℝ => euclideanNorm xStar) := by let e : (Fin n → ℝ) →L[ℝ] EuclideanSpace ℝ (Fin n) := (EuclideanSpace.equiv (Fin n) ℝ).symm have hEq : (fun xStar : Fin n → ℝ => euclideanNorm xStar) = fun xStar => ‖e xStar‖ := by funext xStar simpa [euclideanNorm, e] using section13_sqrt_dotProduct_self_eq_norm_euclideanSpace (n := n) (x := xStar) rw [hEq] exact e.continuous.norm have hNormImageCompact : IsCompact ((fun xStar : Fin n → ℝ => euclideanNorm xStar) '' subdifferentialImageOn f S) := by exact hImageCompact.image hContEuclideanNorm have hNormBddAbove : BddAbove ((fun xStar : Fin n → ℝ => euclideanNorm xStar) '' subdifferentialImageOn f S) := hNormImageCompact.bddAbove have hAlphaBound : ∀ xStar ∈ subdifferentialImageOn f S, euclideanNorm xStar ≤ α := by intro xStar hxStar exact le_csSup hNormBddAbove ⟨xStar, hxStar, rfl⟩ have hSupportBound : ∀ z : Fin n → ℝ, supportFunctionEReal (subdifferentialImageOn f S) z ≤ ((α * euclideanNorm z : ℝ) : EReal) := by intro z refine (section13_supportFunctionEReal_le_coe_iff (C := subdifferentialImageOn f S) (y := z) (μ := α * euclideanNorm z)).2 ?_ intro xStar hxStar have hxAlpha : euclideanNorm xStar ≤ α := hAlphaBound xStar hxStar have hzNonneg : 0 ≤ euclideanNorm z := by simp [euclideanNorm] calc dotProduct xStar z ≤ euclideanNorm xStar * euclideanNorm z := by simpa [euclideanNorm] using section13_dotProduct_le_sqrt_mul_sqrt (n := n) xStar z _ ≤ α * euclideanNorm z := by exact mul_le_mul_of_nonneg_right hxAlpha hzNonneg refine ⟨?_, ?_⟩ · intro x hxS z have hxInt : x ∈ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) := hSint hxS have hxri : x ∈ euclideanRelativeInterior_fin n (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) := helperForTheorem_23_4_mem_relativeInterior_of_mem_interior (n := n) (C := effectiveDomain Set.univ f) hxInt have hsubset : ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) ⊆ subdifferentialImageOn f S := by intro xStar hxStar exact Set.mem_iUnion.2 ⟨x, Set.mem_iUnion.2 ⟨hxS, hxStar⟩⟩ have hDirEq : upperDirectionalDerivativeAt f x z = subdifferentialSupportAt f x z := by exact (helperForTheorem_23_4_directionalDerivative_regularity_of_mem_relativeInterior (f := f) hproper x hxri).2.2.2.2 z calc upperDirectionalDerivativeAt f x z = subdifferentialSupportAt f x z := hDirEq _ = supportFunctionEReal (((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x)) z := by symm exact helperForTheorem_23_2_supportFunctionEReal_preimage_subdifferential_eq f x z _ ≤ supportFunctionEReal (subdifferentialImageOn f S) z := helperForTheorem_23_6_supportFunctionEReal_mono_of_subset hsubset z _ ≤ ((α * euclideanNorm z : ℝ) : EReal) := hSupportBound z · intro x hxS y hyS have hxInt : x ∈ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) := hSint hxS have hyInt : y ∈ interior (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f) := hSint hyS have hxFinite : f x ≠ (⊤ : EReal) ∧ f x ≠ (⊥ : EReal) := by exact ⟨mem_effectiveDomain_imp_ne_top (S := (Set.univ : Set (Fin n → ℝ))) (f := f) (interior_subset hxInt), hproper.2.2 x (by simp)⟩ have hyFinite : f y ≠ (⊤ : EReal) ∧ f y ≠ (⊥ : EReal) := by exact ⟨mem_effectiveDomain_imp_ne_top (S := (Set.univ : Set (Fin n → ℝ))) (f := f) (interior_subset hyInt), hproper.2.2 y (by simp)⟩ have hxSub : Set.Nonempty (subdifferentialAt f x) ∧ Bornology.IsBounded ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) := by exact ((subdifferential_empty_off_effectiveDomain_nonempty_on_relativeInterior_and_bounded_iff_mem_interior f hproper x).2.2.1).2 hxInt have hySub : Set.Nonempty (subdifferentialAt f y) ∧ Bornology.IsBounded ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f y) := by exact ((subdifferential_empty_off_effectiveDomain_nonempty_on_relativeInterior_and_bounded_iff_mem_interior f hproper y).2.2.1).2 hyInt rcases hxSub.1 with ⟨pxDual, hpxDual⟩ rcases hySub.1 with ⟨pyDual, hpyDual⟩ let px : Fin n → ℝ := (dotProductEquiv ℝ (Fin n)).symm pxDual let py : Fin n → ℝ := (dotProductEquiv ℝ (Fin n)).symm pyDual have hpxSub : dotProductEquiv ℝ (Fin n) px ∈ ∂ f x := by simpa [px] using hpxDual have hpySub : dotProductEquiv ℝ (Fin n) py ∈ ∂ f y := by simpa [py] using hpyDual have hpxImage : px ∈ subdifferentialImageOn f S := by exact Set.mem_iUnion.2 ⟨x, Set.mem_iUnion.2 ⟨hxS, by simpa using hpxSub⟩⟩ have hpyImage : py ∈ subdifferentialImageOn f S := by exact Set.mem_iUnion.2 ⟨y, Set.mem_iUnion.2 ⟨hyS, by simpa using hpySub⟩⟩ have hdispNonneg : 0 ≤ euclideanNorm (y - x) := by simp [euclideanNorm] have hpxPair : dotProduct px (y - x) ≤ α * euclideanNorm (y - x) := by have hpxAlpha : euclideanNorm px ≤ α := hAlphaBound px hpxImage calc dotProduct px (y - x) ≤ euclideanNorm px * euclideanNorm (y - x) := by simpa [euclideanNorm] using section13_dotProduct_le_sqrt_mul_sqrt (n := n) px (y - x) _ ≤ α * euclideanNorm (y - x) := by exact mul_le_mul_of_nonneg_right hpxAlpha hdispNonneg have hpyPair : dotProduct py (y - x) ≤ α * euclideanNorm (y - x) := by have hpyAlpha : euclideanNorm py ≤ α := hAlphaBound py hpyImage calc dotProduct py (y - x) ≤ euclideanNorm py * euclideanNorm (y - x) := by simpa [euclideanNorm] using section13_dotProduct_le_sqrt_mul_sqrt (n := n) py (y - x) _ ≤ α * euclideanNorm (y - x) := by exact mul_le_mul_of_nonneg_right hpyAlpha hdispNonneg have hpxPairRev : dotProduct px (x - y) ≤ α * euclideanNorm (y - x) := by have hpxAlpha : euclideanNorm px ≤ α := hAlphaBound px hpxImage have hdispEq : euclideanNorm (x - y) = euclideanNorm (y - x) := by simp [euclideanNorm, dotProduct_comm, sub_eq_add_neg, This simp argument is unused: add_assoc Hint: Omit it from the simp argument list. simp [euclideanNorm, dotProduct_comm, sub_eq_add_neg, add_a̵s̵s̵o̵c̵,̵ ̵a̵d̵d̵_̵left_comm, add_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_assoc, add_left_comm, add_comm] calc dotProduct px (x - y) ≤ euclideanNorm px * euclideanNorm (x - y) := by simpa [euclideanNorm] using section13_dotProduct_le_sqrt_mul_sqrt (n := n) px (x - y) _ ≤ α * euclideanNorm (x - y) := by exact mul_le_mul_of_nonneg_right hpxAlpha (by simp [euclideanNorm]) _ = α * euclideanNorm (y - x) := by rw [hdispEq] have hLowerE : f x + (((dotProduct px (y - x) : ℝ)) : EReal) ≤ f y := by simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using hpxSub y have hUpperReal : (f y).toReal - (f x).toReal ≤ α * euclideanNorm (y - x) := by have hAtX : f y + (((dotProduct py (x - y) : ℝ)) : EReal) ≤ f x := by simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using hpySub x rw [← EReal.coe_toReal hyFinite.1 hyFinite.2, ← EReal.coe_toReal hxFinite.1 hxFinite.2] at hAtX have hReal : (f y).toReal + (dotProduct py x - dotProduct py y) ≤ (f x).toReal := by exact (EReal.coe_le_coe_iff.mp (by simpa [sub_eq_add_neg, EReal.coe_add, dotProduct_sub, add_assoc, add_left_comm, add_comm] using hAtX)) have hpyNeg : dotProduct py (x - y) = -(dotProduct py (y - x)) := by rw [dotProduct_sub, dotProduct_sub] ring have hReal' : (f y).toReal - (f x).toReal ≤ dotProduct py (y - x) := by have hEq : dotProduct py x - dotProduct py y = dotProduct py (x - y) := by rw [dotProduct_sub] rw [hEq] at hReal have hTmp : (f y).toReal - (f x).toReal ≤ -(dotProduct py (x - y)) := by linarith simpa [hpyNeg] using hTmp exact le_trans hReal' hpyPair have hLowerReal : (f x).toReal - (f y).toReal ≤ α * euclideanNorm (y - x) := by rw [← EReal.coe_toReal hxFinite.1 hxFinite.2, ← EReal.coe_toReal hyFinite.1 hyFinite.2] at hLowerE have hReal : (f x).toReal + (dotProduct px y - dotProduct px x) ≤ (f y).toReal := by exact (EReal.coe_le_coe_iff.mp (by simpa [sub_eq_add_neg, EReal.coe_add, dotProduct_sub, add_assoc, add_left_comm, add_comm] using hLowerE)) have hpxLower : -(α * euclideanNorm (y - x)) ≤ dotProduct px (y - x) := by have hpxNeg : dotProduct px (y - x) = -(dotProduct px (x - y)) := by rw [dotProduct_sub, dotProduct_sub] ring linarith have hReal' : (f x).toReal - (f y).toReal ≤ -(dotProduct px (y - x)) := by have hEq : dotProduct px y - dotProduct px x = dotProduct px (y - x) := by rw [dotProduct_sub] rw [hEq] at hReal linarith have hUpperNeg : -(dotProduct px (y - x)) ≤ α * euclideanNorm (y - x) := by linarith exact le_trans hReal' hUpperNeg have hAbs : |(f y).toReal - (f x).toReal| ≤ α * euclideanNorm (y - x) := by rw [abs_le] constructor · linarith · linarith simpa [sub_eq_add_neg] using hAbs

Helper for Theorem 5.24.11: cyclic monotonicity descends along a pointwise graph inclusion.

lemma helperForTheorem_5_24_11_pointwiseSubset_preserves_isCyclicallyMonotone {n : ℕ} {ρ σ : (Fin n → ℝ) → Set (Fin n → ℝ)} (hσ : IsCyclicallyMonotone σ) (hsubset : ∀ x : Fin n → ℝ, ρ x ⊆ σ x) : IsCyclicallyMonotone ρ := by intro m x xStar hxStar -- Replace each selected graph point of `ρ` by the same graph point viewed in `σ`. refine hσ m x xStar ?_ intro i exact hsubset (x i) (hxStar i)

Helper for Theorem 5.24.11: if the graph of Unknown identifier `ρ`ρ is empty, the zero function already provides the required closed proper convex potential.

lemma helperForTheorem_5_24_11_emptyGraph_exists_closedProperConvex_subdifferential_superset {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} (hempty : ∀ x : Fin n → ℝ, ρ x = ∅) : ∃ f : (Fin n → ℝ) → EReal, ClosedConvexFunction f ∧ ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f ∧ ∀ x : Fin n → ℝ, ρ x ⊆ ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) := by let f : (Fin n → ℝ) → EReal := fun _ => (0 : EReal) have hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f := properConvexFunctionOn_const (n := n) 0 have hclosed : ClosedConvexFunction f := by -- A finite constant function is lower semicontinuous, hence closed once properness is known. exact (properConvexFunction_closed_iff_lowerSemicontinuous hproper).2 lowerSemicontinuous_const have hsubset : ∀ x : Fin n → ℝ, ρ x ⊆ ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) := by intro x -- The empty graph branch has no subgradient obligations to discharge. rw [hempty x] simp exact ⟨f, hclosed, hproper, hsubset⟩

Helper for Theorem 5.24.11: the affine-tail value contributed by a finite graph chain based at the anchor Unknown identifier `a`a.

def helperForTheorem_5_24_11_rockafellarCandidateValue {n m : ℕ} (x xStar : Fin (m + 1) → Fin n → ℝ) (y : Fin n → ℝ) : EReal := (∑ i : Fin m, (((dotProduct (x i.succ - x i.castSucc) (xStar i.castSucc) : ℝ)) : EReal)) + (((dotProduct (y - x (Fin.last m)) (xStar (Fin.last m)) : ℝ)) : EReal)

Helper for Theorem 5.24.11: the admissible affine-tail chain values used in Rockafellar's path-supremum construction from the anchor Unknown identifier `a`a.

def helperForTheorem_5_24_11_rockafellarCandidateSet {n : ℕ} (ρ : (Fin n → ℝ) → Set (Fin n → ℝ)) (a y : Fin n → ℝ) : Set EReal := {q : EReal | ∃ m : ℕ, ∃ x xStar : Fin (m + 1) → Fin n → ℝ, x 0 = a ∧ (∀ i : Fin (m + 1), xStar i ∈ ρ (x i)) ∧ q = helperForTheorem_5_24_11_rockafellarCandidateValue x xStar y}

Helper for Theorem 5.24.11: Rockafellar's raw potential is the supremum of all admissible affine-tail chain values based at the anchor Unknown identifier `a`a.

noncomputable def helperForTheorem_5_24_11_rockafellarPotential {n : ℕ} (ρ : (Fin n → ℝ) → Set (Fin n → ℝ)) (a : Fin n → ℝ) : (Fin n → ℝ) → EReal := fun y => sSup (helperForTheorem_5_24_11_rockafellarCandidateSet ρ a y)

Helper for Theorem 5.24.11: appending one more graph point adds exactly the expected affine tail term to the chain value.

lemma helperForTheorem_5_24_11_rockafellarCandidateValue_append {n m : ℕ} (x xStar : Fin (m + 1) → Fin n → ℝ) (xNew v y : Fin n → ℝ) : helperForTheorem_5_24_11_rockafellarCandidateValue (Fin.snoc x xNew) (Fin.snoc xStar v) y = helperForTheorem_5_24_11_rockafellarCandidateValue x xStar xNew + (((dotProduct (y - xNew) v : ℝ)) : EReal) := by -- Split the appended chain into the original edges and the final new edge. rw [helperForTheorem_5_24_11_rockafellarCandidateValue, helperForTheorem_5_24_11_rockafellarCandidateValue, Fin.sum_univ_castSucc] -- The `Fin.snoc` identities identify the old part of the chain and isolate the new tail. simp only [Fin.snoc_castSucc, Fin.snoc_last, Fin.succ_castSucc, Fin.succ_last, add_assoc]

Helper for Theorem 5.24.11: once a chain contributes a value at Unknown identifier `x`x, appending a graph point (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `v`v) produces the shifted affine-tail value at any Unknown identifier `y`y.

lemma helperForTheorem_5_24_11_appendCandidate_mem_rockafellarCandidateSet {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} {a x y v : Fin n → ℝ} (hv : v ∈ ρ x) {q : EReal} (hq : q ∈ helperForTheorem_5_24_11_rockafellarCandidateSet ρ a x) : q + (((dotProduct (y - x) v : ℝ)) : EReal) ∈ helperForTheorem_5_24_11_rockafellarCandidateSet ρ a y := by rcases hq with ⟨m, xChain, xStarChain, hx0, hmem, rfl⟩ -- Append the new graph point to the old admissible chain. refine ⟨m + 1, Fin.snoc xChain x, Fin.snoc xStarChain v, ?_, ?_, ?_⟩ · -- The anchor point is unchanged by appending at the end. simpa using hx0 · -- Every old graph membership is preserved, and the final point uses `hv`. intro i refine Fin.lastCases ?_ ?_ i · simpa [Fin.snoc_last] using hv · intro j simpa [Fin.snoc_castSucc] using hmem j · -- The appended chain value is exactly the old value plus the new tail term. exact (helperForTheorem_5_24_11_rockafellarCandidateValue_append xChain xStarChain x v y).symm

Helper for Theorem 5.24.11: the length-zero chain at the anchor gives the basic affine lower bound for Rockafellar's raw potential.

lemma helperForTheorem_5_24_11_seedCandidate_le_rockafellarPotential {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} {a aStar : Fin n → ℝ} (ha : aStar ∈ ρ a) (y : Fin n → ℝ) : (((dotProduct (y - a) aStar : ℝ)) : EReal) ≤ helperForTheorem_5_24_11_rockafellarPotential ρ a y := by -- The length-zero chain contributes the affine seed value directly. refine le_sSup ?_ refine ⟨0, (fun _ => a), (fun _ => aStar), rfl, ?_, ?_⟩ · intro i simpa using ha · -- For the zero-length chain, the edge sum vanishes and only the affine tail remains. simp [helperForTheorem_5_24_11_rockafellarCandidateValue]

Helper for Theorem 5.24.11: coercing a finite real sum into EReal : TypeEReal commutes with the sum.

lemma helperForTheorem_5_24_11_eReal_coe_finsetSum {α : Type*} (s : Finset α) (f : α → ℝ) : (((Finset.sum s f : ℝ)) : EReal) = Finset.sum s (fun a => (((f a : ℝ)) : EReal)) := by classical -- Induct on the finite set and use that real coercions preserve addition in `EReal`. refine Finset.induction_on s ?_ ?_ · simp · intro a t hat hrec simp [hat, hrec, EReal.coe_add]

Helper for Theorem 5.24.11: evaluating a candidate chain at its anchor point reproduces the cyclic sum of its graph edges.

lemma helperForTheorem_5_24_11_cyclicSum_eq_candidateValue_at_anchor {n m : ℕ} (x xStar : Fin (m + 1) → Fin n → ℝ) {a : Fin n → ℝ} (hx0 : x 0 = a) : (∑ i : Fin (m + 1), dotProduct (x (cyclicSuccessor i) - x i) (xStar i) : ℝ) = (∑ i : Fin m, dotProduct (x i.succ - x i.castSucc) (xStar i.castSucc)) + dotProduct (a - x (Fin.last m)) (xStar (Fin.last m)) := by -- Split off the final edge of the cyclic sum, so the remaining terms align with the chain edges. rw [Fin.sum_univ_castSucc] -- On `Fin.castSucc`, the cyclic successor is just the ordinary successor in the chain. simp_rw [show ∀ i : Fin m, cyclicSuccessor i.castSucc = i.succ by intro i ext simp [cyclicSuccessor]] -- The last cyclic edge closes the chain back to the anchor `a = x 0`. simp [hx0, cyclicSuccessor]

Helper for Theorem 5.24.11: the cyclic sum of the snoc-extended chain is the old candidate value plus the closing anchor tail.

lemma helperForTheorem_5_24_11_cyclicSum_snoc_eq_candidateValue_add_anchorTail {n m : ℕ} (x xStar : Fin (m + 1) → Fin n → ℝ) {a : Fin n → ℝ} (unused variable `hx0` Note: This linter can be disabled with `set_option linter.unusedVariables false`hx0 : x 0 = a) (xNew v : Fin n → ℝ) : helperForTheorem_5_24_11_rockafellarCandidateValue (Fin.snoc x xNew) (Fin.snoc xStar v) a = helperForTheorem_5_24_11_rockafellarCandidateValue x xStar xNew + (((dotProduct (a - xNew) v : ℝ)) : EReal) := by -- The candidate-value append formula already specializes to the anchor evaluation. simpa using helperForTheorem_5_24_11_rockafellarCandidateValue_append x xStar xNew v a

Helper for Theorem 5.24.11: cyclic monotonicity bounds every Rockafellar candidate at Unknown identifier `x`x by the affine functional determined by any graph point (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `v`v).

lemma helperForTheorem_5_24_11_candidateUpperBound_of_cyclicMonotone {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} (hρ : IsCyclicallyMonotone ρ) {a x v : Fin n → ℝ} (hv : v ∈ ρ x) {q : EReal} (hq : q ∈ helperForTheorem_5_24_11_rockafellarCandidateSet ρ a x) : q ≤ (((dotProduct (x - a) v : ℝ)) : EReal) := by rcases hq with ⟨m, xChain, xStarChain, hx0, hmem, rfl⟩ let X : Fin (m + 2) → Fin n → ℝ := Fin.snoc xChain x let XStar : Fin (m + 2) → Fin n → ℝ := Fin.snoc xStarChain v have hreal : (∑ i : Fin m, dotProduct (xChain i.succ - xChain i.castSucc) (xStarChain i.castSucc)) + dotProduct (x - xChain (Fin.last m)) (xStarChain (Fin.last m)) ≤ dotProduct (x - a) v := by have hX0 : X 0 = a := by -- The appended chain still starts at the same anchor. simp [X, hx0] have hcycle := hρ (m + 1) X XStar (by intro i refine Fin.lastCases ?_ ?_ i · -- The newly appended graph point uses the given membership `hv`. simpa [X, XStar] using hv · intro j -- The original chain memberships are unchanged on the old indices. simpa [X, XStar] using hmem j) have hanchor : (∑ i : Fin (m + 2), dotProduct (X (cyclicSuccessor i) - X i) (XStar i) : ℝ) = (∑ i : Fin (m + 1), dotProduct (X i.succ - X i.castSucc) (XStar i.castSucc)) + dotProduct (a - X (Fin.last (m + 1))) (XStar (Fin.last (m + 1))) := by -- Rewrite the cyclic sum of the snoc-extended chain using the real anchor identity. exact helperForTheorem_5_24_11_cyclicSum_eq_candidateValue_at_anchor (x := X) (xStar := XStar) (a := a) hX0 have happend : (∑ i : Fin (m + 1), dotProduct (X i.succ - X i.castSucc) (XStar i.castSucc)) + dotProduct (a - X (Fin.last (m + 1))) (XStar (Fin.last (m + 1))) = ((∑ i : Fin m, dotProduct (xChain i.succ - xChain i.castSucc) (xStarChain i.castSucc)) + dotProduct (x - xChain (Fin.last m)) (xStarChain (Fin.last m))) + dotProduct (a - x) v := by -- Split the appended edge-sum into the old chain and the final closing edge. dsimp [X, XStar] rw [Fin.sum_univ_castSucc] simp only [Fin.snoc_castSucc, Fin.snoc_last, Fin.succ_castSucc, Fin.succ_last, add_assoc] have hsum : ((∑ i : Fin m, dotProduct (xChain i.succ - xChain i.castSucc) (xStarChain i.castSucc)) + dotProduct (x - xChain (Fin.last m)) (xStarChain (Fin.last m))) + dotProduct (a - x) v ≤ 0 := by rw [← happend, ← hanchor] exact hcycle have hdot : dotProduct (a - x) v = - dotProduct (x - a) v := by -- Expand the dot products coordinatewise to express the closing edge as the negative tail. unfold dotProduct simp_rw [Pi.sub_apply] have hterm : ∀ i : Fin n, (a i - x i) * v i = -((x i - a i) * v i) := by intro i ring simp_rw [hterm] rw [Finset.sum_neg_distrib] rw [hdot] at hsum linarith have hsumCoe : helperForTheorem_5_24_11_rockafellarCandidateValue xChain xStarChain x = ((((∑ i : Fin m, dotProduct (xChain i.succ - xChain i.castSucc) (xStarChain i.castSucc)) + dotProduct (x - xChain (Fin.last m)) (xStarChain (Fin.last m)) : ℝ)) : EReal) := by -- Rewrite the candidate value as the `EReal` coercion of its real chain expression. rw [helperForTheorem_5_24_11_rockafellarCandidateValue, ← helperForTheorem_5_24_11_eReal_coe_finsetSum (s := (Finset.univ : Finset (Fin m))) (f := fun i => dotProduct (xChain i.succ - xChain i.castSucc) (xStarChain i.castSucc)), EReal.coe_add] rw [hsumCoe] exact_mod_cast hreal

Helper for Theorem 5.24.11: pointwise membership after adding a finite affine tail transports to the corresponding SupSet.sSup.{u_1} {α : Type u_1} [self : SupSet α] : Set α → αsSup inequality.

lemma helperForTheorem_5_24_11_sSup_add_realTail_le_of_pointwise_mem (S T : Set EReal) (r : ℝ) (hmem : ∀ q : EReal, q ∈ S → q + ((r : ℝ) : EReal) ∈ T) : sSup S + ((r : ℝ) : EReal) ≤ sSup T := by have hs : sSup S ≤ sSup T - ((r : ℝ) : EReal) := by refine sSup_le ?_ intro q hq -- Every element of `S` shifts into `T`, so it lies below the shifted supremum of `T`. exact (EReal.le_sub_iff_add_le (a := q) (b := ((r : ℝ) : EReal)) (c := sSup T) (Or.inl (EReal.coe_ne_bot _)) (Or.inl (EReal.coe_ne_top _))).2 (le_sSup (hmem q hq)) -- Translate the shifted upper bound back into the desired additive form. exact (EReal.le_sub_iff_add_le (a := sSup S) (b := ((r : ℝ) : EReal)) (c := sSup T) (Or.inl (EReal.coe_ne_bot _)) (Or.inl (EReal.coe_ne_top _))).1 hs

Helper for Theorem 5.24.11: appending one graph point yields the raw subgradient inequality for Rockafellar's path-supremum potential.

lemma helperForTheorem_5_24_11_graphPoint_isSubgradient_rawPotential {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} {a x v : Fin n → ℝ} (hv : v ∈ ρ x) : let g : (Fin n → ℝ) → EReal := helperForTheorem_5_24_11_rockafellarPotential ρ a dotProductEquiv ℝ (Fin n) v ∈ subdifferentialAt g x := by -- Unfold the raw potential and prove the subgradient inequality directly via `sSup`. rw [mem_subdifferentialAt_iff] intro y simpa [helperForTheorem_5_24_11_rockafellarPotential, dotProduct_comm] using helperForTheorem_5_24_11_sSup_add_realTail_le_of_pointwise_mem (helperForTheorem_5_24_11_rockafellarCandidateSet ρ a x) (helperForTheorem_5_24_11_rockafellarCandidateSet ρ a y) (dotProduct (y - x) v) (fun q hq => helperForTheorem_5_24_11_appendCandidate_mem_rockafellarCandidateSet hv hq)

Helper for Theorem 5.24.11: every graph point of Unknown identifier `ρ`ρ gives a finite value and a genuine raw subgradient of Rockafellar's supremum potential.

lemma helperForTheorem_5_24_11_graphPoint_mem_subdifferential_rawPotential {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} {a aStar x v : Fin n → ℝ} (hρ : IsCyclicallyMonotone ρ) (ha : aStar ∈ ρ a) (hv : v ∈ ρ x) : let g : (Fin n → ℝ) → EReal := helperForTheorem_5_24_11_rockafellarPotential ρ a g x ≤ (((dotProduct (x - a) v : ℝ)) : EReal) ∧ g x ≠ (⊤ : EReal) ∧ g x ≠ (⊥ : EReal) ∧ dotProductEquiv ℝ (Fin n) v ∈ subdifferentialAt g x := by let g : (Fin n → ℝ) → EReal := helperForTheorem_5_24_11_rockafellarPotential ρ a have hupper : g x ≤ (((dotProduct (x - a) v : ℝ)) : EReal) := by -- Every admissible candidate at `x` is bounded above by the affine functional from `(x, v)`. dsimp [g, helperForTheorem_5_24_11_rockafellarPotential] refine sSup_le ?_ intro q hq exact helperForTheorem_5_24_11_candidateUpperBound_of_cyclicMonotone hρ hv hq have hlower : (((dotProduct (x - a) aStar : ℝ)) : EReal) ≤ g x := by -- The anchor seed chain still gives the textbook affine lower bound. simpa [g] using helperForTheorem_5_24_11_seedCandidate_le_rockafellarPotential ha x have hnotTop : g x ≠ (⊤ : EReal) := by intro hxTop have hEqTop : (((dotProduct (x - a) v : ℝ)) : EReal) = (⊤ : EReal) := by exact le_antisymm le_top (by simpa [hxTop] using hupper) exact EReal.coe_ne_top _ hEqTop have hnotBot : g x ≠ (⊥ : EReal) := by intro hxBot have hEqBot : (((dotProduct (x - a) aStar : ℝ)) : EReal) = (⊥ : EReal) := by exact le_antisymm (by simpa [hxBot] using hlower) bot_le exact EReal.coe_ne_bot _ hEqBot have hsub : dotProductEquiv ℝ (Fin n) v ∈ subdifferentialAt g x := by -- The raw subgradient inequality is independent of cyclic monotonicity and follows from -- append-candidate transport. simpa [g] using helperForTheorem_5_24_11_graphPoint_isSubgradient_rawPotential (ρ := ρ) (a := a) (x := x) hv exact ⟨hupper, hnotTop, hnotBot, hsub⟩

Helper for Theorem 5.24.11: each fixed admissible chain contributes an affine function of the endpoint, so its value at a convex combination is bounded by the matching convex combination of endpoint upper bounds.

lemma helperForTheorem_5_24_11_candidateValue_convexCombination_realBound {n m : ℕ} (x xStar : Fin (m + 1) → Fin n → ℝ) {b μ0 μ1 : ℝ} {y0 y1 : Fin n → ℝ} (hb : 0 ≤ b) (hb1 : b ≤ 1) (h0 : helperForTheorem_5_24_11_rockafellarCandidateValue x xStar y0 ≤ ((μ0 : ℝ) : EReal)) (h1 : helperForTheorem_5_24_11_rockafellarCandidateValue x xStar y1 ≤ ((μ1 : ℝ) : EReal)) : helperForTheorem_5_24_11_rockafellarCandidateValue x xStar ((1 - b) • y0 + b • y1) ≤ ((((1 - b) * μ0 + b * μ1 : ℝ)) : EReal) := by let c : ℝ := ∑ i : Fin m, dotProduct (x i.succ - x i.castSucc) (xStar i.castSucc) have hrepr : ∀ y : Fin n → ℝ, helperForTheorem_5_24_11_rockafellarCandidateValue x xStar y = (((c + dotProduct (y - x (Fin.last m)) (xStar (Fin.last m)) : ℝ)) : EReal) := by intro y -- Separate the chain-dependent constant edge sum from the affine tail at `y`. dsimp [c, helperForTheorem_5_24_11_rockafellarCandidateValue] calc (∑ i : Fin m, (((dotProduct (x i.succ - x i.castSucc) (xStar i.castSucc) : ℝ)) : EReal)) + (((dotProduct (y - x (Fin.last m)) (xStar (Fin.last m)) : ℝ)) : EReal) = ((((∑ i : Fin m, dotProduct (x i.succ - x i.castSucc) (xStar i.castSucc) : ℝ)) : EReal)) + (((dotProduct (y - x (Fin.last m)) (xStar (Fin.last m)) : ℝ)) : EReal) := by rw [← helperForTheorem_5_24_11_eReal_coe_finsetSum (s := (Finset.univ : Finset (Fin m))) (f := fun i => dotProduct (x i.succ - x i.castSucc) (xStar i.castSucc))] _ = (((c + dotProduct (y - x (Fin.last m)) (xStar (Fin.last m)) : ℝ)) : EReal) := by rw [EReal.coe_add] have h0' : c + dotProduct (y0 - x (Fin.last m)) (xStar (Fin.last m)) ≤ μ0 := by -- Convert the first endpoint bound from `EReal` back to the corresponding real inequality. rw [hrepr] at h0 exact_mod_cast h0 have h1' : c + dotProduct (y1 - x (Fin.last m)) (xStar (Fin.last m)) ≤ μ1 := by -- The second endpoint bound gives the same real inequality at `y1`. rw [hrepr] at h1 exact_mod_cast h1 rw [hrepr] -- The tail term is affine in `y`, so the midpoint estimate reduces to the two endpoint bounds. exact_mod_cast (show c + dotProduct (((1 - b) • y0 + b • y1) - x (Fin.last m)) (xStar (Fin.last m)) ≤ (1 - b) * μ0 + b * μ1 by have htail : dotProduct (((1 - b) • y0 + b • y1) - x (Fin.last m)) (xStar (Fin.last m)) = (1 - b) * dotProduct (y0 - x (Fin.last m)) (xStar (Fin.last m)) + b * dotProduct (y1 - x (Fin.last m)) (xStar (Fin.last m)) := by -- Expand only the affine tail; the finite edge sum stays constant. calc dotProduct (((1 - b) • y0 + b • y1) - x (Fin.last m)) (xStar (Fin.last m)) = dotProduct ((1 - b) • (y0 - x (Fin.last m)) + b • (y1 - x (Fin.last m))) (xStar (Fin.last m)) := by congr 1 ext i simp [Pi.add_apply, Pi.sub_apply, Pi.smul_apply] ring _ = (1 - b) * dotProduct (y0 - x (Fin.last m)) (xStar (Fin.last m)) + b * dotProduct (y1 - x (Fin.last m)) (xStar (Fin.last m)) := by rw [dotProduct_comm, dotProduct_add, dotProduct_smul, dotProduct_smul] simp [smul_eq_mul, dotProduct_comm, add_comm, This simp argument is unused: add_left_comm Hint: Omit it from the simp argument list. simp [smul_eq_mul, dotProduct_comm, add_comm, a̵d̵d̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵add_assoc] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_left_comm, This simp argument is unused: add_assoc Hint: Omit it from the simp argument list. simp [smul_eq_mul, dotProduct_comm, add_comm, add_left_comm,̵ ̵a̵d̵d̵_̵a̵s̵s̵o̵c̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_assoc] rw [htail] have hb0 : 0 ≤ 1 - b := by linarith have h0'' : (1 - b) * (c + dotProduct (y0 - x (Fin.last m)) (xStar (Fin.last m))) ≤ (1 - b) * μ0 := by nlinarith have h1'' : b * (c + dotProduct (y1 - x (Fin.last m)) (xStar (Fin.last m))) ≤ b * μ1 := by nlinarith have hsum := add_le_add h0'' h1'' have hleft : (1 - b) * (c + dotProduct (y0 - x (Fin.last m)) (xStar (Fin.last m))) + b * (c + dotProduct (y1 - x (Fin.last m)) (xStar (Fin.last m))) = c + ((1 - b) * dotProduct (y0 - x (Fin.last m)) (xStar (Fin.last m)) + b * dotProduct (y1 - x (Fin.last m)) (xStar (Fin.last m))) := by ring have hright : (1 - b) * μ0 + b * μ1 = (1 - b) * μ0 + b * μ1 := rfl rw [hleft] at hsum simpa [hright] using hsum)

Helper for Theorem 5.24.11: Rockafellar's raw path-supremum potential is convex because it is the pointwise supremum of the affine-tail functions attached to admissible chains.

lemma helperForTheorem_5_24_11_rockafellarPotential_convex {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} {a : Fin n → ℝ} : ConvexFunction (helperForTheorem_5_24_11_rockafellarPotential ρ a) := by have hconvEpigraph : Convex ℝ (epigraph (Set.univ : Set (Fin n → ℝ)) (helperForTheorem_5_24_11_rockafellarPotential ρ a)) := by intro p hp q hq α b hα hb hab have hαeq : α = 1 - b := by linarith have hb1 : b ≤ 1 := by linarith have hp' : helperForTheorem_5_24_11_rockafellarPotential ρ a p.1 ≤ (p.2 : EReal) := by simpa [epigraph] using hp.2 have hq' : helperForTheorem_5_24_11_rockafellarPotential ρ a q.1 ≤ (q.2 : EReal) := by simpa [epigraph] using hq.2 have hmix : helperForTheorem_5_24_11_rockafellarPotential ρ a ((1 - b) • p.1 + b • q.1) ≤ ((((1 - b) * p.2 + b * q.2 : ℝ)) : EReal) := by -- Route correction: prove convexity directly on the epigraph by bounding each admissible -- chain at the mixed point using the same chain at the two endpoints. dsimp [helperForTheorem_5_24_11_rockafellarPotential] refine sSup_le ?_ intro r hr rcases hr with ⟨m, xChain, xStarChain, hx0, hmem, rfl⟩ have hpChain : helperForTheorem_5_24_11_rockafellarCandidateValue xChain xStarChain p.1 ∈ helperForTheorem_5_24_11_rockafellarCandidateSet ρ a p.1 := by -- Reuse the same chain witness at the first endpoint. exact ⟨m, xChain, xStarChain, hx0, hmem, rfl⟩ have hqChain : helperForTheorem_5_24_11_rockafellarCandidateValue xChain xStarChain q.1 ∈ helperForTheorem_5_24_11_rockafellarCandidateSet ρ a q.1 := by -- The identical chain also belongs to the second endpoint candidate set. exact ⟨m, xChain, xStarChain, hx0, hmem, rfl⟩ have hpBound : helperForTheorem_5_24_11_rockafellarCandidateValue xChain xStarChain p.1 ≤ ((p.2 : ℝ) : EReal) := by -- Endpoint values lie below the corresponding epigraph heights. exact le_trans (le_sSup hpChain) hp' have hqBound : helperForTheorem_5_24_11_rockafellarCandidateValue xChain xStarChain q.1 ≤ ((q.2 : ℝ) : EReal) := by -- The same argument bounds the second endpoint value. exact le_trans (le_sSup hqChain) hq' exact helperForTheorem_5_24_11_candidateValue_convexCombination_realBound xChain xStarChain hb hb1 hpBound hqBound have hmem : (((1 - b) • p.1 + b • q.1), ((1 - b) * p.2 + b * q.2)) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) (helperForTheorem_5_24_11_rockafellarPotential ρ a) := by -- The mixed point sits in the epigraph once the value bound is established. exact epigraph_mem_of_le_aux (S := (Set.univ : Set (Fin n → ℝ))) (x := (1 - b) • p.1 + b • q.1) (μ := (1 - b) * p.2 + b * q.2) (by simp) hmix convert hmem using 1 ext <;> simp [hαeq, smul_eq_mul, mul_comm, This simp argument is unused: mul_left_comm Hint: Omit it from the simp argument list. simp [hαeq, smul_eq_mul, mul_comm, mul_l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵m̵u̵l̵_̵assoc] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`mul_left_comm, This simp argument is unused: mul_assoc Hint: Omit it from the simp argument list. simp [hαeq, smul_eq_mul, mul_comm, mul_left_comm,̵ ̵m̵u̵l̵_̵a̵s̵s̵o̵c̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`mul_assoc] simpa [ConvexFunction] using hconvEpigraph

Helper for Theorem 5.24.11: once the raw potential is known to be proper, every raw subgradient at a graph point survives passage to the closure potential.

lemma helperForTheorem_5_24_11_graphPoint_mem_subdifferential_closurePotential {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} {a aStar x v : Fin n → ℝ} (hρ : IsCyclicallyMonotone ρ) (ha : aStar ∈ ρ a) (hgproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) (helperForTheorem_5_24_11_rockafellarPotential ρ a)) (hv : v ∈ ρ x) : dotProductEquiv ℝ (Fin n) v ∈ subdifferentialAt (convexFunctionClosure (helperForTheorem_5_24_11_rockafellarPotential ρ a)) x := by let g : (Fin n → ℝ) → EReal := helperForTheorem_5_24_11_rockafellarPotential ρ a have hraw := helperForTheorem_5_24_11_graphPoint_mem_subdifferential_rawPotential (ρ := ρ) (a := a) (aStar := aStar) (x := x) (v := v) hρ ha hv dsimp [g] at hraw rcases hraw with ⟨_hupper, _hnotTop, _hnotBot, hsubRaw⟩ have hsubne : Set.Nonempty (subdifferentialAt g x) := by -- The raw subgradient witness makes `x` a subdifferentiable point of `g`. exact ⟨dotProductEquiv ℝ (Fin n) v, hsubRaw⟩ have hclosure := convexFunctionClosure_eq_at_subdifferentiable_point_and_subdifferential_eq g hgproper x hsubne -- Transport the witness through the closure equality of subdifferentials. rw [hclosure.2] exact hsubRaw

Helper for Theorem 5.24.11: in the nonempty-graph branch, Rockafellar's chain-supremum construction should produce a closed proper convex potential whose Euclideanized subdifferential contains Unknown identifier `ρ`ρ pointwise.

lemma helperForTheorem_5_24_11_nonemptyGraph_exists_closedProperConvex_subdifferential_superset {n : ℕ} {ρ : (Fin n → ℝ) → Set (Fin n → ℝ)} (hρ : IsCyclicallyMonotone ρ) (hnonempty : ¬ ∀ x : Fin n → ℝ, ρ x = ∅) : ∃ f : (Fin n → ℝ) → EReal, ClosedConvexFunction f ∧ ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f ∧ ∀ x : Fin n → ℝ, ρ x ⊆ ((dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) := by -- Choose an anchor graph point from the nonempty graph. have hgraphNonempty : ∃ x : Fin n → ℝ, ∃ v : Fin n → ℝ, v ∈ ρ x := by by_contra hgraphEmpty apply hnonempty intro x apply Set.eq_empty_iff_forall_notMem.2 intro v hv exact hgraphEmpty ⟨x, v, hv⟩ rcases hgraphNonempty with ⟨a, aStar, ha⟩ let g : (Fin n → ℝ) → EReal := helperForTheorem_5_24_11_rockafellarPotential ρ a have hgConv : ConvexFunction g := by -- Route correction: instead of revisiting the cycle algebra, use the new fixed-chain affine -- bound to prove convexity of the raw potential directly on its epigraph. simpa [g] using helperForTheorem_5_24_11_rockafellarPotential_convex (ρ := ρ) (a := a) have hanchor := helperForTheorem_5_24_11_graphPoint_mem_subdifferential_rawPotential (ρ := ρ) (a := a) (aStar := aStar) (x := a) (v := aStar) hρ ha ha dsimp [g] at hanchor rcases hanchor with ⟨_hupperA, hnotTopA, hnotBotA, hsubA⟩ have hgproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) g := by -- The anchor subgradient makes the convex raw potential proper by Theorem 23.3. exact helperForTheorem_23_3_proper_of_mem_subdifferential g hgConv a ⟨hnotTopA, hnotBotA⟩ (dotProductEquiv ℝ (Fin n) aStar) hsubA let f : (Fin n → ℝ) → EReal := convexFunctionClosure g have hclosure := (convexFunctionClosure_closed_properConvexFunctionOn_and_agrees_on_ri (f := g) hgproper).1 refine ⟨f, hclosure.1, hclosure.2, ?_⟩ Try this: intro x v hvintro x intro v hv change dotProductEquiv ℝ (Fin n) v ∈ subdifferentialAt f x -- Every graph point of `ρ` is already a raw subgradient, and closure preserves it. simpa [f, g] using helperForTheorem_5_24_11_graphPoint_mem_subdifferential_closurePotential (ρ := ρ) (a := a) (aStar := aStar) (x := x) (v := v) hρ ha hgproper hv
end Section24end Chap05