Convex Analysis (Rockafellar, 1970) -- Chapter 04 -- Section 19 -- Part 6

open scoped BigOperatorsopen scoped Pointwiseopen Topologysection Chap19section Section19

Helper for Corollary 19.1.2: in EReal : TypeEReal, if a nonempty closed set has infimum a finite real value, then that value belongs to the set.

lemma helperForCorollary_19_1_2_mem_of_sInf_eq_real_of_closed
    {S : Set EReal} {r : ℝ}
    (hSnonempty : S.Nonempty)
    (hSclosed : IsClosed S)
    (hsInf_real : sInf S = (r : EReal)) :
    (r : EReal) ∈ S := by
  have hsInf_mem : sInf S ∈ S := IsClosed.sInf_mem hSnonempty hSclosed
  simpa [hsInf_real] using hsInf_mem

Helper for Corollary 19.1.2: extract finite indexed point and ray generator families for the transformed epigraph from IsFinitelyGeneratedConvexSet (n : ℕ) (C : Set (Fin n → ℝ)) : PropIsFinitelyGeneratedConvexSet.

lemma helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph_extractData
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hfg_epi :
      IsFinitelyGeneratedConvexSet (n + 1)
        ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f)) :
    ∃ (k m : ℕ) (p : Fin k → Fin (n + 1) → ℝ) (d : Fin m → Fin (n + 1) → ℝ),
      ((fun q => (prodLinearEquiv_append_coord (n := n)) q) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) =
        mixedConvexHull (n := n + 1) (Set.range p) (Set.range d) := by
  classical
  rcases hfg_epi with ⟨S₀, S₁, hS₀fin, hS₁fin, hEq⟩
  let I₀ : Type := {x : Fin (n + 1) → ℝ // x ∈ S₀}
  let I₁ : Type := {x : Fin (n + 1) → ℝ // x ∈ S₁}
  letI : Fintype I₀ := hS₀fin.fintype
  letI : Fintype I₁ := hS₁fin.fintype
  let e₀ : I₀ ≃ Fin (Fintype.card I₀) := Fintype.equivFin I₀
  let e₁ : I₁ ≃ Fin (Fintype.card I₁) := Fintype.equivFin I₁
  let p : Fin (Fintype.card I₀) → Fin (n + 1) → ℝ :=
    fun i => (e₀.symm i).1
  let d : Fin (Fintype.card I₁) → Fin (n + 1) → ℝ :=
    fun j => (e₁.symm j).1
  have hRangeP : Set.range p = S₀ := by
    ext x
    constructor
    · rintro ⟨i, rfl⟩
      exact (e₀.symm i).2
    · intro hx
      refine ⟨e₀ ⟨x, hx⟩, ?_⟩
      simp [p]
  have hRangeD : Set.range d = S₁ := by
    ext x
    constructor
    · rintro ⟨j, rfl⟩
      exact (e₁.symm j).2
    · intro hx
      refine ⟨e₁ ⟨x, hx⟩, ?_⟩
      simp [d]
  refine ⟨Fintype.card I₀, Fintype.card I₁, p, d, ?_⟩
  simpa [hRangeP, hRangeD] using hEq

Helper for Corollary 19.1.2: from membership in a mixed convex hull generated by finite families, extract fixed-index coefficient functions on those families.

lemma helperForCorollary_19_1_2_exists_fixedCoeffs_of_mem_mixedConvexHull_range
    {n k m : ℕ} (p : Fin k → Fin n → ℝ) (d : Fin m → Fin n → ℝ) {y : Fin n → ℝ}
    (hy : y ∈ mixedConvexHull (n := n) (Set.range p) (Set.range d)) :
    ∃ a : Fin k → ℝ, ∃ b : Fin m → ℝ,
      (∀ i, 0 ≤ a i) ∧
      (∀ j, 0 ≤ b j) ∧
      (∑ i, a i) = 1 ∧
      y = (∑ i, a i • p i) + (∑ j, b j • d j) := by
  classical
  rcases
      exists_strict_mixedConvexCombination_of_mem_mixedConvexHull
        (n := n) (S₀ := Set.range p) (S₁ := Set.range d) (x := y) hy with
    ⟨k', m', p', d', a', b', hp', hd', ha', hb', hsum', hy'⟩
  choose ip hip using hp'
  choose id hid using hd'
  let a : Fin k → ℝ :=
    fun i =>
      Finset.sum (Finset.univ.filter (fun u : Fin k' => ip u = i)) (fun t => a' t)
  let b : Fin m → ℝ :=
    fun j =>
      Finset.sum (Finset.univ.filter (fun u : Fin m' => id u = j)) (fun t => b' t)
  have ha_nonneg : ∀ i, 0 ≤ a i := by
    intro i
    unfold a
    refine Finset.sum_nonneg ?_
    intro t ht
    exact le_of_lt (ha' t)
  have hb_nonneg : ∀ j, 0 ≤ b j := by
    intro j
    unfold b
    refine Finset.sum_nonneg ?_
    intro t ht
    exact le_of_lt (hb' t)
  have hsum_a : (∑ i, a i) = 1 := by
    unfold a
    calc
      (∑ i, Finset.sum (Finset.univ.filter (fun u : Fin k' => ip u = i)) (fun t => a' t))
          = ∑ i, ∑ t, (if ip t = i then a' t else 0) := by
              refine Finset.sum_congr rfl ?_
              intro i hi
              simpa using
                (Finset.sum_filter (s := (Finset.univ : Finset (Fin k')))
                  (p := fun u : Fin k' => ip u = i) (f := fun t : Fin k' => a' t))
      _ = ∑ t, ∑ i, (if ip t = i then a' t else 0) := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [Finset.sum_comm]
      _ = ∑ t, a' t := by
            refine Finset.sum_congr rfl ?_
            intro t ht
            simp
      _ = 1 := hsum'
  have hsum_points :
      (∑ i, a i • p i) = ∑ t, a' t • p (ip t) := by
    unfold a
    calc
      (∑ i,
        (Finset.sum (Finset.univ.filter (fun u : Fin k' => ip u = i)) (fun t => a' t)) • p i)
          = ∑ i, Finset.sum (Finset.univ.filter (fun u : Fin k' => ip u = i))
              (fun t => a' t • p i) := by
              refine Finset.sum_congr rfl ?_
              intro i hi
              simpa using
                (Finset.sum_smul
                  (s := Finset.univ.filter (fun u : Fin k' => ip u = i))
                  (f := fun t : Fin k' => a' t) (x := p i))
      _ = ∑ i, ∑ t, (if ip t = i then a' t • p i else 0) := by
            refine Finset.sum_congr rfl ?_
            intro i hi
            simpa using
              (Finset.sum_filter (s := (Finset.univ : Finset (Fin k')))
                (p := fun u : Fin k' => ip u = i)
                (f := fun t : Fin k' => a' t • p i))
      _ = ∑ t, ∑ i, (if ip t = i then a' t • p i else 0) := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [Finset.sum_comm]
      _ = ∑ t, a' t • p (ip t) := by
            refine Finset.sum_congr rfl ?_
            intro t ht
            simp
  have hsum_dirs :
      (∑ j, b j • d j) = ∑ t, b' t • d (id t) := by
    unfold b
    calc
      (∑ j,
        (Finset.sum (Finset.univ.filter (fun u : Fin m' => id u = j)) (fun t => b' t)) • d j)
          = ∑ j, Finset.sum (Finset.univ.filter (fun u : Fin m' => id u = j))
              (fun t => b' t • d j) := by
              refine Finset.sum_congr rfl ?_
              intro j hj
              simpa using
                (Finset.sum_smul
                  (s := Finset.univ.filter (fun u : Fin m' => id u = j))
                  (f := fun t : Fin m' => b' t) (x := d j))
      _ = ∑ j, ∑ t, (if id t = j then b' t • d j else 0) := by
            refine Finset.sum_congr rfl ?_
            intro j hj
            simpa using
              (Finset.sum_filter (s := (Finset.univ : Finset (Fin m')))
                (p := fun u : Fin m' => id u = j)
                (f := fun t : Fin m' => b' t • d j))
      _ = ∑ t, ∑ j, (if id t = j then b' t • d j else 0) := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [Finset.sum_comm]
      _ = ∑ t, b' t • d (id t) := by
            refine Finset.sum_congr rfl ?_
            intro t ht
            simp
  have hsum_points' :
      (∑ t, a' t • p (ip t)) = (∑ t, a' t • p' t) := by
    refine Finset.sum_congr rfl ?_
    intro t ht
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hip t]
  have hsum_dirs' :
      (∑ t, b' t • d (id t)) = (∑ t, b' t • d' t) := by
    refine Finset.sum_congr rfl ?_
    intro t ht
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hid t]
  refine ⟨a, b, ha_nonneg, hb_nonneg, hsum_a, ?_⟩
  calc
    y = (∑ t, a' t • p' t) + (∑ t, b' t • d' t) := hy'
    _ = (∑ t, a' t • p (ip t)) + (∑ t, b' t • d (id t)) := by
          simp [hsum_points', hsum_dirs']
    _ = (∑ i, a i • p i) + (∑ j, b j • d j) := by
          simp [hsum_points, hsum_dirs]

Helper for Corollary 19.1.2: linear maps send mixed convex hulls generated by finite families to mixed convex hulls generated by the mapped families.

lemma helperForCorollary_19_1_2_linearImage_mixedConvexHull_range
    {n p k m : ℕ}
    (L : (Fin n → ℝ) →ₗ[ℝ] (Fin p → ℝ))
    (pointGen : Fin k → Fin n → ℝ)
    (dirGen : Fin m → Fin n → ℝ) :
    L '' mixedConvexHull (n := n) (Set.range pointGen) (Set.range dirGen) =
      mixedConvexHull (n := p)
        (Set.range (fun i => L (pointGen i)))
        (Set.range (fun j => L (dirGen j))) := by
  ext y
  constructor
  · intro hy
    rcases hy with ⟨x, hx, rfl⟩
    rcases
        helperForCorollary_19_1_2_exists_fixedCoeffs_of_mem_mixedConvexHull_range
          (n := n) (k := k) (m := m) pointGen dirGen hx with
      ⟨a, b, ha_nonneg, hb_nonneg, hsum_a, hx_repr⟩
    have hLx_repr :
        L x = (∑ i, a i • L (pointGen i)) + (∑ j, b j • L (dirGen j)) := by
      calc
        L x = L ((∑ i, a i • pointGen i) + (∑ j, b j • dirGen j)) := by
              try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hx_repr]
        _ = L (∑ i, a i • pointGen i) + L (∑ j, b j • dirGen j) := by
              simp
        _ = (∑ i, a i • L (pointGen i)) + (∑ j, b j • L (dirGen j)) := by
              simp
    exact
      mem_mixedConvexHull_range_of_exists_coeffs
        (n := p) (p := fun i => L (pointGen i)) (d := fun j => L (dirGen j))
        (y := L x) a b ha_nonneg hb_nonneg hsum_a hLx_repr
  · intro hy
    rcases
        helperForCorollary_19_1_2_exists_fixedCoeffs_of_mem_mixedConvexHull_range
          (n := p) (k := k) (m := m)
          (fun i => L (pointGen i))
          (fun j => L (dirGen j)) hy with
      ⟨a, b, ha_nonneg, hb_nonneg, hsum_a, hy_repr⟩
    let x : Fin n → ℝ :=
      (∑ i, a i • pointGen i) + (∑ j, b j • dirGen j)
    have hx_mixed :
        x ∈ mixedConvexHull (n := n) (Set.range pointGen) (Set.range dirGen) :=
      mem_mixedConvexHull_range_of_exists_coeffs
        (n := n) (p := pointGen) (d := dirGen)
        (y := x) a b ha_nonneg hb_nonneg hsum_a rfl
    have hLx : L x = y := by
      calc
        L x = (∑ i, a i • L (pointGen i)) + (∑ j, b j • L (dirGen j)) := by
              simp [x]
        _ = y := by
              try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hy_repr] using hy_repr.symm
    exact ⟨x, hx_mixed, hLx⟩

Helper for Corollary 19.1.2: linear images of finitely generated convex sets remain finitely generated.

lemma helperForCorollary_19_1_2_linearImage_finitelyGeneratedSet
    {n p : ℕ} {C : Set (Fin n → ℝ)}
    (hfg : IsFinitelyGeneratedConvexSet n C)
    (L : (Fin n → ℝ) →ₗ[ℝ] (Fin p → ℝ)) :
    IsFinitelyGeneratedConvexSet p (L '' C) := by
  classical
  rcases hfg with ⟨S₀, S₁, hS₀finite, hS₁finite, hEqC⟩
  let I₀ : Type := {x : Fin n → ℝ // x ∈ S₀}
  let I₁ : Type := {x : Fin n → ℝ // x ∈ S₁}
  letI : Fintype I₀ := hS₀finite.fintype
  letI : Fintype I₁ := hS₁finite.fintype
  let e₀ : I₀ ≃ Fin (Fintype.card I₀) := Fintype.equivFin I₀
  let e₁ : I₁ ≃ Fin (Fintype.card I₁) := Fintype.equivFin I₁
  let pointGen : Fin (Fintype.card I₀) → Fin n → ℝ :=
    fun i => (e₀.symm i).1
  let dirGen : Fin (Fintype.card I₁) → Fin n → ℝ :=
    fun j => (e₁.symm j).1
  have hRangePoint : Set.range pointGen = S₀ := by
    ext x
    constructor
    · rintro ⟨i, rfl⟩
      exact (e₀.symm i).2
    · intro hx
      refine ⟨e₀ ⟨x, hx⟩, ?_⟩
      simp [pointGen]
  have hRangeDir : Set.range dirGen = S₁ := by
    ext x
    constructor
    · rintro ⟨j, rfl⟩
      exact (e₁.symm j).2
    · intro hx
      refine ⟨e₁ ⟨x, hx⟩, ?_⟩
      simp [dirGen]
  have hEqC' :
      C = mixedConvexHull (n := n) (Set.range pointGen) (Set.range dirGen) := by
    simpa [hRangePoint, hRangeDir] using hEqC
  have hImageEq :
      L '' C =
        mixedConvexHull (n := p)
          (Set.range (fun i => L (pointGen i)))
          (Set.range (fun j => L (dirGen j))) := by
    calc
      L '' C =
          L '' mixedConvexHull (n := n) (Set.range pointGen) (Set.range dirGen) := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hEqC']
      _ =
          mixedConvexHull (n := p)
            (Set.range (fun i => L (pointGen i)))
            (Set.range (fun j => L (dirGen j))) :=
            helperForCorollary_19_1_2_linearImage_mixedConvexHull_range
              (n := n) (p := p)
              (k := Fintype.card I₀) (m := Fintype.card I₁)
              L pointGen dirGen
  refine ⟨Set.range (fun i => L (pointGen i)), Set.range (fun j => L (dirGen j)),
    Set.finite_range _, Set.finite_range _, ?_⟩
  exact hImageEq

Helper for Corollary 19.1.2: decode fixed-index mixed-hull coefficients in transformed epigraph coordinates into Text 19.0.10 coefficient data.

lemma helperForCorollary_19_1_2_decode_transformedGeneratorCoeffs_to_Text19_0_10_lam
    {n k' m' : ℕ}
    (p : Fin k' → Fin (n + 1) → ℝ)
    (d : Fin m' → Fin (n + 1) → ℝ)
    {x : Fin n → ℝ} {μ : ℝ}
    {a' : Fin k' → ℝ} {b' : Fin m' → ℝ}
    (ha_nonneg : ∀ i, 0 ≤ a' i)
    (hb_nonneg : ∀ j, 0 ≤ b' j)
    (hsum_a : (∑ i, a' i) = 1)
    (hy_repr :
      (prodLinearEquiv_append_coord (n := n)) (x, μ) =
        (∑ i, a' i • p i) + (∑ j, b' j • d j)) :
    ∃ (lam : Fin (k' + m') → ℝ),
      (∀ j0,
        (∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).1)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).1)
              i) j0) = x j0) ∧
      (Finset.sum (Finset.univ.filter (fun i : Fin (k' + m') => (i : ℕ) < k'))
        (fun i => lam i)) = 1 ∧
      (∀ i, 0 ≤ lam i) ∧
      ((∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).2)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).2)
              i : ℝ)) = μ) := by
  let preP : Fin k' → (Fin n → ℝ) × ℝ :=
    fun i => (prodLinearEquiv_append_coord (n := n)).symm (p i)
  let preD : Fin m' → (Fin n → ℝ) × ℝ :=
    fun j => (prodLinearEquiv_append_coord (n := n)).symm (d j)
  let aDec : Fin (k' + m') → Fin n → ℝ :=
    Fin.append (fun i => (preP i).1) (fun j => (preD j).1)
  let αDec : Fin (k' + m') → ℝ :=
    Fin.append (fun i => (preP i).2) (fun j => (preD j).2)
  let lamDec : Fin (k' + m') → ℝ := Fin.append a' b'
  have hpair :
      (x, μ) =
        (∑ i, a' i • preP i) + (∑ j, b' j • preD j) := by
    have hmap := congrArg (fun y => (prodLinearEquiv_append_coord (n := n)).symm y) hy_repr
    simpa [preP, preD] using hmap
  have hx_repr :
      x = (∑ i, a' i • (preP i).1) + (∑ j, b' j • (preD j).1) := by
    have hfst := congrArg Prod.fst hpair
    simpa [Prod.fst_sum, Prod.smul_fst, smul_eq_mul] using hfst
  have hμ_repr :
      μ = (∑ i, a' i * (preP i).2) + (∑ j, b' j * (preD j).2) := by
    have hsnd := congrArg Prod.snd hpair
    simpa [Prod.snd_sum, Prod.smul_snd, smul_eq_mul] using hsnd
  have hlin : ∀ j0, (∑ i, lamDec i * aDec i j0) = x j0 := by
    intro j0
    have hsplit :
        (∑ i, lamDec i * aDec i j0) =
          (∑ i, a' i * (preP i).1 j0) + (∑ j, b' j * (preD j).1 j0) := by
      calc
        (∑ i, lamDec i * aDec i j0)
            =
              (∑ i : Fin k', lamDec (Fin.castAdd m' i) * aDec (Fin.castAdd m' i) j0) +
                (∑ j : Fin m', lamDec (Fin.natAdd k' j) * aDec (Fin.natAdd k' j) j0) := by
                simpa using
                  (Fin.sum_univ_add
                    (f := fun i : Fin (k' + m') => lamDec i * aDec i j0))
        _ = (∑ i, a' i * (preP i).1 j0) + (∑ j, b' j * (preD j).1 j0) := by
              simp [lamDec, aDec]
    have hxj := congrArg (fun u : Fin n → ℝ => u j0) hx_repr
    calc
      (∑ i, lamDec i * aDec i j0)
          = (∑ i, a' i * (preP i).1 j0) + (∑ j, b' j * (preD j).1 j0) := hsplit
      _ = x j0 := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hxj] using hxj.symm
  have hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin (k' + m') => (i : ℕ) < k'))
        (fun i => lamDec i)) = 1 := by
    rw [helperForCorollary_19_1_2_sum_filter_lt_eq_sum_castAdd
      (k := k') (m := m') (g := lamDec)]
    simpa [lamDec] using hsum_a
  have hnonneg : ∀ i, 0 ≤ lamDec i := by
    intro i
    exact Fin.addCases
      (fun i0 => by
        simpa [lamDec] using ha_nonneg i0)
      (fun j0 => by
        simpa [lamDec] using hb_nonneg j0)
      i
  have hobj : (∑ i, lamDec i * αDec i : ℝ) = μ := by
    have hsplit :
        (∑ i, lamDec i * αDec i : ℝ) =
          (∑ i, a' i * (preP i).2) + (∑ j, b' j * (preD j).2) := by
      calc
        (∑ i, lamDec i * αDec i : ℝ)
            =
              (∑ i : Fin k', lamDec (Fin.castAdd m' i) * αDec (Fin.castAdd m' i)) +
                (∑ j : Fin m', lamDec (Fin.natAdd k' j) * αDec (Fin.natAdd k' j)) := by
                simpa using
                  (Fin.sum_univ_add
                    (f := fun i : Fin (k' + m') => lamDec i * αDec i))
        _ = (∑ i, a' i * (preP i).2) + (∑ j, b' j * (preD j).2) := by
              simp [lamDec, αDec]
    calc
      (∑ i, lamDec i * αDec i : ℝ)
          = (∑ i, a' i * (preP i).2) + (∑ j, b' j * (preD j).2) := hsplit
      _ = μ := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hμ_repr] using hμ_repr.symm
  refine ⟨lamDec, ?_, hnorm, hnonneg, ?_⟩
  · simpa [aDec, preP, preD] using hlin
  · simpa [αDec, preP, preD] using hobj

Helper for Corollary 19.1.2: decode mixed-hull membership in packed transformed-epigraph coordinates into feasible Text 19.0.10 coefficients with an objective value bounded by Unknown identifier `μ`μ.

lemma helperForCorollary_19_1_2_unpack_packGenerators_coeffs_to_Text19_0_10_le
    {n k' m' : ℕ}
    (p : Fin k' → Fin (n + 1) → ℝ)
    (d : Fin m' → Fin (n + 1) → ℝ)
    {x : Fin n → ℝ} {μ : ℝ}
    (hy :
      (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
        mixedConvexHull (n := n + 1) (Set.range p) (Set.range d)) :
    ∃ (lam : Fin (k' + m') → ℝ) (q : ℝ),
      (∀ j0,
        (∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).1)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).1)
              i) j0) = x j0) ∧
      (Finset.sum (Finset.univ.filter (fun i : Fin (k' + m') => (i : ℕ) < k'))
        (fun i => lam i)) = 1 ∧
      (∀ i, 0 ≤ lam i) ∧
      q ≤ μ ∧
      q =
        (∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).2)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).2)
              i : ℝ)) := by
  rcases
      helperForCorollary_19_1_2_exists_fixedCoeffs_of_mem_mixedConvexHull_range
        (n := n + 1) (k := k') (m := m') p d hy with
    ⟨a', b', ha_nonneg, hb_nonneg, hsum_a, hy_repr⟩
  rcases
      helperForCorollary_19_1_2_decode_transformedGeneratorCoeffs_to_Text19_0_10_lam
        (n := n) (k' := k') (m' := m') p d
        (x := x) (μ := μ) (a' := a') (b' := b')
        ha_nonneg hb_nonneg hsum_a hy_repr with
    ⟨lam, hlin, hnorm, hnonneg, hobj⟩
  let q : ℝ :=
    (∑ i,
      lam i *
        (Fin.append
          (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).2)
          (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).2)
          i : ℝ))
  have hq_le : q ≤ μ := by
    have hq_eq : q = μ := by
      simpa [q] using hobj
    exact hq_eq.le
  exact ⟨lam, q, hlin, hnorm, hnonneg, hq_le, rfl⟩

Helper for Corollary 19.1.2: unpack packed transformed-epigraph mixed-hull membership into feasible decoded coefficients with objective value bounded above by Unknown identifier `μ`μ.

lemma helperForCorollary_19_1_2_unpack_packedMembership_to_Text19_0_10_le
    {n k' m' : ℕ}
    (p : Fin k' → Fin (n + 1) → ℝ)
    (d : Fin m' → Fin (n + 1) → ℝ)
    {x : Fin n → ℝ} {μ : ℝ}
    (hy :
      (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
        mixedConvexHull (n := n + 1) (Set.range p) (Set.range d)) :
    ∃ (lam : Fin (k' + m') → ℝ),
      (∀ j0,
        (∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).1)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).1)
              i) j0) = x j0) ∧
      (Finset.sum (Finset.univ.filter (fun i : Fin (k' + m') => (i : ℕ) < k'))
        (fun i => lam i)) = 1 ∧
      (∀ i, 0 ≤ lam i) ∧
      ((∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).2)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).2)
              i : ℝ)) : EReal) ≤ (μ : EReal) := by
  rcases
      helperForCorollary_19_1_2_unpack_packGenerators_coeffs_to_Text19_0_10_le
        (n := n) (k' := k') (m' := m') p d (x := x) (μ := μ) hy with
    ⟨lam, q, hlin, hnorm, hnonneg, hq_le, hq_eq⟩
  refine ⟨lam, hlin, hnorm, hnonneg, ?_⟩
  let β : Fin (k' + m') → ℝ :=
    Fin.append
      (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).2)
      (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).2)
  have hcoe_sum :
      (∑ i, (lam i : EReal) * (β i : EReal)) =
        ((∑ i, lam i * β i : ℝ) : EReal) := by
    classical
    refine Finset.induction_on (Finset.univ : Finset (Fin (k' + m'))) ?_ ?_
    · simp
    · intro x s hx hs
      simp [Finset.sum_insert, hx, hs, EReal.coe_add, EReal.coe_mul]
  have hq_le' : (∑ i, lam i * β i : ℝ) ≤ μ := by
    calc
      (∑ i, lam i * β i : ℝ) = q := by
        simpa [β] using hq_eq.symm
      _ ≤ μ := hq_le
  have hq_leE : ((∑ i, lam i * β i : ℝ) : EReal) ≤ (μ : EReal) := by
    exact_mod_cast hq_le'
  have hgoalE : (∑ i, (lam i : EReal) * (β i : EReal)) ≤ (μ : EReal) := by
    rw [hcoe_sum]
    exact hq_leE
  simpa [β] using hgoalE

Helper for Corollary 19.1.2: feasible decoded Text 19.0.10 coefficients transport to membership in the mixed convex hull generated by transformed epigraph families.

lemma helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph_transport_feasible
    {n k' m' : ℕ}
    (p : Fin k' → Fin (n + 1) → ℝ)
    (d : Fin m' → Fin (n + 1) → ℝ)
    {x : Fin n → ℝ}
    {lam : Fin (k' + m') → ℝ}
    (hlin :
      ∀ j0,
        (∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).1)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).1)
              i) j0) = x j0)
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin (k' + m') => (i : ℕ) < k'))
        (fun i => lam i)) = 1)
    (hnonneg : ∀ i, 0 ≤ lam i) :
    (prodLinearEquiv_append_coord (n := n))
        (x, (∑ i,
          lam i *
            (Fin.append
              (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).2)
              (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).2)
              i : ℝ))) ∈
      mixedConvexHull (n := n + 1) (Set.range p) (Set.range d) := by
  let preP : Fin k' → (Fin n → ℝ) × ℝ :=
    fun i => (prodLinearEquiv_append_coord (n := n)).symm (p i)
  let preD : Fin m' → (Fin n → ℝ) × ℝ :=
    fun j => (prodLinearEquiv_append_coord (n := n)).symm (d j)
  let aDec : Fin (k' + m') → Fin n → ℝ :=
    Fin.append (fun i => (preP i).1) (fun j => (preD j).1)
  let αDec : Fin (k' + m') → ℝ :=
    Fin.append (fun i => (preP i).2) (fun j => (preD j).2)
  let aCoeff : Fin k' → ℝ := fun i => lam (Fin.castAdd m' i)
  let bCoeff : Fin m' → ℝ := fun j => lam (Fin.natAdd k' j)
  have hlin' : ∀ j0, (∑ i, lam i * aDec i j0) = x j0 := by
    intro j0
    simpa [aDec, preP, preD] using hlin j0
  have hsum_a : (∑ i, aCoeff i) = 1 := by
    have hnorm' := hnorm
    rw [helperForCorollary_19_1_2_sum_filter_lt_eq_sum_castAdd
      (k := k') (m := m') (g := lam)] at hnorm'
    simpa [aCoeff] using hnorm'
  have ha_nonneg : ∀ i, 0 ≤ aCoeff i := by
    intro i
    simpa [aCoeff] using hnonneg (Fin.castAdd m' i)
  have hb_nonneg : ∀ j, 0 ≤ bCoeff j := by
    intro j
    simpa [bCoeff] using hnonneg (Fin.natAdd k' j)
  let μ : ℝ := ∑ i, lam i * αDec i
  have hpair :
      (x, μ) =
        (∑ i, aCoeff i • preP i) + (∑ j, bCoeff j • preD j) := by
    apply Prod.ext
    · ext j0
      have hsplit :
          (∑ i, lam i * aDec i j0) =
            (∑ i : Fin k', aCoeff i * (preP i).1 j0) +
              (∑ j : Fin m', bCoeff j * (preD j).1 j0) := by
        calc
          (∑ i, lam i * aDec i j0)
              =
                (∑ i : Fin k', lam (Fin.castAdd m' i) * aDec (Fin.castAdd m' i) j0) +
                  (∑ j : Fin m', lam (Fin.natAdd k' j) * aDec (Fin.natAdd k' j) j0) := by
                  simpa using
                    (Fin.sum_univ_add
                      (f := fun i : Fin (k' + m') => lam i * aDec i j0))
          _ = (∑ i : Fin k', aCoeff i * (preP i).1 j0) +
                (∑ j : Fin m', bCoeff j * (preD j).1 j0) := by
                simp [aCoeff, bCoeff, aDec, preP, preD]
      have hxj : x j0 = (∑ i, lam i * aDec i j0) := by
        try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hlin' j0] using (hlin' j0).symm
      calc
        x j0 = (∑ i, lam i * aDec i j0) := hxj
        _ =
            (∑ i : Fin k', aCoeff i * (preP i).1 j0) +
              (∑ j : Fin m', bCoeff j * (preD j).1 j0) := hsplit
        _ =
            ((
              (∑ i, aCoeff i • preP i) +
                (∑ j, bCoeff j • preD j)).1) j0 := by
              simp [Prod.fst_sum, Prod.smul_fst, smul_eq_mul]
    · have hsplit :
          μ =
            (∑ i : Fin k', aCoeff i * (preP i).2) +
              (∑ j : Fin m', bCoeff j * (preD j).2) := by
        calc
          μ = ∑ i, lam i * αDec i := rfl
          _ =
              (∑ i : Fin k', lam (Fin.castAdd m' i) * αDec (Fin.castAdd m' i)) +
                (∑ j : Fin m', lam (Fin.natAdd k' j) * αDec (Fin.natAdd k' j)) := by
                simpa using
                  (Fin.sum_univ_add
                    (f := fun i : Fin (k' + m') => lam i * αDec i))
          _ =
              (∑ i : Fin k', aCoeff i * (preP i).2) +
                (∑ j : Fin m', bCoeff j * (preD j).2) := by
                simp [aCoeff, bCoeff, αDec, preP, preD]
      calc
        μ =
            (∑ i : Fin k', aCoeff i * (preP i).2) +
              (∑ j : Fin m', bCoeff j * (preD j).2) := hsplit
        _ =
            ((
              (∑ i, aCoeff i • preP i) +
                (∑ j, bCoeff j • preD j)).2) := by
              simp [Prod.snd_sum, Prod.smul_snd, smul_eq_mul]
  have hy_repr :
      (prodLinearEquiv_append_coord (n := n)) (x, μ) =
        (∑ i, aCoeff i • p i) + (∑ j, bCoeff j • d j) := by
    have hmap := congrArg (prodLinearEquiv_append_coord (n := n)) hpair
    simpa [preP, preD] using hmap
  exact
    mem_mixedConvexHull_range_of_exists_coeffs
      (n := n + 1) (p := p) (d := d)
      (y := (prodLinearEquiv_append_coord (n := n)) (x, μ))
      aCoeff bCoeff ha_nonneg hb_nonneg hsum_a hy_repr

Helper for Corollary 19.1.2: unpacking transformed-epigraph finite-generation data into the coefficient representation of Text 19.0.10.

lemma helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hfg_epi :
      IsFinitelyGeneratedConvexSet (n + 1)
        ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f)) :
    ∃ (k m : ℕ) (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ),
      k ≤ m ∧
        ∀ x,
          f x =
            sInf {r : EReal |
              ∃ (lam : Fin m → ℝ),
                (∀ j, (∑ i, lam i * a i j) = x j) ∧
                (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
                  (fun i => lam i)) = 1 ∧
                (∀ i, 0 ≤ lam i) ∧
                r = ((∑ i, lam i * α i : ℝ) : EReal)} := by
  rcases
      helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph_extractData
        (n := n) (f := f) hfg_epi with
    ⟨k', m', p, d, hEq_mixed⟩
  have hEq_mixed' :
      ((fun q => (prodLinearEquiv_append_coord (n := n)) q) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) =
        mixedConvexHull (n := n + 1) (Set.range p) (Set.range d) := hEq_mixed
  clear hEq_mixed
  have hfixedCoeffs :
      ∀ {y : Fin (n + 1) → ℝ},
        y ∈ mixedConvexHull (n := n + 1) (Set.range p) (Set.range d) →
        ∃ a' : Fin k' → ℝ, ∃ b' : Fin m' → ℝ,
          (∀ i, 0 ≤ a' i) ∧
          (∀ j, 0 ≤ b' j) ∧
          (∑ i, a' i) = 1 ∧
          y = (∑ i, a' i • p i) + (∑ j, b' j • d j) := by
    intro y hy
    exact
      helperForCorollary_19_1_2_exists_fixedCoeffs_of_mem_mixedConvexHull_range
        (n := n + 1) (k := k') (m := m') p d hy
  let aDec : Fin (k' + m') → Fin n → ℝ :=
    Fin.append
      (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).1)
      (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).1)
  let αDec : Fin (k' + m') → ℝ :=
    Fin.append
      (fun i => ((prodLinearEquiv_append_coord (n := n)).symm (p i)).2)
      (fun j => ((prodLinearEquiv_append_coord (n := n)).symm (d j)).2)
  refine ⟨k', k' + m', aDec, αDec, Nat.le_add_right k' m', ?_⟩
  intro x
  let Sx : Set EReal :=
    {r : EReal |
      ∃ (lam : Fin (k' + m') → ℝ),
        (∀ j,
          (∑ i, lam i * aDec i j) = x j) ∧
        (Finset.sum (Finset.univ.filter (fun i : Fin (k' + m') => (i : ℕ) < k'))
          (fun i => lam i)) = 1 ∧
        (∀ i, 0 ≤ lam i) ∧
        r = ((∑ i, lam i * αDec i : ℝ) : EReal)}
  have hfx_le_sInf : f x ≤ sInf Sx := by
    refine le_sInf ?_
    intro r hrSx
    rcases hrSx with ⟨lam, hlin, hnorm, hnonneg, hrEq⟩
    let μ : ℝ := ∑ i, lam i * αDec i
    have hmem_mixed :
        (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
          mixedConvexHull (n := n + 1) (Set.range p) (Set.range d) := by
      exact
        helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph_transport_feasible
          (n := n) (k' := k') (m' := m') p d
          (x := x) (lam := lam) hlin hnorm hnonneg
    have hmem_img :
        (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
          ((fun q => (prodLinearEquiv_append_coord (n := n)) q) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
      simpa [hEq_mixed'] using hmem_mixed
    rcases hmem_img with ⟨q, hqepi, hqeq⟩
    have hq_pair : q = (x, μ) := by
      apply (prodLinearEquiv_append_coord (n := n)).injective
      simpa using hqeq
    have hleμ : f x ≤ (μ : EReal) := by
      have hq_le : f q.1 ≤ (q.2 : EReal) := (mem_epigraph_univ_iff (f := f)).1 hqepi
      simpa [hq_pair] using hq_le
    simpa [Sx, μ, hrEq] using hleμ
  have hmem_Sx_of_le_real :
      ∀ {μ : ℝ}, f x ≤ (μ : EReal) → (μ : EReal) ∈ Sx := by
    intro μ hleμ
    have hqepi : (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f :=
      (mem_epigraph_univ_iff (f := f)).2 hleμ
    have hmem_img :
        (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
          ((fun q => (prodLinearEquiv_append_coord (n := n)) q) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
      exact ⟨(x, μ), hqepi, rfl⟩
    have hmem_mixed :
        (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
          mixedConvexHull (n := n + 1) (Set.range p) (Set.range d) := by
      simpa [hEq_mixed'] using hmem_img
    rcases hfixedCoeffs hmem_mixed with
      ⟨a', b', ha_nonneg, hb_nonneg, hsum_a, hy_repr⟩
    rcases
      helperForCorollary_19_1_2_decode_transformedGeneratorCoeffs_to_Text19_0_10_lam
        (n := n) (k' := k') (m' := m') p d
        (x := x) (μ := μ) (a' := a') (b' := b')
        ha_nonneg hb_nonneg hsum_a hy_repr with
      ⟨lam, hlin, hnorm, hnonneg, hobj⟩
    have hlin' : ∀ j, (∑ i, lam i * aDec i j) = x j := by
      simpa [aDec] using hlin
    have hobj' : (∑ i, lam i * αDec i : ℝ) = μ := by
      simpa [αDec] using hobj
    have hobjE : (μ : EReal) = ((∑ i, lam i * αDec i : ℝ) : EReal) := by
      exact congrArg (fun t : ℝ => (t : EReal)) hobj'.symm
    exact ⟨lam, hlin', hnorm, hnonneg, hobjE⟩
  have hsInf_le_fx : sInf Sx ≤ f x := by
    by_cases htop : f x = ⊤
    · try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [htop] using (le_top : sInf Sx ≤ (⊤ : EReal))
    · by_cases hbot : f x = ⊥
      · have hforall_real_mem : ∀ z : ℝ, (z : EReal) ∈ Sx := by
          intro z
          have hle : f x ≤ (z : EReal) := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hbot] using (EReal.bot_lt_coe z).le
          exact hmem_Sx_of_le_real (μ := z) hle
        have hforall_real_le : ∀ z : ℝ, sInf Sx ≤ (z : EReal) := by
          intro z
          exact sInf_le (hforall_real_mem z)
        have hle_bot : sInf Sx ≤ (⊥ : EReal) := by
          exact
            (EReal.le_of_forall_lt_iff_le (x := (⊥ : EReal)) (y := sInf Sx)).1
              (by
                intro z hz
                exact hforall_real_le z)
        simpa [hbot] using hle_bot
      · let r : ℝ := (f x).toReal
        have hrfx : f x = (r : EReal) := by
          have hcoe : ((f x).toReal : EReal) = f x :=
            EReal.coe_toReal htop hbot
          simpa [r] using hcoe.symm
        have hr_mem : (r : EReal) ∈ Sx := by
          have hle : f x ≤ (r : EReal) := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hrfx]
          exact hmem_Sx_of_le_real (μ := r) hle
        have hsInf_le_r : sInf Sx ≤ (r : EReal) := sInf_le hr_mem
        simpa [hrfx] using hsInf_le_r
  exact le_antisymm hfx_le_sInf hsInf_le_fx

Helper for Corollary 19.1.2: finite-generation of the transformed epigraph induces finite-generation of the function representation.

lemma helperForCorollary_19_1_2_finitelyGeneratedFunction_of_epigraphFG
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hconv : ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f)
    (hfg_epi :
      IsFinitelyGeneratedConvexSet (n + 1)
        ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f)) :
    IsFinitelyGeneratedConvexFunction n f :=
  by
    have hfpoly : IsPolyhedralConvexFunction n f :=
      helperForCorollary_19_1_2_polyhedralFunction_of_epigraphFG
        (n := n) (f := f) hconv hfg_epi
    have hconv_from_poly : ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f := hfpoly.1
    rcases
      helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph
        (n := n) (f := f) hfg_epi with
      ⟨k, m, a, α, hk, hrepr⟩
    exact ⟨hconv_from_poly, ⟨k, m, a, α, hk, hrepr⟩⟩

Helper for Corollary 19.1.2: finite-generation of the function representation induces finite-generation of the transformed epigraph.

lemma helperForCorollary_19_1_2_epigraphFG_of_finitelyGeneratedFunction
    {n : ℕ} {f : (Fin n → ℝ) → EReal} :
    IsFinitelyGeneratedConvexFunction n f →
      IsFinitelyGeneratedConvexSet (n + 1)
        ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) :=
  by
    intro hfgen
    rcases
      helperForCorollary_19_1_2_unpack_finitelyGeneratedData
        (n := n) (f := f) hfgen with
      ⟨k, m, a, α, hk, hrepr⟩
    exact
      helperForCorollary_19_1_2_pack_transformedEpigraph_from_functionRepresentation
        (n := n) (k := k) (m := m) (f := f) (a := a) (α := α) hk hrepr

Helper for Corollary 19.1.2: polyhedral convex functions are finitely generated.

lemma helperForCorollary_19_1_2_polyhedral_imp_finitelyGenerated
    {n : ℕ} {f : (Fin n → ℝ) → EReal} :
    IsPolyhedralConvexFunction n f → IsFinitelyGeneratedConvexFunction n f := by
  intro hfpoly
  let C : Set (Fin (n + 1) → ℝ) :=
    ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
      epigraph (Set.univ : Set (Fin n → ℝ)) f)
  have hpolyC : IsPolyhedralConvexSet (n + 1) C := by
    simpa [C, prodLinearEquiv_append_coord] using hfpoly.2
  have hconvC : Convex ℝ C :=
    helperForTheorem_19_1_polyhedral_isConvex (n := n + 1) (C := C) hpolyC
  have hTFAE :
      [IsPolyhedralConvexSet (n + 1) C,
          (IsClosed C ∧ {C' : Set (Fin (n + 1) → ℝ) | IsFace (𝕜 := ℝ) C C'}.Finite),
        IsFinitelyGeneratedConvexSet (n + 1) C].TFAE :=
    polyhedral_closed_finiteFaces_finitelyGenerated_equiv (n := n + 1) (C := C) hconvC
  have hfgC : IsFinitelyGeneratedConvexSet (n + 1) C :=
    (hTFAE.out 0 2).1 hpolyC
  exact
    helperForCorollary_19_1_2_finitelyGeneratedFunction_of_epigraphFG
      (n := n) (f := f) hfpoly.1 (by simpa [C] using hfgC)

Helper for Corollary 19.1.2: finitely generated convex functions are polyhedral.

lemma helperForCorollary_19_1_2_finitelyGenerated_imp_polyhedral
    {n : ℕ} {f : (Fin n → ℝ) → EReal} :
    IsFinitelyGeneratedConvexFunction n f → IsPolyhedralConvexFunction n f := by
  intro hfgen
  let C : Set (Fin (n + 1) → ℝ) :=
    ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
      epigraph (Set.univ : Set (Fin n → ℝ)) f)
  have hconv_epi : Convex ℝ (epigraph (Set.univ : Set (Fin n → ℝ)) f) :=
    convex_epigraph_of_convexFunctionOn (f := f) (hf := hfgen.1)
  have hconvC : Convex ℝ C := by
    simpa [C] using
      hconv_epi.linear_image (prodLinearEquiv_append_coord (n := n)).toLinearMap
  have hTFAE :
      [IsPolyhedralConvexSet (n + 1) C,
          (IsClosed C ∧ {C' : Set (Fin (n + 1) → ℝ) | IsFace (𝕜 := ℝ) C C'}.Finite),
        IsFinitelyGeneratedConvexSet (n + 1) C].TFAE :=
    polyhedral_closed_finiteFaces_finitelyGenerated_equiv (n := n + 1) (C := C) hconvC
  have hfgC : IsFinitelyGeneratedConvexSet (n + 1) C :=
    helperForCorollary_19_1_2_epigraphFG_of_finitelyGeneratedFunction
      (n := n) (f := f) hfgen
  have hpolyC : IsPolyhedralConvexSet (n + 1) C :=
    (hTFAE.out 2 0).1 hfgC
  have hpoly_append :
      IsPolyhedralConvexSet (n + 1)
        ((fun p => (prodLinearEquiv_append (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
    simpa [C, prodLinearEquiv_append_coord] using hpolyC
  exact ⟨hfgen.1, hpoly_append⟩

Helper for Corollary 19.1.2: a proper polyhedral convex function is closed.

lemma helperForCorollary_19_1_2_closed_of_polyhedral_proper
    {n : ℕ} {f : (Fin n → ℝ) → EReal} :
    IsPolyhedralConvexFunction n f →
      ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f →
      ClosedConvexFunction f := by
  intro hfpoly hfproper
  have hclosed_transformedEpigraph :
      IsClosed
        ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
    exact
      (helperForTheorem_19_1_polyhedral_imp_closed_finiteFaces
        (n := n + 1)
        (C := ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f))
        (by
          simpa [prodLinearEquiv_append_coord] using hfpoly.2)).1
  let hhome :=
    ((prodLinearEquiv_append_coord (n := n)).toAffineEquiv).toHomeomorphOfFiniteDimensional
  have hclosed_epigraph :
      IsClosed (epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
    have hclosed_image_homeomorph :
        IsClosed
          ((hhome : ((Fin n → ℝ) × ℝ) → (Fin (n + 1) → ℝ)) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
      simpa [hhome, AffineEquiv.coe_toHomeomorphOfFiniteDimensional] using
        hclosed_transformedEpigraph
    exact
      (hhome.isClosed_image (s := epigraph (Set.univ : Set (Fin n → ℝ)) f)).1
        hclosed_image_homeomorph
  have hclosed_sublevel :
      ∀ α : ℝ, IsClosed {x : Fin n → ℝ | f x ≤ (α : EReal)} :=
    (lowerSemicontinuous_iff_closed_sublevel_iff_closed_epigraph
      (f := f)).2.mpr hclosed_epigraph
  have hlsc : LowerSemicontinuous f :=
    (lowerSemicontinuous_iff_closed_sublevel_iff_closed_epigraph
      (f := f)).1.mpr hclosed_sublevel
  exact
    (properConvexFunction_closed_iff_lowerSemicontinuous
      (f := f) hfproper).2 hlsc

Helper for Corollary 19.1.2: an EReal : TypeEReal infimum equal to a finite real value cannot come from the empty set.

lemma helperForCorollary_19_1_2_nonempty_of_sInf_eq_real
    {S : Set EReal} {r : ℝ} (hr : sInf S = (r : EReal)) :
    S.Nonempty := by
  by_contra hSempty
  have hS : S = (∅ : Set EReal) := (Set.not_nonempty_iff_eq_empty).1 hSempty
  have hsInfTop : sInf S = (⊤ : EReal) := by
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hS] using (sInf_empty : sInf (∅ : Set EReal) = (⊤ : EReal))
  have hrtop : (r : EReal) = (⊤ : EReal) := by
    calc
      (r : EReal) = sInf S := by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hr]
      _ = (⊤ : EReal) := hsInfTop
  exact (EReal.coe_ne_top r) hrtop

end Section19end Chap19