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

open scoped BigOperatorsopen scoped Pointwiseopen Topologysection Chap19section Section19

Helper for Theorem 19.1: cones generated by finite sets are polyhedral.

lemma helperForTheorem_19_1_cone_polyhedral_of_finite_generators
    {m : ℕ} {T : Set (Fin m → ℝ)} (hT : Set.Finite T) :
    IsPolyhedralConvexSet m (cone m T) := by
  classical
  by_cases hTne : T.Nonempty
  ·
    let P : Set (Fin m → ℝ) :=
      {xStar : Fin m → ℝ | ∀ x ∈ cone m T, dotProduct x xStar ≤ 0}
    have hP_eq :
        P = ⋂ t ∈ T, closedHalfSpaceLE m t 0 := by
      simpa [P] using
        (helperForTheorem_19_1_cone_polar_eq_iInter_halfspaces (m := m) (T := T))
    have hP_poly : IsPolyhedralConvexSet m P := by
      let ι : Type := {t : Fin m → ℝ // t ∈ T}
      have hfin : Fintype ι := hT.fintype
      refine ⟨ι, hfin, (fun i : ι => i.1), (fun _ => (0 : ℝ)), ?_⟩
      have hP_eq' :
          P = ⋂ i : ι, closedHalfSpaceLE m i.1 0 := by
        have hrewrite :
            (⋂ i : ι, closedHalfSpaceLE m i.1 0) =
              ⋂ t ∈ T, closedHalfSpaceLE m t 0 :=
          Set.iInter_subtype (p := fun t : Fin m → ℝ => t ∈ T)
            (s := fun i : ι => closedHalfSpaceLE m i.1 0)
        calc
          P = ⋂ t ∈ T, closedHalfSpaceLE m t 0 := hP_eq
          _ = ⋂ i : ι, closedHalfSpaceLE m i.1 0 := hrewrite.symm
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hP_eq'] using hP_eq'
    have hP_conv : Convex ℝ P :=
      helperForTheorem_19_1_polyhedral_isConvex (n := m) (C := P) hP_poly
    have hP_gen : IsFinitelyGeneratedConvexSet m P :=
      (helperForTheorem_19_1_closed_finiteFaces_imp_finitelyGenerated (n := m) (C := P) hP_conv)
        (helperForTheorem_19_1_polyhedral_imp_closed_finiteFaces (n := m) (C := P) hP_poly)
    rcases hP_gen with ⟨S₀, S₁, hS₀fin, hS₁fin, hP_mixed⟩
    have h0mem : (0 : Fin m → ℝ) ∈ P := by
      refine Set.mem_setOf.2 ?_
      intro x hx
      simp
    have h0mem_mixed :
        (0 : Fin m → ℝ) ∈ mixedConvexHull (n := m) S₀ S₁ := by
      simpa [hP_mixed] using h0mem
    have hS₀ne : S₀.Nonempty := by
      by_contra hS₀ne
      have hS₀empty : S₀ = (∅ : Set (Fin m → ℝ)) :=
        (Set.not_nonempty_iff_eq_empty).1 hS₀ne
      have hmix_empty :
          mixedConvexHull (n := m) S₀ S₁ = (∅ : Set (Fin m → ℝ)) := by
        simpa [hS₀empty] using (mixedConvexHull_empty_points (n := m) (S₁ := S₁))
      have : (0 : Fin m → ℝ) ∈ (∅ : Set (Fin m → ℝ)) := by
        Try `simp at h0mem_mixed` instead of `simpa using h0mem_mixed`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hmix_empty] using h0mem_mixed
      exact (Set.notMem_empty (0 : Fin m → ℝ)) this
    have hpolar_P :
        {xStar : Fin m → ℝ | ∀ x ∈ P, dotProduct x xStar ≤ 0} =
          (⋂ s ∈ S₀, closedHalfSpaceLE m s 0) ∩
            (⋂ d ∈ S₁, closedHalfSpaceLE m d 0) := by
      have hpolar_mixed :
          {xStar : Fin m → ℝ |
              ∀ x ∈ mixedConvexHull (n := m) S₀ S₁, dotProduct x xStar ≤ 0} =
            (⋂ s ∈ S₀, closedHalfSpaceLE m s 0) ∩
              (⋂ d ∈ S₁, closedHalfSpaceLE m d 0) :=
        helperForTheorem_19_1_polar_of_mixedConvexHull_eq_iInter
          (n := m) (S₀ := S₀) (S₁ := S₁) hS₀ne
      simpa [hP_mixed] using hpolar_mixed
    have hS₀_poly : IsPolyhedralConvexSet m (⋂ s ∈ S₀, closedHalfSpaceLE m s 0) := by
      let ι0 : Type := {s : Fin m → ℝ // s ∈ S₀}
      have hfin0 : Fintype ι0 := hS₀fin.fintype
      refine ⟨ι0, hfin0, (fun i : ι0 => i.1), (fun _ => (0 : ℝ)), ?_⟩
      have hrewrite :
          (⋂ i : ι0, closedHalfSpaceLE m i.1 0) =
            ⋂ s ∈ S₀, closedHalfSpaceLE m s 0 :=
        Set.iInter_subtype (p := fun s : Fin m → ℝ => s ∈ S₀)
          (s := fun i : ι0 => closedHalfSpaceLE m i.1 0)
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hrewrite] using hrewrite.symm
    have hS₁_poly : IsPolyhedralConvexSet m (⋂ d ∈ S₁, closedHalfSpaceLE m d 0) := by
      let ι1 : Type := {d : Fin m → ℝ // d ∈ S₁}
      have hfin1 : Fintype ι1 := hS₁fin.fintype
      refine ⟨ι1, hfin1, (fun i : ι1 => i.1), (fun _ => (0 : ℝ)), ?_⟩
      have hrewrite :
          (⋂ i : ι1, closedHalfSpaceLE m i.1 0) =
            ⋂ d ∈ S₁, closedHalfSpaceLE m d 0 :=
        Set.iInter_subtype (p := fun d : Fin m → ℝ => d ∈ S₁)
          (s := fun i : ι1 => closedHalfSpaceLE m i.1 0)
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hrewrite] using hrewrite.symm
    have hpolar_poly :
        IsPolyhedralConvexSet m
          ((⋂ s ∈ S₀, closedHalfSpaceLE m s 0) ∩
            (⋂ d ∈ S₁, closedHalfSpaceLE m d 0)) :=
      helperForTheorem_19_1_polyhedral_inter hS₀_poly hS₁_poly
    have hpolar_poly' :
        IsPolyhedralConvexSet m {xStar : Fin m → ℝ | ∀ x ∈ P, dotProduct x xStar ≤ 0} := by
      simpa [hpolar_P] using hpolar_poly
    have hcone : IsConvexCone m (cone m T) := by
      have hcone' : IsConvexCone m (convexConeGenerated m T) :=
        isConvexCone_convexConeGenerated (n := m) (S₁ := T)
      simpa [cone_eq_convexConeGenerated (n := m) (S₁ := T)] using hcone'
    have hsmul :
        ∀ ⦃c : ℝ⦄, 0 < c → ∀ ⦃x : Fin m → ℝ⦄, x ∈ cone m T → c • x ∈ cone m T := by
      intro c hc x hx
      exact hcone.1 x hx c hc
    have hadd :
        ∀ ⦃x : Fin m → ℝ⦄, x ∈ cone m T →
          ∀ ⦃y : Fin m → ℝ⦄, y ∈ cone m T → x + y ∈ cone m T := by
      intro x hx y hy
      exact isConvexCone_add_closed m (cone m T) hcone x hx y hy
    set K : ConvexCone ℝ (Fin m → ℝ) :=
      { carrier := cone m T, smul_mem' := hsmul, add_mem' := hadd } with hK
    have h0ray : (0 : Fin m → ℝ) ∈ ray m T := by
      change (0 : Fin m → ℝ) ∈ Set.insert 0 (rayNonneg m T)
      exact (Set.mem_insert_iff).2 (Or.inl rfl)
    have h0cone : (0 : Fin m → ℝ) ∈ cone m T := by
      have h0conv : (0 : Fin m → ℝ) ∈ conv (ray m T) :=
        (subset_convexHull (𝕜 := ℝ) (s := ray m T)) h0ray
      simpa [cone, conv] using h0conv
    have hKne : (K : Set (Fin m → ℝ)).Nonempty := by
      refine ⟨0, ?_⟩
      simpa [hK] using h0cone
    have hpolarpolar :
        {xStar : Fin m → ℝ |
            ∀ x ∈ {z : Fin m → ℝ | ∀ x ∈ (K : Set (Fin m → ℝ)), dotProduct x z ≤ 0},
              dotProduct x xStar ≤ 0} =
          closure (K : Set (Fin m → ℝ)) :=
      section16_polar_polar_eq_closure_convexCone (K := K) hKne
    have hpolarpolar' :
        {xStar : Fin m → ℝ | ∀ x ∈ P, dotProduct x xStar ≤ 0} =
          closure (cone m T) := by
      simpa [P, hK] using hpolarpolar
    have hclosed_cone : IsClosed (cone m T) :=
      helperForTheorem_19_1_isClosed_cone_of_finite_generators (m := m) (T := T) hT
    have hpolarpolar'' :
        {xStar : Fin m → ℝ | ∀ x ∈ P, dotProduct x xStar ≤ 0} =
          cone m T := by
      simpa [hclosed_cone.closure_eq] using hpolarpolar'
    simpa [hpolarpolar''] using hpolar_poly'
  ·
    have hTempty : T = (∅ : Set (Fin m → ℝ)) :=
      (Set.not_nonempty_iff_eq_empty).1 hTne
    subst hTempty
    have hcone : cone m (∅ : Set (Fin m → ℝ)) = ({0} : Set (Fin m → ℝ)) := by
      have hrayNonneg : rayNonneg m (∅ : Set (Fin m → ℝ)) = (∅ : Set (Fin m → ℝ)) := by
        ext x
        simp [rayNonneg]
      have hray : ray m (∅ : Set (Fin m → ℝ)) = ({0} : Set (Fin m → ℝ)) := by
        ext x
        constructor
        · intro hx
          have hx'' :
              x ∈ Set.insert (0 : Fin m → ℝ) (rayNonneg m (∅ : Set (Fin m → ℝ))) := by
            simpa [ray] using hx
          have hx''' : x = 0 ∨ x ∈ rayNonneg m (∅ : Set (Fin m → ℝ)) :=
            (Set.mem_insert_iff).1 hx''
          have hx' : x = 0 ∨ x ∈ (∅ : Set (Fin m → ℝ)) := by
            simpa [hrayNonneg] using hx'''
          cases hx' with
          | inl hx0 => try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hx0]
          | inr hxempty => exact (Set.notMem_empty x hxempty).elim
        · intro hx
          have hx0 : x = 0 := by
            simpa [Set.mem_singleton_iff] using hx
          have hx' : x = 0 ∨ x ∈ (∅ : Set (Fin m → ℝ)) := by
            left
            exact hx0
          have hx'' : x = 0 ∨ x ∈ rayNonneg m (∅ : Set (Fin m → ℝ)) := by
            simpa [hrayNonneg] using hx'
          have hxmem :
              x ∈ Set.insert (0 : Fin m → ℝ) (rayNonneg m (∅ : Set (Fin m → ℝ))) :=
            (Set.mem_insert_iff).2 hx''
          simpa [ray] using hxmem
      calc
        cone m (∅ : Set (Fin m → ℝ)) = conv (ray m (∅ : Set (Fin m → ℝ))) := rfl
        _ = conv ({0} : Set (Fin m → ℝ)) := by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hray]
        _ = ({0} : Set (Fin m → ℝ)) := by
          simp [conv]
    simpa [hcone] using (helperForTheorem_19_1_zero_set_polyhedral (m := m))

Helper for Theorem 19.1: mixed convex hull of finitely many generators is polyhedral.

lemma helperForTheorem_19_1_mixedConvexHull_polyhedral_of_finite_generators
    {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hS₀ : Set.Finite S₀) (hS₁ : Set.Finite S₁) :
    IsPolyhedralConvexSet n (mixedConvexHull (n := n) S₀ S₁) := by
  classical
  have hlift :
      Set.Finite (liftingSet (n := n) S₀ S₁) := by
    have hS₀' :
        Set.Finite
          ((fun x : Fin n → ℝ =>
              (Fin.cases (1 : ℝ) x : Fin (n + 1) → ℝ)) '' S₀) := by
      exact
        hS₀.image
          (fun x : Fin n → ℝ => (Fin.cases (1 : ℝ) x : Fin (n + 1) → ℝ))
    have hS₁' :
        Set.Finite
          ((fun x : Fin n → ℝ =>
              (Fin.cases (0 : ℝ) x : Fin (n + 1) → ℝ)) '' S₁) := by
      exact
        hS₁.image
          (fun x : Fin n → ℝ => (Fin.cases (0 : ℝ) x : Fin (n + 1) → ℝ))
    have hfinite :
        Set.Finite
          (((fun x : Fin n → ℝ =>
                (Fin.cases (1 : ℝ) x : Fin (n + 1) → ℝ)) '' S₀) ∪
            ((fun x : Fin n → ℝ =>
                (Fin.cases (0 : ℝ) x : Fin (n + 1) → ℝ)) '' S₁)) := by
      exact hS₀'.union hS₁'
    simpa [liftingSet] using hfinite
  have hcone :
      IsPolyhedralConvexSet (n + 1) (liftingCone (n := n) S₀ S₁) := by
    have hcone' :
        IsPolyhedralConvexSet (n + 1) (cone (n + 1) (liftingSet (n := n) S₀ S₁)) := by
      exact
        helperForTheorem_19_1_cone_polyhedral_of_finite_generators
          (m := n + 1) (T := liftingSet (n := n) S₀ S₁) hlift
    simpa [liftingCone] using hcone'
  have hhyper : IsPolyhedralConvexSet (n + 1) (liftingHyperplane n) :=
    helperForTheorem_19_1_liftingHyperplane_polyhedral n
  have hinter :
      IsPolyhedralConvexSet (n + 1)
        (liftingCone (n := n) S₀ S₁ ∩ liftingHyperplane n) :=
    helperForTheorem_19_1_polyhedral_inter hcone hhyper
  have hpre :
      IsPolyhedralConvexSet n
        {x : Fin n → ℝ |
          (Fin.cases (1 : ℝ) x) ∈
            (liftingCone (n := n) S₀ S₁ ∩ liftingHyperplane n)} :=
    helperForTheorem_19_1_lift_preimage_polyhedral (n := n)
      (K := liftingCone (n := n) S₀ S₁ ∩ liftingHyperplane n) hinter
  have hEq :
      {x : Fin n → ℝ |
          (Fin.cases (1 : ℝ) x) ∈ liftingCone (n := n) S₀ S₁ ∧
          (Fin.cases (1 : ℝ) x) ∈ liftingHyperplane n} =
        mixedConvexHull (n := n) S₀ S₁ := by
    ext x
    constructor
    · intro hx
      have hx' :
          (Fin.cases (1 : ℝ) x) ∈
            (liftingCone (n := n) S₀ S₁ ∩ liftingHyperplane n) := by
        exact hx
      exact
        (mem_mixedConvexHull_iff_lift_mem_liftingCone_inter_liftingHyperplane (n := n)
            (S₀ := S₀) (S₁' := S₁) (x := x)).2 hx'
    · intro hx
      have hx' :=
        (mem_mixedConvexHull_iff_lift_mem_liftingCone_inter_liftingHyperplane (n := n)
            (S₀ := S₀) (S₁' := S₁) (x := x)).1 hx
      exact hx'
  simpa [hEq, Set.mem_inter] using hpre

Helper for Theorem 19.1: finitely generated convex sets are polyhedral.

lemma helperForTheorem_19_1_finitelyGenerated_imp_polyhedral
    {n : ℕ} {C : Set (Fin n → ℝ)} (unused variable `hc`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hc : Convex ℝ C) :
    IsFinitelyGeneratedConvexSet n C → IsPolyhedralConvexSet n C := by
  intro hgen
  rcases hgen with ⟨S₀, S₁, hS₀finite, hS₁finite, hEq⟩
  have hpoly :
      IsPolyhedralConvexSet n (mixedConvexHull (n := n) S₀ S₁) := by
    exact
      helperForTheorem_19_1_mixedConvexHull_polyhedral_of_finite_generators
        (n := n) (S₀ := S₀) (S₁ := S₁) hS₀finite hS₁finite
  simpa [hEq] using hpoly

Theorem 19.1: The following properties of a convex set Unknown identifier `C`C are equivalent: (a) Unknown identifier `C`C is polyhedral; (b) Unknown identifier `C`C is closed and has only finitely many faces; (c) Unknown identifier `C`C is finitely generated.

theorem polyhedral_closed_finiteFaces_finitelyGenerated_equiv
    {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) :
    [IsPolyhedralConvexSet n C,
        (IsClosed C ∧ {C' : Set (Fin n → ℝ) | IsFace (𝕜 := ℝ) C C'}.Finite),
      IsFinitelyGeneratedConvexSet n C].TFAE := by
  classical
  refine List.tfae_of_cycle ?_ ?_
  ·
    refine List.IsChain.cons_cons ?_ ?_
    · intro hpoly
      exact helperForTheorem_19_1_polyhedral_imp_closed_finiteFaces (n := n) (C := C) hpoly
    ·
      refine List.IsChain.cons_cons ?_ ?_
      · intro hclosed
        exact
          helperForTheorem_19_1_closed_finiteFaces_imp_finitelyGenerated (n := n) (C := C) hc
            hclosed
      · exact List.IsChain.singleton _
  · intro hgen
    exact helperForTheorem_19_1_finitelyGenerated_imp_polyhedral (n := n) (C := C) hc hgen

Helper for Corollary 19.1.1: positive multiples preserve IsDirectionOf.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C' : Set E) (d : E) : PropIsDirectionOf.

lemma helperForCorollary_19_1_1_isDirectionOf_posMul
    {n : ℕ} {C' : Set (Fin n → ℝ)} {d : Fin n → ℝ}
    (hd : IsDirectionOf (𝕜 := ℝ) C' d) {t : ℝ} (ht : 0 < t) :
    IsDirectionOf (𝕜 := ℝ) C' (t • d) := by
  rcases hd with ⟨x, hdne, hC'⟩
  have htne : t ≠ 0 := ne_of_gt ht
  refine ⟨x, ?_, ?_⟩
  · intro hzero
    have hzero' := smul_eq_zero.mp hzero
    cases hzero' with
    | inl ht0 => exact htne ht0
    | inr hd0 => exact hdne hd0
  ·
    apply Set.Subset.antisymm
    · intro y hy
      have hy' : y ∈ (fun s : ℝ => x + s • d) '' Set.Ici (0 : ℝ) := by
        simpa [hC'] using hy
      rcases hy' with ⟨u, hu, rfl⟩
      have hnonneg : 0 ≤ u / t := by
        exact div_nonneg hu (le_of_lt ht)
      refine ⟨u / t, hnonneg, ?_⟩
      calc
        x + (u / t) • (t • d)
            = x + (u * t⁻¹) • (t • d) := by
                simp [div_eq_mul_inv]
        _ = x + ((u * t⁻¹) * t) • d := by
              simp [smul_smul, mul_comm]
        _ = x + u • d := by
              simp [htne]
    · intro y hy
      rcases hy with ⟨s, hs, rfl⟩
      have hs' : 0 ≤ s * t := mul_nonneg hs (le_of_lt ht)
      have hmem :
          x + (s * t) • d ∈ (fun u : ℝ => x + u • d) '' Set.Ici (0 : ℝ) := by
        exact ⟨s * t, hs', rfl⟩
      have hcalc : x + s • (t • d) = x + (s * t) • d := by
        simp [smul_smul, mul_comm]
      have hmem' :
          x + s • (t • d) ∈ (fun u : ℝ => x + u • d) '' Set.Ici (0 : ℝ) := by
        simpa [hcalc] using hmem
      simpa [hC'] using hmem'

Helper for Corollary 19.1.1: positive multiples of an extreme direction are extreme directions.

lemma helperForCorollary_19_1_1_extremeDirection_posMul_closed
    {n : ℕ} {C : Set (Fin n → ℝ)} {d : Fin n → ℝ}
    (hd : IsExtremeDirection (𝕜 := ℝ) C d) {t : ℝ} (ht : 0 < t) :
    IsExtremeDirection (𝕜 := ℝ) C (t • d) := by
  rcases hd with ⟨C', hhalf, hdir⟩
  refine ⟨C', hhalf, ?_⟩
  exact
    helperForCorollary_19_1_1_isDirectionOf_posMul (C' := C') (d := d) hdir ht

Helper for Corollary 19.1.1: extreme directions are nonzero.

lemma helperForCorollary_19_1_1_extremeDirection_ne_zero
    {n : ℕ} {C : Set (Fin n → ℝ)} {d : Fin n → ℝ}
    (hd : IsExtremeDirection (𝕜 := ℝ) C d) : d ≠ 0 := by
  rcases hd with ⟨C', hhalf, hdir⟩
  rcases hdir with ⟨x, hdne, hC'⟩
  exact hdne

Helper for Corollary 19.1.1: if any extreme direction exists, then there are infinitely many extreme-direction vectors.

lemma helperForCorollary_19_1_1_infinite_extremeDirections_of_exists
    {n : ℕ} {C : Set (Fin n → ℝ)} :
    (∃ d : Fin n → ℝ, IsExtremeDirection (𝕜 := ℝ) C d) →
      Set.Infinite {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} := by
  classical
  intro hex
  rcases hex with ⟨d, hd⟩
  let f : ℕ → Fin n → ℝ := fun k => ((k : ℝ) + 1) • d
  have hdne : d ≠ 0 :=
    helperForCorollary_19_1_1_extremeDirection_ne_zero (C := C) hd
  have hinj : Function.Injective f := by
    intro m n hmn
    have hinj' : Function.Injective (fun t : ℝ => t • d) :=
      smul_left_injective ℝ (x := d) hdne
    have hmn' : ((m : ℝ) + 1) • d = ((n : ℝ) + 1) • d := by
      simpa [f] using hmn
    have h' : ((m : ℝ) + 1) = ((n : ℝ) + 1) := hinj' hmn'
    have h'' : (m : ℝ) = (n : ℝ) := by
      linarith
    exact (Nat.cast_inj (R := ℝ)).1 h''
  have hinjOn : Set.InjOn f (Set.univ : Set ℕ) :=
    Function.Injective.injOn hinj
  have hUnivInf : (Set.univ : Set ℕ).Infinite := by
    simpa using (Set.infinite_univ : (Set.univ : Set ℕ).Infinite)
  have hImageInf : (f '' (Set.univ : Set ℕ)).Infinite :=
    Set.Infinite.image (s := (Set.univ : Set ℕ)) (f := f) hinjOn hUnivInf
  have hsubset :
      f '' (Set.univ : Set ℕ) ⊆
        {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} := by
    intro x hx
    rcases hx with ⟨k, hk, rfl⟩
    have hk0 : (0 : ℝ) ≤ (k : ℝ) := by
      exact_mod_cast (Nat.zero_le k)
    have hkpos : 0 < ((k : ℝ) + 1) := by
      linarith
    exact
      helperForCorollary_19_1_1_extremeDirection_posMul_closed
        (C := C) (d := d) hd hkpos
  exact Set.Infinite.mono hsubset hImageInf

Helper for Corollary 19.1.1: finiteness of extreme-direction vectors is equivalent to the absence of extreme directions.

lemma helperForCorollary_19_1_1_finite_extremeDirections_iff_not_exists
    {n : ℕ} {C : Set (Fin n → ℝ)} :
    Set.Finite {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} ↔
      ¬ ∃ d : Fin n → ℝ, IsExtremeDirection (𝕜 := ℝ) C d := by
  classical
  constructor
  · intro hfinite hex
    have hinf :
        Set.Infinite {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} :=
      helperForCorollary_19_1_1_infinite_extremeDirections_of_exists (C := C) hex
    exact hinf hfinite
  · intro hno
    have hempty :
        {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} =
          (∅ : Set (Fin n → ℝ)) := by
      apply Set.eq_empty_iff_forall_notMem.mpr
      intro d hd
      exact hno ⟨d, hd⟩
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hempty] using (Set.finite_empty : Set.Finite (∅ : Set (Fin n → ℝ)))

Helper for Corollary 19.1.1: polyhedral sets admit finitely many extreme-direction representatives up to positive scaling.

lemma helperForCorollary_19_1_1_correct_direction_statement_via_representatives
    {n : ℕ} {C : Set (Fin n → ℝ)} :
    IsPolyhedralConvexSet n C →
      ∃ S : Set (Fin n → ℝ),
        Set.Finite S ∧
          (∀ d, IsExtremeDirection (𝕜 := ℝ) C d →
            ∃ d0 ∈ S, ∃ t : ℝ, 0 < t ∧ d = t • d0) ∧
          S ⊆ {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} := by
  intro hpoly
  have hfaces :
      IsClosed C ∧ {C' : Set (Fin n → ℝ) | IsFace (𝕜 := ℝ) C C'}.Finite :=
    helperForTheorem_19_1_polyhedral_imp_closed_finiteFaces (n := n) (C := C) hpoly
  exact
    helperForTheorem_19_1_finiteFaces_imp_exists_finite_direction_reps
      (n := n) (C := C) hfaces.2

Helper for Corollary 19.1.1: in Fin 1 → ℝ : TypeFin 1 → ℝ, every vector is a multiple of the all-ones vector.

lemma helperForCorollary_19_1_1_fin1_eq_smul_one (x : Fin 1 → ℝ) :
    x = (x 0) • (fun _ : Fin 1 => (1 : ℝ)) := by
  ext i
  fin_cases i
  simp

Helper for Corollary 19.1.1: compute the dot product with the constant -1 : ℤ-1 vector in Fin 1 → ℝ : TypeFin 1 → ℝ.

lemma helperForCorollary_19_1_1_dotProduct_neg_one (x : Fin 1 → ℝ) :
    x ⬝ᵥ (fun _ : Fin 1 => (-1 : ℝ)) = - x 0 := by
  simp [dotProduct]

Helper for Corollary 19.1.1: the nonnegative half-space in Fin 1 → ℝ : TypeFin 1 → ℝ is polyhedral.

lemma helperForCorollary_19_1_1_polyhedral_halfspace_fin1 :
    IsPolyhedralConvexSet 1 (closedHalfSpaceLE 1 (fun _ => (-1 : ℝ)) 0) := by
  classical
  refine ⟨PUnit, ?_, (fun _ : PUnit => (fun _ : Fin 1 => (-1 : ℝ))), (fun _ => (0 : ℝ)), ?_⟩
  · infer_instance
  · ext x
    simp [closedHalfSpaceLE]

Helper for Corollary 19.1.1: the nonnegative half-space in Fin 1 → ℝ : TypeFin 1 → ℝ has direction vector 1 : ℕ1.

lemma helperForCorollary_19_1_1_halfspace_fin1_isDirectionOf :
    IsDirectionOf (𝕜 := ℝ)
      (closedHalfSpaceLE 1 (fun _ => (-1 : ℝ)) 0)
      (fun _ : Fin 1 => (1 : ℝ)) := by
  classical
  let d : Fin 1 → ℝ := fun _ => (1 : ℝ)
  refine ⟨0, ?_, ?_⟩
  · intro hzero
    have hzero' : (1 : ℝ) = 0 := by
      have h := congrArg (fun f => f 0) hzero
      Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [d] using h
    exact one_ne_zero hzero'
  ·
    ext x
    constructor
    · intro hx
      have hx' : x ⬝ᵥ (fun _ : Fin 1 => (-1 : ℝ)) ≤ 0 := by
        simpa [closedHalfSpaceLE] using hx
      have hx0 : 0 ≤ x 0 := by
        have hdot := helperForCorollary_19_1_1_dotProduct_neg_one x
        linarith [hx', hdot]
      refine ⟨x 0, hx0, ?_⟩
      have hxrepr : x = (x 0) • d := by
        have hxrepr' :
            x = (x 0) • (fun _ : Fin 1 => (1 : ℝ)) :=
          helperForCorollary_19_1_1_fin1_eq_smul_one x
        simpa [d] using hxrepr'
      have hxrepr' : (x 0) • d = x := hxrepr.symm
      calc
        (0 : Fin 1 → ℝ) + (x 0) • d = (x 0) • d := by simp
        _ = x := hxrepr'
    · intro hx
      rcases hx with ⟨t, ht, rfl⟩
      have ht0 : 0 ≤ t := by
        simpa using ht
      have ht' : -t ≤ 0 := by linarith [ht0]
      have hle :
          ((0 : Fin 1 → ℝ) + t • d) ⬝ᵥ (fun _ : Fin 1 => (-1 : ℝ)) ≤ 0 := by
        simpa [d, dotProduct, Fin.sum_univ_succ] using ht'
      simpa [closedHalfSpaceLE] using hle

Helper for Corollary 19.1.1: the nonnegative half-space in Fin 1 → ℝ : TypeFin 1 → ℝ has an extreme direction.

lemma helperForCorollary_19_1_1_halfspace_fin1_extremeDirection :
    IsExtremeDirection (𝕜 := ℝ)
      (closedHalfSpaceLE 1 (fun _ => (-1 : ℝ)) 0)
      (fun _ : Fin 1 => (1 : ℝ)) := by
  let C : Set (Fin 1 → ℝ) := closedHalfSpaceLE 1 (fun _ => (-1 : ℝ)) 0
  let d : Fin 1 → ℝ := fun _ => (1 : ℝ)
  have hpoly : IsPolyhedralConvexSet 1 C := by
    simpa [C] using helperForCorollary_19_1_1_polyhedral_halfspace_fin1
  have hconv : Convex ℝ C :=
    helperForTheorem_19_1_polyhedral_isConvex (n := 1) (C := C) hpoly
  have hface : IsFace (𝕜 := ℝ) C C := isFace_self (C := C) hconv
  have hdir : IsDirectionOf (𝕜 := ℝ) C d := by
    simpa [C, d] using helperForCorollary_19_1_1_halfspace_fin1_isDirectionOf
  have hhalf : IsHalfLineFace (𝕜 := ℝ) C C := by
    refine ⟨hface, ?_⟩
    refine ⟨d, hdir⟩
  exact ⟨C, hhalf, hdir⟩

Helper for Corollary 19.1.1: a polyhedral half-space in Fin 1 → ℝ : TypeFin 1 → ℝ has an extreme direction.

lemma helperForCorollary_19_1_1_counterexample_polyhedral_has_extremeDirection :
    ∃ C : Set (Fin 1 → ℝ),
      IsPolyhedralConvexSet 1 C ∧
        ∃ d : Fin 1 → ℝ, IsExtremeDirection (𝕜 := ℝ) C d := by
  let C : Set (Fin 1 → ℝ) := closedHalfSpaceLE 1 (fun _ => (-1 : ℝ)) 0
  let d : Fin 1 → ℝ := fun _ => (1 : ℝ)
  have hpoly : IsPolyhedralConvexSet 1 C := by
    simpa [C] using helperForCorollary_19_1_1_polyhedral_halfspace_fin1
  have hd : IsExtremeDirection (𝕜 := ℝ) C d := by
    simpa [C, d] using helperForCorollary_19_1_1_halfspace_fin1_extremeDirection
  refine ⟨C, hpoly, ?_⟩
  refine ⟨d, hd⟩

Helper for Corollary 19.1.1: a polyhedral set can have infinitely many extreme-direction vectors.

lemma helperForCorollary_19_1_1_counterexample_infinite_extremeDirections :
    ∃ C : Set (Fin 1 → ℝ),
      IsPolyhedralConvexSet 1 C ∧
        Set.Infinite {d : Fin 1 → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} := by
  rcases helperForCorollary_19_1_1_counterexample_polyhedral_has_extremeDirection with
    ⟨C, hpoly, hd⟩
  rcases hd with ⟨d, hd⟩
  refine ⟨C, hpoly, ?_⟩
  have hex : ∃ d : Fin 1 → ℝ, IsExtremeDirection (𝕜 := ℝ) C d := ⟨d, hd⟩
  exact
    helperForCorollary_19_1_1_infinite_extremeDirections_of_exists (C := C) hex

Helper for Corollary 19.1.1: the extreme-direction set for a polyhedral half-space in Fin 1 → ℝ : TypeFin 1 → ℝ is not finite.

lemma helperForCorollary_19_1_1_counterexample_not_finite_extremeDirections :
    ∃ C : Set (Fin 1 → ℝ),
      IsPolyhedralConvexSet 1 C ∧
        ¬ Set.Finite {d : Fin 1 → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} := by
  rcases helperForCorollary_19_1_1_counterexample_infinite_extremeDirections with
    ⟨C, hpoly, hInf⟩
  refine ⟨C, hpoly, ?_⟩
  intro hfin
  exact hInf hfin

Helper for Corollary 19.1.1: the statement fails already in dimension 1 : ℕ1.

lemma helperForCorollary_19_1_1_statement_false_fin1 :
    ¬ (∀ C : Set (Fin 1 → ℝ),
        IsPolyhedralConvexSet 1 C →
          Set.Finite {x : Fin 1 → ℝ | IsExtremePoint (𝕜 := ℝ) C x} ∧
            Set.Finite {d : Fin 1 → ℝ | IsExtremeDirection (𝕜 := ℝ) C d}) := by
  intro h
  rcases helperForCorollary_19_1_1_counterexample_not_finite_extremeDirections with
    ⟨C, hpoly, hnotfin⟩
  have h' := h C hpoly
  exact hnotfin h'.2

Helper for Corollary 19.1.1: the global finite-extreme-direction-vector claim is false, as witnessed by the dimension-1 : ℕ1 counterexample.

lemma helperForCorollary_19_1_1_statement_false_global :
    ¬ (∀ (n : ℕ) (C : Set (Fin n → ℝ)),
        IsPolyhedralConvexSet n C →
          Set.Finite {x : Fin n → ℝ | IsExtremePoint (𝕜 := ℝ) C x} ∧
            Set.Finite {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d}) := by
  intro h
  have hfin1 :
      ∀ C : Set (Fin 1 → ℝ),
        IsPolyhedralConvexSet 1 C →
          Set.Finite {x : Fin 1 → ℝ | IsExtremePoint (𝕜 := ℝ) C x} ∧
            Set.Finite {d : Fin 1 → ℝ | IsExtremeDirection (𝕜 := ℝ) C d} := by
    intro C hpoly
    simpa using h 1 C hpoly
  exact helperForCorollary_19_1_1_statement_false_fin1 hfin1

Helper for Corollary 19.1.1: polyhedral sets have finitely many extreme points.

lemma helperForCorollary_19_1_1_finite_extremePoints_of_polyhedral
    {n : ℕ} {C : Set (Fin n → ℝ)} :
    IsPolyhedralConvexSet n C →
      Set.Finite {x : Fin n → ℝ | IsExtremePoint (𝕜 := ℝ) C x} := by
  intro hpoly
  have hfaces :
      IsClosed C ∧ {C' : Set (Fin n → ℝ) | IsFace (𝕜 := ℝ) C C'}.Finite :=
    helperForTheorem_19_1_polyhedral_imp_closed_finiteFaces (n := n) (C := C) hpoly
  have hconv : Convex ℝ C :=
    helperForTheorem_19_1_polyhedral_isConvex n C hpoly
  exact
    helperForTheorem_19_1_finiteFaces_imp_finite_extremePoints
      (n := n) (C := C) hconv hfaces.2

Helper for Corollary 19.1.1: corrected direction claim via finitely many extreme-direction representatives up to positive scaling.

theorem polyhedralConvexSet_finite_extremePoints_extremeDirectionRepresentatives
    (n : ℕ) (C : Set (Fin n → ℝ)) :
    IsPolyhedralConvexSet n C →
      Set.Finite {x : Fin n → ℝ | IsExtremePoint (𝕜 := ℝ) C x} ∧
        (∃ S : Set (Fin n → ℝ),
          Set.Finite S ∧
            (∀ d, IsExtremeDirection (𝕜 := ℝ) C d →
              ∃ d0 ∈ S, ∃ t : ℝ, 0 < t ∧ d = t • d0) ∧
            S ⊆ {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d}) := by
  intro hpoly
  refine ⟨?_, ?_⟩
  · exact
      helperForCorollary_19_1_1_finite_extremePoints_of_polyhedral
        (n := n) (C := C) hpoly
  · exact
      helperForCorollary_19_1_1_correct_direction_statement_via_representatives
        (n := n) (C := C) hpoly

Corollary 19.1.1 (formalized via rays): A polyhedral convex set has at most a finite number of extreme points and finitely many extreme-direction representatives up to positive scaling.

theorem polyhedralConvexSet_finite_extremePoints_extremeDirections
    (n : ℕ) (C : Set (Fin n → ℝ)) :
    IsPolyhedralConvexSet n C →
      Set.Finite {x : Fin n → ℝ | IsExtremePoint (𝕜 := ℝ) C x} ∧
        (∃ S : Set (Fin n → ℝ),
          Set.Finite S ∧
            (∀ d, IsExtremeDirection (𝕜 := ℝ) C d →
              ∃ d0 ∈ S, ∃ t : ℝ, 0 < t ∧ d = t • d0) ∧
            S ⊆ {d : Fin n → ℝ | IsExtremeDirection (𝕜 := ℝ) C d}) := by
  exact
    polyhedralConvexSet_finite_extremePoints_extremeDirectionRepresentatives
      n C

Text 19.0.8: A convex function is called polyhedral convex if its epigraph Unknown identifier `epi`sorry = {x | sorry} : Propepi f = {Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`(x, μ) ∈ ℝ^{n+1} | f x ≤ μ} is a polyhedral convex set in ℝ ^ {sorry + 1} : Typeℝ^{Unknown identifier `n`n+1}.

def IsPolyhedralConvexFunction (n : ℕ) (f : (Fin n → ℝ) → EReal) : Prop :=
  ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f ∧
    IsPolyhedralConvexSet (n + 1)
      ((fun p => (prodLinearEquiv_append (n := n)) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f)

Helper for Text 19.0.9: every value of the max-affine-plus-indicator expression is different from ⊥ : ?m.1⊥.

lemma helperForText_19_0_9_rhsRepresentation_ne_bot
    {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ} {x : Fin n → ℝ} :
    ((sSup {r : ℝ |
        ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
      indicatorFunction
        (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
          (∑ j, y j * b i j) ≤ β i})
        x ≠ (⊥ : EReal) := by
  by_cases hx : x ∈ ({y | ∀ i : Fin m, k ≤ (i : ℕ) →
      (∑ j, y j * b i j) ≤ β i} : Set (Fin n → ℝ))
  · simp [indicatorFunction, hx]
  · simp [indicatorFunction, hx]

Helper for Text 19.0.9: any function with the theorem's max-affine-plus-indicator representation never takes the value ⊥ : ?m.1⊥.

lemma helperForText_19_0_9_representable_pointwise_ne_bot
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hrepr :
      ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          f =
            (fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x)) :
    ∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal) := by
  intro x
  rcases hrepr with ⟨k, m, b, β, _hk_le_m, hEq⟩
  subst hEq
  simpa using
    (helperForText_19_0_9_rhsRepresentation_ne_bot (n := n) (k := k) (m := m)
      (b := b) (β := β) (x := x))

Helper for Text 19.0.9: the max-affine-plus-indicator schema is never the constant ⊥ : ?m.1⊥ function.

lemma helperForText_19_0_9_constBot_ne_rhsRepresentation
    {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) :
    (fun _ : Fin n → ℝ => (⊥ : EReal)) ≠
      (fun x =>
        ((sSup {r : ℝ |
            ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
          indicatorFunction
            (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
              (∑ j, y j * b i j) ≤ β i})
            x) := by
  intro hEq
  let rhs : (Fin n → ℝ) → EReal :=
    fun x =>
      ((sSup {r : ℝ |
          ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
        indicatorFunction
          (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
            (∑ j, y j * b i j) ≤ β i})
          x
  have hEqRhs : (fun _ : Fin n → ℝ => (⊥ : EReal)) = rhs := by
    simpa [rhs] using hEq
  have hRhsAtZero_ne_bot : rhs 0 ≠ (⊥ : EReal) := by
    simpa [rhs] using
      (helperForText_19_0_9_rhsRepresentation_ne_bot (n := n) (k := k) (m := m)
        (b := b) (β := β) (x := 0))
  have hEqAtZero : (fun _ : Fin n → ℝ => (⊥ : EReal)) 0 = rhs 0 :=
    congrArg (fun g : (Fin n → ℝ) → EReal => g 0) hEqRhs
  have hRhsAtZero_eq_bot : rhs 0 = (⊥ : EReal) := by
    simpa using hEqAtZero.symm
  exact hRhsAtZero_ne_bot hRhsAtZero_eq_bot

Helper for Text 19.0.9: any function admitting the theorem's max-affine-plus-indicator representation is not the constant bottom function.

lemma helperForText_19_0_9_representable_ne_constBot
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hrepr :
      ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          f =
            (fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x)) :
    f ≠ (fun _ : Fin n → ℝ => (⊥ : EReal)) := by
  intro hconst
  have hPointwise : ∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal) :=
    helperForText_19_0_9_representable_pointwise_ne_bot (n := n) (f := f) hrepr
  have hAtZero : f 0 = (⊥ : EReal) := by
    simpa using congrArg (fun g : (Fin n → ℝ) → EReal => g 0) hconst
  exact (hPointwise 0) hAtZero

Helper for Text 19.0.9: a max-affine-plus-indicator representation yields both pointwise non-⊥ : ?m.1⊥ values and global non-constancy at ⊥ : ?m.1⊥.

lemma helperForText_19_0_9_representation_implies_nonbot_and_ne_constBot
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hrepr :
      ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          f =
            (fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x)) :
    (∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal)) ∧
      f ≠ (fun _ : Fin n → ℝ => (⊥ : EReal)) := by
  refine ⟨?_, ?_⟩
  · exact helperForText_19_0_9_representable_pointwise_ne_bot (n := n) (f := f) hrepr
  · exact helperForText_19_0_9_representable_ne_constBot (n := n) (f := f) hrepr

Helper for Text 19.0.9: the constant function satisfies IsPolyhedralConvexFunction (n : ℕ) (f : (Fin n → ℝ) → EReal) : PropIsPolyhedralConvexFunction in the present formalization.

lemma helperForText_19_0_9_constBot_isPolyhedralConvexFunction
    (n : ℕ) :
    IsPolyhedralConvexFunction n (fun _ : Fin n → ℝ => (⊥ : EReal)) := by
  refine ⟨?_, ?_⟩
  · have hEpiUniv :
      epigraph (Set.univ : Set (Fin n → ℝ)) (fun _ : Fin n → ℝ => (⊥ : EReal)) =
        Set.univ := by
      ext p
      constructor
      · intro hp
        trivial
      · intro hp
        refine ⟨?_, ?_⟩
        · trivial
        · simp
    simpa [ConvexFunctionOn, hEpiUniv] using
      (convex_univ : Convex ℝ (Set.univ : Set ((Fin n → ℝ) × ℝ)))
  · classical
    let ι : Type := PEmpty
    let b : ι → Fin (n + 1) → ℝ := fun i => nomatch i
    let β : ι → ℝ := fun i => nomatch i
    have hPolyUniv : IsPolyhedralConvexSet (n + 1) (Set.univ : Set (Fin (n + 1) → ℝ)) := by
      refine ⟨ι, inferInstance, b, β, ?_⟩
      ext x
      simp [closedHalfSpaceLE, b, β]
    have hEpiUniv :
        epigraph (Set.univ : Set (Fin n → ℝ)) (fun _ : Fin n → ℝ => (⊥ : EReal)) =
          Set.univ := by
      ext p
      constructor
      · intro hp
        trivial
      · intro hp
        refine ⟨?_, ?_⟩
        · trivial
        · simp
    have hImageUnivCoord :
        ((fun p => prodLinearEquiv_append_coord (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) (fun _ : Fin n → ℝ => (⊥ : EReal))) =
          (Set.univ : Set (Fin (n + 1) → ℝ)) := by
      rw [hEpiUniv, Set.image_univ]
      exact Set.range_eq_univ.mpr (prodLinearEquiv_append_coord (n := n)).surjective
    have hpolyCoord :
        IsPolyhedralConvexSet (n + 1)
          ((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) (fun _ : Fin n → ℝ => (⊥ : EReal))) := by
      simpa [hImageUnivCoord] using hPolyUniv
    simpa [prodLinearEquiv_append_coord] using hpolyCoord

Helper for Text 19.0.9: the constant function cannot be represented by the max-affine-plus-indicator normal form from the theorem statement.

lemma helperForText_19_0_9_constBot_not_representable
    (n : ℕ) :
    ¬ ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          (fun _ : Fin n → ℝ => (⊥ : EReal)) =
            (fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x) := by
  intro hrepr
  have hPointwise :
      ∀ x : Fin n → ℝ,
        (fun _ : Fin n → ℝ => (⊥ : EReal)) x ≠ (⊥ : EReal) :=
    helperForText_19_0_9_representable_pointwise_ne_bot
      (n := n) (f := (fun _ : Fin n → ℝ => (⊥ : EReal))) hrepr
  exact (hPointwise 0) rfl

Helper for Text 19.0.9: the constant function provides both sides of the counterexample data used to refute the biconditional schema.

lemma helperForText_19_0_9_constBot_counterexample_data
    (n : ℕ) :
    IsPolyhedralConvexFunction n (fun _ : Fin n → ℝ => (⊥ : EReal)) ∧
      ¬ ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
          k ≤ m ∧
            (fun _ : Fin n → ℝ => (⊥ : EReal)) =
              (fun x =>
                ((sSup {r : ℝ |
                    ∃ i : Fin m, (i : ℕ) < k ∧
                      r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                  indicatorFunction
                    (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                      (∑ j, y j * b i j) ≤ β i})
                    x) := by
  refine ⟨?_, ?_⟩
  · exact helperForText_19_0_9_constBot_isPolyhedralConvexFunction n
  · exact helperForText_19_0_9_constBot_not_representable n

Helper for Text 19.0.9: if the biconditional schema is assumed at a fixed polyhedral-convex function Unknown identifier `f`f, then Unknown identifier `f`f must be pointwise non-⊥ : ?m.1⊥.

lemma helperForText_19_0_9_schema_at_polyhedral_function_implies_pointwise_ne_bot
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hSchemaAtF :
      IsPolyhedralConvexFunction n f ↔
        ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
          k ≤ m ∧
            f =
              (fun x =>
                ((sSup {r : ℝ |
                    ∃ i : Fin m, (i : ℕ) < k ∧
                      r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                  indicatorFunction
                    (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                      (∑ j, y j * b i j) ≤ β i})
                    x))
    (hPoly : IsPolyhedralConvexFunction n f) :
    ∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal) := by
  have hrepr :
      ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          f =
            (fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x) :=
    hSchemaAtF.mp hPoly
  exact helperForText_19_0_9_representable_pointwise_ne_bot (n := n) (f := f) hrepr

Helper for Text 19.0.9: the constant-⊥ : ?m.1⊥ instance of the biconditional schema forces a contradiction with pointwise non-⊥ : ?m.1⊥.

lemma helperForText_19_0_9_constBot_schema_implies_false
    (n : ℕ)
    (hSchemaAtConstBot :
      IsPolyhedralConvexFunction n (fun _ : Fin n → ℝ => (⊥ : EReal)) ↔
        ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
          k ≤ m ∧
            (fun _ : Fin n → ℝ => (⊥ : EReal)) =
              (fun x =>
                ((sSup {r : ℝ |
                    ∃ i : Fin m, (i : ℕ) < k ∧
                      r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                  indicatorFunction
                    (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                      (∑ j, y j * b i j) ≤ β i})
                    x)) :
    False := by
  have hPolyConstBot :
      IsPolyhedralConvexFunction n (fun _ : Fin n → ℝ => (⊥ : EReal)) :=
    helperForText_19_0_9_constBot_isPolyhedralConvexFunction n
  have hPointwiseNonBotConstBot :
      ∀ x : Fin n → ℝ,
        (fun _ : Fin n → ℝ => (⊥ : EReal)) x ≠ (⊥ : EReal) :=
    helperForText_19_0_9_schema_at_polyhedral_function_implies_pointwise_ne_bot
      (n := n) (f := (fun _ : Fin n → ℝ => (⊥ : EReal)))
      hSchemaAtConstBot hPolyConstBot
  exact (hPointwiseNonBotConstBot 0) rfl

Helper for Text 19.0.9: instantiating the theorem schema at the constant-⊥ : ?m.1⊥ function yields a contradiction in the current EReal : TypeEReal formalization.

lemma helperForText_19_0_9_constBot_breaks_biconditional
    (n : ℕ) :
    ¬
      (IsPolyhedralConvexFunction n (fun _ : Fin n → ℝ => (⊥ : EReal)) ↔
        ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
          k ≤ m ∧
            (fun _ : Fin n → ℝ => (⊥ : EReal)) =
              (fun x =>
                ((sSup {r : ℝ |
                    ∃ i : Fin m, (i : ℕ) < k ∧
                      r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                  indicatorFunction
                    (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                      (∑ j, y j * b i j) ≤ β i})
                    x)) := by
  intro hiff
  exact helperForText_19_0_9_constBot_schema_implies_false n hiff

Helper for Text 19.0.9: in each fixed dimension Unknown identifier `n`n, the constant-⊥ : ?m.1⊥ function is an explicit witness where the biconditional schema fails.

lemma helperForText_19_0_9_exists_function_counterexample_at_dimension
    (n : ℕ) :
    ∃ f : (Fin n → ℝ) → EReal,
      ¬
        (IsPolyhedralConvexFunction n f ↔
          ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
            k ≤ m ∧
              f =
                (fun x =>
                  ((sSup {r : ℝ |
                      ∃ i : Fin m, (i : ℕ) < k ∧
                        r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                    indicatorFunction
                      (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                        (∑ j, y j * b i j) ≤ β i})
                      x)) := by
  refine ⟨(fun _ : Fin n → ℝ => (⊥ : EReal)), ?_⟩
  exact helperForText_19_0_9_constBot_breaks_biconditional n

Helper for Text 19.0.9: the target biconditional schema cannot hold for all functions , since it fails at the constant-⊥ : ?m.1⊥ function.

lemma helperForText_19_0_9_not_forall_function_schema
    (n : ℕ) :
    ¬
      (∀ f : (Fin n → ℝ) → EReal,
        IsPolyhedralConvexFunction n f ↔
          ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
            k ≤ m ∧
              f =
                (fun x =>
                  ((sSup {r : ℝ |
                      ∃ i : Fin m, (i : ℕ) < k ∧
                        r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                    indicatorFunction
                      (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                        (∑ j, y j * b i j) ≤ β i})
                      x)) := by
  intro hAll
  rcases helperForText_19_0_9_exists_function_counterexample_at_dimension n with ⟨f, hf⟩
  exact hf (hAll f)

Helper for Text 19.0.9: a concrete (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `n`n, Unknown identifier `f`f) witness shows the target schema fails at the constant-⊥ : ?m.1⊥ function.

lemma helperForText_19_0_9_exists_counterexample_to_schema :
    ∃ n : ℕ, ∃ f : (Fin n → ℝ) → EReal,
      ¬
        (IsPolyhedralConvexFunction n f ↔
          ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
            k ≤ m ∧
              f =
                (fun x =>
                  ((sSup {r : ℝ |
                      ∃ i : Fin m, (i : ℕ) < k ∧
                        r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                    indicatorFunction
                      (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                        (∑ j, y j * b i j) ≤ β i})
                      x)) := by
  refine ⟨0, ?_⟩
  refine ⟨(fun _ : Fin 0 → ℝ => (⊥ : EReal)), ?_⟩
  exact helperForText_19_0_9_constBot_breaks_biconditional 0

Helper for Text 19.0.9: if the biconditional schema held for all dimensions and functions, it would contradict the explicit counterexample.

lemma helperForText_19_0_9_global_schema_implies_false
    (hGlobal :
      ∀ n : ℕ, ∀ f : (Fin n → ℝ) → EReal,
        IsPolyhedralConvexFunction n f ↔
          ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
            k ≤ m ∧
              f =
                (fun x =>
                  ((sSup {r : ℝ |
                      ∃ i : Fin m, (i : ℕ) < k ∧
                        r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                    indicatorFunction
                      (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                        (∑ j, y j * b i j) ≤ β i})
                      x)) :
    False := by
  rcases helperForText_19_0_9_exists_counterexample_to_schema with ⟨n, f, hNotSchema⟩
  exact hNotSchema (hGlobal n f)

Helper for Text 19.0.9: a theorem-schema claiming the biconditional for all dimensions and functions is refuted by the constant-⊥ : ?m.1⊥ counterexample.

lemma helperForText_19_0_9_no_global_theorem_schema :
    ¬
      (∀ n : ℕ, ∀ f : (Fin n → ℝ) → EReal,
        IsPolyhedralConvexFunction n f ↔
          ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
            k ≤ m ∧
              f =
                (fun x =>
                  ((sSup {r : ℝ |
                      ∃ i : Fin m, (i : ℕ) < k ∧
                        r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                    indicatorFunction
                      (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                        (∑ j, y j * b i j) ≤ β i})
                      x)) := by
  intro hGlobal
  exact helperForText_19_0_9_global_schema_implies_false hGlobal

Helper for Text 19.0.9: the finite family of affine-epigraph inequalities with normals (sorry, -1) : ?m.1 × ℤ(Unknown identifier `b_i`b_i, -1) defines a polyhedral set in failed to synthesize HPow Type ℕ Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.ℝ ^ (sorry + 1) : Typeℝ^(Unknown identifier `n`n+1).

lemma helperForText_19_0_9_affineConstraintSet_polyhedral
    {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) :
    IsPolyhedralConvexSet (n + 1)
      {z : Fin (n + 1) → ℝ |
        ∀ i : Fin m, (i : ℕ) < k →
          dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} := by
  classical
  let bAff : Fin m → Fin (n + 1) → ℝ :=
    fun i => if hik : (i : ℕ) < k then Fin.cases (-1 : ℝ) (b i) else 0
  let βAff : Fin m → ℝ :=
    fun i => if hik : (i : ℕ) < k then β i else 0
  refine ⟨Fin m, inferInstance, bAff, βAff, ?_⟩
  ext z
  constructor
  · intro hz
    refine Set.mem_iInter.2 ?_
    intro i
    by_cases hik : (i : ℕ) < k
    · have hineq : dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i := hz i hik
      simpa [bAff, βAff, hik, closedHalfSpaceLE] using hineq
    · have htriv : dotProduct z (0 : Fin (n + 1) → ℝ) ≤ (0 : ℝ) := by
        simp
      simp [bAff, βAff, hik, closedHalfSpaceLE] at htriv ⊢
  · intro hz i hik
    have hzi : z ∈ closedHalfSpaceLE (n + 1) (bAff i) (βAff i) :=
      Set.mem_iInter.1 hz i
    simpa [bAff, βAff, hik, closedHalfSpaceLE] using hzi

Helper for Text 19.0.9: the finite family of domain inequalities with normals (sorry, 0) : ?m.1 × ℕ(Unknown identifier `b_i`b_i, 0) defines a polyhedral set in failed to synthesize HPow Type ℕ Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.ℝ ^ (sorry + 1) : Typeℝ^(Unknown identifier `n`n+1).

lemma helperForText_19_0_9_liftedIndicatorConstraintSet_polyhedral
    {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) :
    IsPolyhedralConvexSet (n + 1)
      {z : Fin (n + 1) → ℝ |
        ∀ i : Fin m, k ≤ (i : ℕ) →
          dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i} := by
  classical
  let bDom : Fin m → Fin (n + 1) → ℝ :=
    fun i => if hki : k ≤ (i : ℕ) then Fin.cases (0 : ℝ) (b i) else 0
  let βDom : Fin m → ℝ :=
    fun i => if hki : k ≤ (i : ℕ) then β i else 0
  refine ⟨Fin m, inferInstance, bDom, βDom, ?_⟩
  ext z
  constructor
  · intro hz
    refine Set.mem_iInter.2 ?_
    intro i
    by_cases hki : k ≤ (i : ℕ)
    · have hineq : dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i := hz i hki
      simpa [bDom, βDom, hki, closedHalfSpaceLE] using hineq
    · have htriv : dotProduct z (0 : Fin (n + 1) → ℝ) ≤ (0 : ℝ) := by
        simp
      simp [bDom, βDom, hki, closedHalfSpaceLE] at htriv ⊢
  · intro hz i hki
    have hzi : z ∈ closedHalfSpaceLE (n + 1) (bDom i) (βDom i) :=
      Set.mem_iInter.1 hz i
    simpa [bDom, βDom, hki, closedHalfSpaceLE] using hzi

Helper for Text 19.0.9: intersecting the affine-epigraph and lifted-domain constraint families yields a polyhedral set in failed to synthesize HPow Type ℕ Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.ℝ ^ (sorry + 1) : Typeℝ^(Unknown identifier `n`n+1).

lemma helperForText_19_0_9_liftedConstraintIntersection_polyhedral
    {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) :
    IsPolyhedralConvexSet (n + 1)
      ({z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, (i : ℕ) < k →
            dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} ∩
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, k ≤ (i : ℕ) →
            dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i}) := by
  exact
    helperForTheorem_19_1_polyhedral_inter
      (helperForText_19_0_9_affineConstraintSet_polyhedral (n := n) (k := k) (m := m)
        b β)
      (helperForText_19_0_9_liftedIndicatorConstraintSet_polyhedral
        (n := n) (k := k) (m := m) b β)

Helper for Text 19.0.9: if the transformed epigraph image is empty, then Unknown identifier `f`f admits the max-affine-plus-indicator representation (the Unknown identifier `f`sorry = ⊤ : Propf = ⊤ branch).

lemma helperForText_19_0_9_empty_transformedEpigraph_implies_representation
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hEmpty :
      ((fun p => prodLinearEquiv_append (n := n) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) = ∅) :
    ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
      k ≤ m ∧
        f =
          fun x =>
            ((sSup {r : ℝ |
                ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
              indicatorFunction
                (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                  (∑ j, y j * b i j) ≤ β i})
                x := by
  have hfTop : ∀ x : Fin n → ℝ, f x = (⊤ : EReal) := by
    intro x
    by_contra hNotTop
    have hExistsMu : ∃ μ : ℝ, f x ≤ (μ : EReal) := by
      by_cases hBot : f x = (⊥ : EReal)
      · refine ⟨0, ?_⟩
        simp [hBot]
      · refine ⟨(f x).toReal, ?_⟩
        have hcoe : (((f x).toReal : ℝ) : EReal) = f x := by
          simpa using (EReal.coe_toReal hNotTop hBot)
        simp [hcoe]
    rcases hExistsMu with ⟨μ, hle⟩
    have hmemEpi : (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f := by
      exact (mem_epigraph_univ_iff (f := f)).2 hle
    have hmemImage :
        (prodLinearEquiv_append (n := n)) (x, μ) ∈
          ((fun p => prodLinearEquiv_append (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
      exact ⟨(x, μ), hmemEpi, rfl⟩
    have hnotMem :
        (prodLinearEquiv_append (n := n)) (x, μ) ∉
          ((fun p => prodLinearEquiv_append (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
      simp [hEmpty]
    exact hnotMem hmemImage
  have hfConstTop : f = (fun _ : Fin n → ℝ => (⊤ : EReal)) := by
    funext x
    exact hfTop x
  refine ⟨0, 1, (fun _ _ => (0 : ℝ)), (fun _ => (-1 : ℝ)), Nat.zero_le 1, ?_⟩
  calc
    f = (fun _ : Fin n → ℝ => (⊤ : EReal)) := hfConstTop
    _ =
      (fun x =>
        ((sSup {r : ℝ |
            ∃ i : Fin 1, (i : ℕ) < 0 ∧ r = (∑ j, x j * (0 : ℝ)) - (-1 : ℝ)} : ℝ) : EReal) +
          indicatorFunction
            (C := {y : Fin n → ℝ | ∀ i : Fin 1, 0 ≤ (i : ℕ) →
              (∑ j, y j * (0 : ℝ)) ≤ (-1 : ℝ)})
            x) := by
          funext x
          simp [indicatorFunction]

Helper for Text 19.0.9: in the forward direction, the empty transformed-epigraph branch is discharged by the dedicated Unknown identifier `f`sorry = ⊤ : Propf = ⊤ representation lemma.

lemma helperForText_19_0_9_polyhedral_nonbot_implies_representation_of_empty_transformedEpigraph
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (_hpolyNonbot :
      IsPolyhedralConvexFunction n f ∧
        (∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal)))
    (hEmpty :
      ((fun p => prodLinearEquiv_append (n := n) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) = ∅) :
    ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
      k ≤ m ∧
        f =
          fun x =>
            ((sSup {r : ℝ |
                ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
              indicatorFunction
                (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                  (∑ j, y j * b i j) ≤ β i})
                x := by
  exact helperForText_19_0_9_empty_transformedEpigraph_implies_representation
    (n := n) (f := f) hEmpty

Helper for Text 19.0.9: any represented function satisfies the theorem's pointwise non-⊥ : ?m.1⊥ side condition.

lemma helperForText_19_0_9_representation_implies_pointwise_nonbot_sideCondition
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hrepr :
      ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          f =
            (fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x)) :
    ∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal) := by
  exact helperForText_19_0_9_representable_pointwise_ne_bot
    (n := n) (f := f) hrepr

Helper for Text 19.0.9: membership in a transformed-image subset of Euclidean space can be transported to function coordinates via WithLp.toLp.{u_1} (p : ENNReal) {V : Type u_1} (ofLp : V) : WithLp p VWithLp.toLp.

lemma helperForText_19_0_9_mem_transformedImage_coordEuclid_transport
    {n : ℕ} {S : Set (EuclideanSpace ℝ (Fin (n + 1)))} {z : Fin (n + 1) → ℝ} :
    (WithLp.toLp 2 z ∈ S) ↔ z ∈ (WithLp.toLp 2) ⁻¹' S := by
  rfl

Helper for Text 19.0.9: unpacking prodLinearEquiv_append_coord (n : ℕ) : ((Fin n → ℝ) × ℝ) ≃ₗ[ℝ] Fin (n + 1) → ℝprodLinearEquiv_append_coord equals unpacking prodLinearEquiv_append {n : ℕ} : ((Fin n → ℝ) × ℝ) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin (n + 1))prodLinearEquiv_append after the coordinate-to-Euclidean coercion.

lemma helperForText_19_0_9_prodLinearEquivAppendCoord_symm_eq
    {n : ℕ} (z : Fin (n + 1) → ℝ) :
    (prodLinearEquiv_append_coord (n := n)).symm z =
      (prodLinearEquiv_append (n := n)).symm (WithLp.toLp 2 z) := by
  rfl

Helper for Text 19.0.9: the packed-coordinate embedding recovers each base coordinate at Fin.castSucc {n : ℕ} : Fin n → Fin (n + 1)Fin.castSucc.

lemma helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
    {n : ℕ} (x0 : Fin n → ℝ) (μ0 : ℝ) (j0 : Fin n) :
    x0 j0 = (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (Fin.castSucc j0) := by
  change x0 j0 = (prodLinearEquiv_append (n := n) (x0, μ0)).ofLp (Fin.castSucc j0)
  change x0 j0 =
    ((appendAffineEquiv n 1).linear
      (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0))).ofLp (Fin.castSucc j0)
  have happ := congrArg
    (fun v => ((EuclideanSpace.equiv (𝕜 := Real) (ι := Fin (n + 1))) v) (Fin.castSucc j0))
    (appendAffineEquiv_apply n 1 (WithLp.toLp 2 x0) (WithLp.toLp 2 (Function.const (Fin 1) μ0)))
  have hlin :
      (appendAffineEquiv n 1) (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0)) =
        (appendAffineEquiv n 1).linear
          (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0)) := by
    simpa using congrArg
      (fun f => f (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0)))
      (appendAffineEquiv_eq_linear_toAffineEquiv n 1)
  have happ' :
      ((appendAffineEquiv n 1).linear
        (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0))).ofLp (Fin.castSucc j0) =
        Fin.append x0 (Function.const (Fin 1) μ0) (Fin.castSucc j0) := by
    simpa [hlin] using happ
  have happend : Fin.append x0 (Function.const (Fin 1) μ0) (Fin.castSucc j0) = x0 j0 := by
    exact Fin.append_left (u := x0) (v := Function.const (Fin 1) μ0) j0
  exact (happ'.trans happend).symm

Helper for Text 19.0.9: the last packed coordinate equals the appended scalar.

lemma helperForText_19_0_9_prodLinearEquivAppendCoord_last
    {n : ℕ} (x0 : Fin n → ℝ) (μ0 : ℝ) :
    μ0 = (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (Fin.last n) := by
  change μ0 = (prodLinearEquiv_append (n := n) (x0, μ0)).ofLp (Fin.last n)
  change μ0 =
    ((appendAffineEquiv n 1).linear
      (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0))).ofLp (Fin.last n)
  have happ := congrArg
    (fun v => ((EuclideanSpace.equiv (𝕜 := Real) (ι := Fin (n + 1))) v) (Fin.last n))
    (appendAffineEquiv_apply n 1 (WithLp.toLp 2 x0) (WithLp.toLp 2 (Function.const (Fin 1) μ0)))
  have hlin :
      (appendAffineEquiv n 1) (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0)) =
        (appendAffineEquiv n 1).linear
          (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0)) := by
    simpa using congrArg
      (fun f => f (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0)))
      (appendAffineEquiv_eq_linear_toAffineEquiv n 1)
  have happ' :
      ((appendAffineEquiv n 1).linear
        (WithLp.toLp 2 x0, WithLp.toLp 2 (Function.const (Fin 1) μ0))).ofLp (Fin.last n) =
        Fin.append x0 (Function.const (Fin 1) μ0) (Fin.last n) := by
    simpa [hlin] using happ
  have happend : Fin.append x0 (Function.const (Fin 1) μ0) (Fin.last n) = μ0 := by
    have hlast : Fin.natAdd n (0 : Fin 1) = Fin.last n := by
      simpa [Nat.add_zero] using (Fin.natAdd_last (n := n) (m := 0))
    rw [← hlast]
    simp [Fin.append]
  exact (happ'.trans happend).symm

Helper for Text 19.0.9: dot product in packed coordinates splits as base dot product plus product of the appended scalar coordinates.

lemma helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord
    {n : ℕ} (p q : (Fin n → ℝ) × ℝ) :
    dotProduct
      (prodLinearEquiv_append_coord (n := n) p)
      (prodLinearEquiv_append_coord (n := n) q) =
      dotProduct p.1 q.1 + p.2 * q.2 := by
  rcases p with ⟨x, μ⟩
  rcases q with ⟨y, ν⟩
  have hx_cast :
      ∀ j : Fin n,
        (prodLinearEquiv_append_coord (n := n) (x, μ)) (Fin.castSucc j) = x j := by
    intro j
    exact
      (helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
        (n := n) (x0 := x) (μ0 := μ) (j0 := j)).symm
  have hy_cast :
      ∀ j : Fin n,
        (prodLinearEquiv_append_coord (n := n) (y, ν)) (Fin.castSucc j) = y j := by
    intro j
    exact
      (helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
        (n := n) (x0 := y) (μ0 := ν) (j0 := j)).symm
  have hx_last :
      (prodLinearEquiv_append_coord (n := n) (x, μ)) (Fin.last n) = μ := by
    exact
      (helperForText_19_0_9_prodLinearEquivAppendCoord_last
        (n := n) (x0 := x) (μ0 := μ)).symm
  have hy_last :
      (prodLinearEquiv_append_coord (n := n) (y, ν)) (Fin.last n) = ν := by
    exact
      (helperForText_19_0_9_prodLinearEquivAppendCoord_last
        (n := n) (x0 := y) (μ0 := ν)).symm
  calc
    dotProduct
      (prodLinearEquiv_append_coord (n := n) (x, μ))
      (prodLinearEquiv_append_coord (n := n) (y, ν))
        =
          (∑ j : Fin n,
            (prodLinearEquiv_append_coord (n := n) (x, μ)) (Fin.castSucc j) *
              (prodLinearEquiv_append_coord (n := n) (y, ν)) (Fin.castSucc j)) +
            (prodLinearEquiv_append_coord (n := n) (x, μ)) (Fin.last n) *
              (prodLinearEquiv_append_coord (n := n) (y, ν)) (Fin.last n) := by
          simp [dotProduct, Fin.sum_univ_castSucc]
    _ = (∑ j : Fin n, x j * y j) + μ * ν := by
          simp [hx_cast, hy_cast, hx_last, hy_last]
    _ = dotProduct x y + μ * ν := by
          simp [dotProduct]

Helper for Text 19.0.9: dot products against packed normals (sorry, -1) : ?m.1 × ℤ(Unknown identifier `b_i`b_i, -1) decode to the affine expression sorry ⬝ᵥ sorry - sorry : ?m.9dotProduct (Unknown identifier `b_i`b_i) Unknown identifier `x`x - Unknown identifier `μ`μ at pulled-back coordinates.

lemma helperForText_19_0_9_dotPacked_point
    {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m)
    (y : Fin (n + 1) → ℝ) :
    dotProduct y (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) =
      dotProduct (b i) ((prodLinearEquiv_append_coord (n := n)).symm y).1 -
        ((prodLinearEquiv_append_coord (n := n)).symm y).2 := by
  let q : (Fin n → ℝ) × ℝ := (prodLinearEquiv_append_coord (n := n)).symm y
  have hy : prodLinearEquiv_append_coord (n := n) q = y := by
    simp [q]
  calc
    dotProduct y (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ)))
        = dotProduct (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) y := by
            simp [dotProduct_comm]
    _ = dotProduct
          (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ)))
          (prodLinearEquiv_append_coord (n := n) q) := by
            simp [hy]
    _ = dotProduct (b i) q.1 + (-1 : ℝ) * q.2 := by
          simpa using
            helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord
              (n := n) (p := (b i, (-1 : ℝ))) (q := q)
    _ = dotProduct (b i) q.1 - q.2 := by
          ring
    _ = dotProduct (b i) ((prodLinearEquiv_append_coord (n := n)).symm y).1 -
          ((prodLinearEquiv_append_coord (n := n)).symm y).2 := by
            simp [q]

Helper for Text 19.0.9: dot products against packed normals (sorry, 0) : ?m.1 × ℕ(Unknown identifier `b_i`b_i, 0) decode to sorry ⬝ᵥ sorry : ?m.2dotProduct (Unknown identifier `b_i`b_i) Unknown identifier `x`x at pulled-back coordinates.

lemma helperForText_19_0_9_dotPacked_direction
    {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m)
    (y : Fin (n + 1) → ℝ) :
    dotProduct y (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) =
      dotProduct (b i) ((prodLinearEquiv_append_coord (n := n)).symm y).1 := by
  let q : (Fin n → ℝ) × ℝ := (prodLinearEquiv_append_coord (n := n)).symm y
  have hy : prodLinearEquiv_append_coord (n := n) q = y := by
    simp [q]
  calc
    dotProduct y (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ)))
        = dotProduct (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) y := by
            simp [dotProduct_comm]
    _ = dotProduct
          (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ)))
          (prodLinearEquiv_append_coord (n := n) q) := by
            simp [hy]
    _ = dotProduct (b i) q.1 + (0 : ℝ) * q.2 := by
          simpa using
            helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord
              (n := n) (p := (b i, (0 : ℝ))) (q := q)
    _ = dotProduct (b i) q.1 := by
          ring
    _ = dotProduct (b i) ((prodLinearEquiv_append_coord (n := n)).symm y).1 := by
          simp [q]

Helper for Text 19.0.9: the transformed-epigraph image is upward closed in the last coordinate at fixed base point.

lemma helperForText_19_0_9_transformedEpigraphImage_upwardClosed_lastCoord
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    {x : Fin n → ℝ} {μ t : ℝ}
    (hy :
      prodLinearEquiv_append (n := n) (x, μ) ∈
        ((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f))
    (ht : 0 ≤ t) :
    prodLinearEquiv_append (n := n) (x, μ + t) ∈
      ((fun p => prodLinearEquiv_append (n := n) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
  rcases hy with ⟨p, hpEpi, hpMap⟩
  have hpEq : p = (x, μ) :=
    (prodLinearEquiv_append (n := n)).injective hpMap
  rcases p with ⟨x0, μ0⟩
  cases hpEq
  have hleμ : f x ≤ ((μ : ℝ) : EReal) :=
    (mem_epigraph_univ_iff (f := f)).1 hpEpi
  have hμ_le_μt : ((μ : ℝ) : EReal) ≤ (((μ + t : ℝ) : ℝ) : EReal) := by
    exact_mod_cast (show μ ≤ μ + t from by linarith [ht])
  have hleμt : f x ≤ (((μ + t : ℝ) : ℝ) : EReal) :=
    le_trans hleμ hμ_le_μt
  have hEpi' : (x, μ + t) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f :=
    (mem_epigraph_univ_iff (f := f)).2 hleμt
  exact ⟨(x, μ + t), hEpi', rfl⟩

Helper for Text 19.0.9: nonemptiness of the transformed-epigraph image yields a base point and scalar with finite-epigraph inequality data.

lemma helperForText_19_0_9_nonempty_transformedEpigraphImage_unpack
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hNonempty :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)).Nonempty) :
    ∃ x : Fin n → ℝ, ∃ μ : ℝ, f x ≤ (μ : EReal) := by
  rcases hNonempty with ⟨y, hy⟩
  rcases hy with ⟨p, hpEpi, hpMap⟩
  rcases p with ⟨x, μ⟩
  refine ⟨x, μ, ?_⟩
  exact (mem_epigraph_univ_iff (f := f)).1 hpEpi

Helper for Text 19.0.9: transformed-epigraph image membership at a packed point is equivalent to ordinary epigraph membership at the unpacked point.

lemma helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
    {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} :
    (prodLinearEquiv_append (n := n) (x, μ)) ∈
      ((fun p => prodLinearEquiv_append (n := n) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) ↔
      (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f := by
  constructor
  · intro hmem
    rcases hmem with ⟨p, hpEpi, hpImage⟩
    have hp : p = (x, μ) :=
      (prodLinearEquiv_append (n := n)).injective hpImage
    simpa [hp] using hpEpi
  · intro hmem
    exact ⟨(x, μ), hmem, rfl⟩

Helper for Text 19.0.9: polyhedrality of the transformed epigraph image yields a finite raw halfspace presentation.

lemma helperForText_19_0_9_nonempty_polyhedral_transformedImage_extract_rawHalfspaces
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hpoly : IsPolyhedralConvexFunction n f) :
    ∃ (m : ℕ) (a : Fin m → Fin (n + 1) → ℝ) (α : Fin m → ℝ),
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        ⋂ i, closedHalfSpaceLE (n + 1) (a i) (α i) := by
  exact
    (isPolyhedralConvexSet_iff_exists_finite_halfspaces
      (n := n + 1)
      (C :=
        (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)))).1
      hpoly.2

Helper for Text 19.0.9: in the Unknown identifier `k`sorry = 0 : Propk = 0 branch, feasibility of the domain-inequality family yields a witness that the split-halfspace set is nonempty.

lemma helperForText_19_0_9_kZero_splitHalfspaces_allow_negativeLastCoord
    {n m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ)
    (hfeas : ∃ x0 : Fin n → ℝ, ∀ i : Fin m, (∑ j, x0 j * b i j) ≤ β i) :
    let g : (Fin n → ℝ) → EReal :=
      fun x =>
        ((sSup {r : ℝ |
            ∃ i : Fin m, (i : ℕ) < 0 ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
          indicatorFunction
            (C := {y | ∀ i : Fin m, 0 ≤ (i : ℕ) →
              (∑ j, y j * b i j) ≤ β i})
            x
    let _Simg : Set (Fin (n + 1) → ℝ) :=
      ((fun p => prodLinearEquiv_append (n := n) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) g)
    let Ssplit : Set (Fin (n + 1) → ℝ) :=
      ({z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, (i : ℕ) < 0 →
            dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} ∩
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, 0 ≤ (i : ℕ) →
            dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i})
    ∃ y0 : Fin (n + 1) → ℝ, y0 ∈ Ssplit := by
  rcases hfeas with ⟨x0, hx0feas⟩
  let Ssplit : Set (Fin (n + 1) → ℝ) :=
    ({z : Fin (n + 1) → ℝ |
        ∀ i : Fin m, (i : ℕ) < 0 →
          dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} ∩
      {z : Fin (n + 1) → ℝ |
        ∀ i : Fin m, 0 ≤ (i : ℕ) →
          dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i})
  change ∃ y0 : Fin (n + 1) → ℝ, y0 ∈ Ssplit
  let y0 : Fin (n + 1) → ℝ := Fin.cases (0 : ℝ) x0
  refine ⟨y0, ?_⟩
  refine And.intro ?_ ?_
  · intro i hi
    exact (Nat.not_lt_zero (i : ℕ) hi).elim
  · intro i hi
    have hdot : dotProduct y0 (Fin.cases (0 : ℝ) (b i)) = dotProduct x0 (b i) := by
      simp [dotProduct, y0, Fin.sum_univ_succ]
    have hfeasDot : dotProduct x0 (b i) ≤ β i := by
      simpa [dotProduct] using hx0feas i
    simpa [hdot] using hfeasDot

Helper for Text 19.0.9: equality of transformed-epigraph images determines the underlying EReal : TypeEReal-valued function uniquely.

lemma helperForText_19_0_9_transformedImage_eq_implies_function_eq
    {n : ℕ} {f g : (Fin n → ℝ) → EReal}
    (hImageEq :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f)) =
        (((fun p => prodLinearEquiv_append (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) g))) :
    f = g := by
  funext x
  have hUpperCutsEq :
      ∀ μ : ℝ, f x ≤ (μ : EReal) ↔ g x ≤ (μ : EReal) := by
    intro μ
    constructor
    · intro hfx
      have hmemF :
          (prodLinearEquiv_append (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) f)) := by
        exact
          (helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := f) (x := x) (μ := μ)).2
            ((mem_epigraph_univ_iff (f := f)).2 hfx)
      have hmemG :
          (prodLinearEquiv_append (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) g)) := by
        simpa [hImageEq] using hmemF
      exact
        (mem_epigraph_univ_iff (f := g)).1
          ((helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := g) (x := x) (μ := μ)).1 hmemG)
    · intro hgx
      have hmemG :
          (prodLinearEquiv_append (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) g)) := by
        exact
          (helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := g) (x := x) (μ := μ)).2
            ((mem_epigraph_univ_iff (f := g)).2 hgx)
      have hmemF :
          (prodLinearEquiv_append (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) f)) := by
        simpa [hImageEq] using hmemG
      exact
        (mem_epigraph_univ_iff (f := f)).1
          ((helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := f) (x := x) (μ := μ)).1 hmemF)
  apply le_antisymm
  · exact
      (EReal.le_of_forall_lt_iff_le).1
        (by
          intro μ hμ
          exact (hUpperCutsEq μ).2 (le_of_lt hμ))
  · exact
      (EReal.le_of_forall_lt_iff_le).1
        (by
          intro μ hμ
          exact (hUpperCutsEq μ).1 (le_of_lt hμ))

Helper for Text 19.0.9: equality of packed-coordinate transformed-epigraph images determines the underlying EReal : TypeEReal-valued function uniquely.

lemma helperForText_19_0_9_transformedImageCoord_eq_implies_function_eq
    {n : ℕ} {f g : (Fin n → ℝ) → EReal}
    (hImageEq :
      (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ))) :
    f = g := by
  funext x
  have hUpperCutsEq :
      ∀ μ : ℝ, f x ≤ (μ : EReal) ↔ g x ≤ (μ : EReal) := by
    intro μ
    constructor
    · intro hfx
      have hmemF :
          (prodLinearEquiv_append_coord (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) := by
        simpa [prodLinearEquiv_append_coord] using
          (helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := f) (x := x) (μ := μ)).2
            ((mem_epigraph_univ_iff (f := f)).2 hfx)
      have hmemG :
          (prodLinearEquiv_append_coord (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ)) := by
        simpa [hImageEq] using hmemF
      have hmemGEuclid :
          (prodLinearEquiv_append (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) g)) := by
        simpa [prodLinearEquiv_append_coord] using hmemG
      exact
        (mem_epigraph_univ_iff (f := g)).1
          ((helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := g) (x := x) (μ := μ)).1 hmemGEuclid)
    · intro hgx
      have hmemG :
          (prodLinearEquiv_append_coord (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ)) := by
        simpa [prodLinearEquiv_append_coord] using
          (helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := g) (x := x) (μ := μ)).2
            ((mem_epigraph_univ_iff (f := g)).2 hgx)
      have hmemF :
          (prodLinearEquiv_append_coord (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) := by
        simpa [hImageEq] using hmemG
      have hmemFEuclid :
          (prodLinearEquiv_append (n := n) (x, μ)) ∈
            (((fun p => prodLinearEquiv_append (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) f)) := by
        simpa [prodLinearEquiv_append_coord] using hmemF
      exact
        (mem_epigraph_univ_iff (f := f)).1
          ((helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
            (n := n) (f := f) (x := x) (μ := μ)).1 hmemFEuclid)
  apply le_antisymm
  · exact
      (EReal.le_of_forall_lt_iff_le).1
        (by
          intro μ hμ
          exact (hUpperCutsEq μ).2 (le_of_lt hμ))
  · exact
      (EReal.le_of_forall_lt_iff_le).1
        (by
          intro μ hμ
          exact (hUpperCutsEq μ).1 (le_of_lt hμ))

Helper for Text 19.0.9: the lower-bound guard on the unpacked scalar coordinate is a polyhedral halfspace in packed coordinates.

lemma helperForText_19_0_9_lastCoordGuard_polyhedral
    {n : ℕ} :
    IsPolyhedralConvexSet (n + 1)
      {z : Fin (n + 1) → ℝ |
        0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2} := by
  classical
  let b : Fin 1 → Fin (n + 1) → ℝ :=
    fun _ =>
      prodLinearEquiv_append_coord (n := n)
        ((fun _ : Fin n => (0 : ℝ)), (-1 : ℝ))
  let β : Fin 1 → ℝ := fun _ => 0
  refine ⟨Fin 1, inferInstance, b, β, ?_⟩
  ext z
  constructor
  · intro hz
    refine Set.mem_iInter.2 ?_
    intro i
    have hdot :
        dotProduct z (b i) =
          -((prodLinearEquiv_append_coord (n := n)).symm z).2 := by
      have hdotRaw :=
        helperForText_19_0_9_dotPacked_point
          (n := n) (m := 1)
          (b := fun _ : Fin 1 => (fun _ : Fin n => (0 : ℝ)))
          i z
      simpa [b, dotProduct] using hdotRaw
    have hle : dotProduct z (b i) ≤ β i := by
      have hneg : -((prodLinearEquiv_append_coord (n := n)).symm z).2 ≤ 0 :=
        neg_nonpos.mpr hz
      simpa [β, hdot] using hneg
    simpa [closedHalfSpaceLE, b, β] using hle
  · intro hz
    have hz0 : z ∈ closedHalfSpaceLE (n + 1) (b 0) (β 0) :=
      Set.mem_iInter.1 hz 0
    have hdot :
        dotProduct z (b 0) =
          -((prodLinearEquiv_append_coord (n := n)).symm z).2 := by
      have hdotRaw :=
        helperForText_19_0_9_dotPacked_point
          (n := n) (m := 1)
          (b := fun _ : Fin 1 => (fun _ : Fin n => (0 : ℝ)))
          0 z
      simpa [b, dotProduct] using hdotRaw
    have hle : -((prodLinearEquiv_append_coord (n := n)).symm z).2 ≤ 0 := by
      simpa [closedHalfSpaceLE, b, β, hdot] using hz0
    exact neg_nonpos.mp hle

Helper for Text 19.0.9: the guarded packed-normal constraint form is polyhedral.

lemma helperForText_19_0_9_guardedSplitConstraintSet_polyhedral
    {n k m : ℕ} (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) :
    IsPolyhedralConvexSet (n + 1)
      (({z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, (i : ℕ) < k →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, k ≤ (i : ℕ) →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
        (if k = 0 then
          {z : Fin (n + 1) → ℝ |
            0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
        else Set.univ)) := by
  have hactive :
      IsPolyhedralConvexSet (n + 1)
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, (i : ℕ) < k →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} := by
    classical
    let ι : Type := {i : Fin m // (i : ℕ) < k}
    let a : ι → Fin (n + 1) → ℝ :=
      fun i => prodLinearEquiv_append_coord (n := n) (b i.1, (-1 : ℝ))
    let α : ι → ℝ := fun i => β i.1
    refine ⟨ι, inferInstance, a, α, ?_⟩
    ext z
    constructor
    · intro hz
      refine Set.mem_iInter.2 ?_
      intro i
      have hz_i : dotProduct z
          (prodLinearEquiv_append_coord (n := n) (b i.1, (-1 : ℝ))) ≤ β i.1 :=
        hz i.1 i.2
      simpa [closedHalfSpaceLE, a, α] using hz_i
    · intro hz i hi
      have hz_i : z ∈ closedHalfSpaceLE (n + 1) (a ⟨i, hi⟩) (α ⟨i, hi⟩) :=
        Set.mem_iInter.1 hz ⟨i, hi⟩
      simpa [closedHalfSpaceLE, a, α] using hz_i
  have hdomain :
      IsPolyhedralConvexSet (n + 1)
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, k ≤ (i : ℕ) →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i} := by
    classical
    let ι : Type := {i : Fin m // k ≤ (i : ℕ)}
    let a : ι → Fin (n + 1) → ℝ :=
      fun i => prodLinearEquiv_append_coord (n := n) (b i.1, (0 : ℝ))
    let α : ι → ℝ := fun i => β i.1
    refine ⟨ι, inferInstance, a, α, ?_⟩
    ext z
    constructor
    · intro hz
      refine Set.mem_iInter.2 ?_
      intro i
      have hz_i : dotProduct z
          (prodLinearEquiv_append_coord (n := n) (b i.1, (0 : ℝ))) ≤ β i.1 :=
        hz i.1 i.2
      simpa [closedHalfSpaceLE, a, α] using hz_i
    · intro hz i hi
      have hz_i : z ∈ closedHalfSpaceLE (n + 1) (a ⟨i, hi⟩) (α ⟨i, hi⟩) :=
        Set.mem_iInter.1 hz ⟨i, hi⟩
      simpa [closedHalfSpaceLE, a, α] using hz_i
  have hsplit :
      IsPolyhedralConvexSet (n + 1)
        ({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, (i : ℕ) < k →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, k ≤ (i : ℕ) →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) :=
    helperForTheorem_19_1_polyhedral_inter hactive hdomain
  by_cases hk0 : k = 0
  · have hguard :
      IsPolyhedralConvexSet (n + 1)
        {z : Fin (n + 1) → ℝ |
          0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2} :=
      helperForText_19_0_9_lastCoordGuard_polyhedral (n := n)
    have hinter :
        IsPolyhedralConvexSet (n + 1)
          (({z : Fin (n + 1) → ℝ |
              ∀ i : Fin m, (i : ℕ) < k →
                dotProduct z
                  (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
            {z : Fin (n + 1) → ℝ |
              ∀ i : Fin m, k ≤ (i : ℕ) →
                dotProduct z
                  (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
            {z : Fin (n + 1) → ℝ |
              0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}) :=
      helperForTheorem_19_1_polyhedral_inter hsplit hguard
    simpa [hk0] using hinter
  · simpa [hk0, Set.inter_univ] using hsplit

Helper for Text 19.0.9: packed normals with last coordinate -1 : ℤ-1 decode to the split affine expression after unpacking coordinates.

lemma helperForText_19_0_9_dotPacked_point_finCases_normalForm
    {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m)
    (y : Fin (n + 1) → ℝ) :
    dotProduct y (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) =
      dotProduct (b i) ((prodLinearEquiv_append_coord (n := n)).symm y).1 -
        ((prodLinearEquiv_append_coord (n := n)).symm y).2 := by
  simpa using helperForText_19_0_9_dotPacked_point (n := n) (m := m) (b := b) i y

Helper for Text 19.0.9: packed-direction normals with last coordinate 0 : ℕ0 decode to the base-coordinate dot product after unpacking.

lemma helperForText_19_0_9_dotPacked_direction_finCases_normalForm
    {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m)
    (y : Fin (n + 1) → ℝ) :
    dotProduct y (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) =
      dotProduct (b i) ((prodLinearEquiv_append_coord (n := n)).symm y).1 := by
  simpa using helperForText_19_0_9_dotPacked_direction (n := n) (m := m) (b := b) i y

Helper for Text 19.0.9: evaluating the packed normal (sorry, -1) : ?m.1 × ℤ(Unknown identifier `b_i`b_i, -1) at base coordinates recovers the coefficient function Unknown identifier `b_i`b_i.

lemma helperForText_19_0_9_packedNormal_point_eq_finCases
    {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (j : Fin n) :
    (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) (Fin.castSucc j) = b i j := by
  exact
    (helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
      (n := n) (x0 := b i) (μ0 := (-1 : ℝ)) (j0 := j)).symm

Helper for Text 19.0.9: evaluating the packed normal (sorry, 0) : ?m.1 × ℕ(Unknown identifier `b_i`b_i, 0) at base coordinates recovers the coefficient function Unknown identifier `b_i`b_i.

lemma helperForText_19_0_9_packedNormal_direction_eq_finCases
    {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m) (j : Fin n) :
    (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) (Fin.castSucc j) = b i j := by
  exact
    (helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
      (n := n) (x0 := b i) (μ0 := (0 : ℝ)) (j0 := j)).symm

Helper for Text 19.0.9: an epigraph upper bound on the represented value at Unknown identifier `x`x forces Unknown identifier `x`x to satisfy all domain-side inequalities.

lemma helperForText_19_0_9_representation_le_implies_domain_membership
    {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ}
    {x : Fin n → ℝ} {μ : ℝ}
    (hgμ :
      ((sSup {r : ℝ |
          ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
        indicatorFunction
          (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
            (∑ j, y j * b i j) ≤ β i})
          x ≤ (μ : EReal)) :
    x ∈ ({y | ∀ i : Fin m, k ≤ (i : ℕ) → (∑ j, y j * b i j) ≤ β i} : Set (Fin n → ℝ)) := by
  by_contra hxC
  have htop : (⊤ : EReal) ≤ (μ : EReal) := by
    simp [indicatorFunction, hxC] at hgμ
  exact (not_top_le_coe μ) htop

Helper for Text 19.0.9: the same represented upper bound yields an upper bound on the corresponding affine supremum term.

lemma helperForText_19_0_9_representation_le_implies_sup_bound
    {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ}
    {x : Fin n → ℝ} {μ : ℝ}
    (hgμ :
      ((sSup {r : ℝ |
          ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
        indicatorFunction
          (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
            (∑ j, y j * b i j) ≤ β i})
          x ≤ (μ : EReal)) :
    sSup {r : ℝ | ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} ≤ μ := by
  have hxC :
      x ∈ ({y | ∀ i : Fin m, k ≤ (i : ℕ) → (∑ j, y j * b i j) ≤ β i} : Set (Fin n → ℝ)) :=
    helperForText_19_0_9_representation_le_implies_domain_membership
      (n := n) (k := k) (m := m) (b := b) (β := β) (x := x) (μ := μ) hgμ
  have hsSup_leE :
      ((sSup {r : ℝ | ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) ≤
        (μ : EReal) := by
    simpa [indicatorFunction, hxC] using hgμ
  exact_mod_cast hsSup_leE

Helper for Text 19.0.9: each active affine piece (Unknown identifier `i`sorry < sorry : Propi < Unknown identifier `k`k) is bounded above by Unknown identifier `μ`μ whenever the represented value at Unknown identifier `x`x is bounded by Unknown identifier `μ`μ.

lemma helperForText_19_0_9_representation_le_implies_active_affine_bound
    {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ}
    {x : Fin n → ℝ} {μ : ℝ}
    (hgμ :
      ((sSup {r : ℝ |
          ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
        indicatorFunction
          (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
            (∑ j, y j * b i j) ≤ β i})
          x ≤ (μ : EReal))
    (i : Fin m) (hi : (i : ℕ) < k) :
    (∑ j, x j * b i j) - β i ≤ μ := by
  let A : Set ℝ :=
    {r : ℝ | ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i}
  have hsSup_le : sSup A ≤ μ := by
    simpa [A] using
      helperForText_19_0_9_representation_le_implies_sup_bound
        (n := n) (k := k) (m := m) (b := b) (β := β) (x := x) (μ := μ) hgμ
  have hA_sub : A ⊆ Set.range (fun i : Fin m => (∑ j, x j * b i j) - β i) := by
    intro r hr
    rcases hr with ⟨i', _hi', rfl⟩
    exact ⟨i', rfl⟩
  have hA_finite : Set.Finite A :=
    (Set.finite_range (fun i : Fin m => (∑ j, x j * b i j) - β i)).subset hA_sub
  have hA_bdd : BddAbove A := hA_finite.bddAbove
  have hi_memA : (∑ j, x j * b i j) - β i ∈ A := by
    exact ⟨i, hi, rfl⟩
  exact le_trans (le_csSup hA_bdd hi_memA) hsSup_le

Helper for Text 19.0.9: dot products against the Fin.cases.{u_1} {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) : motive iFin.cases split normals expand into the zero-coordinate term plus the Unknown identifier `succ`succ-indexed base sum.

lemma helperForText_19_0_9_dotFinCasesNormals_unpacked_normalForm
    {n m : ℕ} {b : Fin m → Fin n → ℝ} (i : Fin m)
    (z : Fin (n + 1) → ℝ) :
    dotProduct z (Fin.cases (-1 : ℝ) (b i)) =
      z 0 * (-1 : ℝ) + ∑ j : Fin n, z j.succ * b i j ∧
    dotProduct z (Fin.cases (0 : ℝ) (b i)) =
      ∑ j : Fin n, z j.succ * b i j := by
  constructor
  ·
    calc
      dotProduct z (Fin.cases (-1 : ℝ) (b i))
          = ∑ t : Fin (n + 1), z t * Fin.cases (-1 : ℝ) (b i) t := by
              simp [dotProduct]
      _ = z 0 * (-1 : ℝ) + ∑ j : Fin n, z j.succ * Fin.cases (-1 : ℝ) (b i) j.succ := by
            simp [Fin.sum_univ_succ]
      _ = z 0 * (-1 : ℝ) + ∑ j : Fin n, z j.succ * b i j := by
            simp [Fin.cases_succ]
  ·
    calc
      dotProduct z (Fin.cases (0 : ℝ) (b i))
          = ∑ t : Fin (n + 1), z t * Fin.cases (0 : ℝ) (b i) t := by
              simp [dotProduct]
      _ = z 0 * (0 : ℝ) + ∑ j : Fin n, z j.succ * Fin.cases (0 : ℝ) (b i) j.succ := by
            simp [Fin.sum_univ_succ]
      _ = ∑ j : Fin n, z j.succ * b i j := by
            simp [Fin.cases_succ]

Helper for Text 19.0.9: for Unknown identifier `n`sorry = 1 : Propn = 1, , and zero coefficients, the packed point corresponding to (sorry, sorry) = (-1, 0) : Prop(Unknown identifier `x`x, Unknown identifier `μ`μ) = (-1, 0) belongs to the transformed epigraph image of the represented function.

lemma helperForText_19_0_9_counterexample_mem_transformedImage
    :
    let g : (Fin 1 → ℝ) → EReal :=
      fun x =>
        ((sSup {r : ℝ |
            ∃ i : Fin 1, (i : ℕ) < 1 ∧ r = (∑ j, x j * (0 : ℝ)) - (0 : ℝ)} : ℝ) : EReal) +
          indicatorFunction
            (C := {y : Fin 1 → ℝ | ∀ i : Fin 1, 1 ≤ (i : ℕ) →
              (∑ j, y j * (0 : ℝ)) ≤ (0 : ℝ)})
            x
    let z0 : Fin 2 → ℝ :=
      prodLinearEquiv_append (n := 1) ((fun _ : Fin 1 => (-1 : ℝ)), (0 : ℝ))
    z0 ∈ (((fun p => prodLinearEquiv_append (n := 1) p) ''
      epigraph (Set.univ : Set (Fin 1 → ℝ)) g) : Set (Fin 2 → ℝ)) := by
  intro g z0
  have hmemEpi :
      ((fun _ : Fin 1 => (-1 : ℝ)), (0 : ℝ)) ∈
        epigraph (Set.univ : Set (Fin 1 → ℝ)) g := by
    exact (mem_epigraph_univ_iff (f := g)).2 (by simp [g, indicatorFunction])
  refine ⟨((fun _ : Fin 1 => (-1 : ℝ)), (0 : ℝ)), ?_, rfl⟩
  exact hmemEpi

Helper for Text 19.0.9: under the same concrete data, the point above violates the split Fin.cases.{u_1} {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) : motive iFin.cases affine-constraint family.

lemma helperForText_19_0_9_counterexample_not_mem_finCases_split
    :
    let z0 : Fin 2 → ℝ :=
      prodLinearEquiv_append (n := 1) ((fun _ : Fin 1 => (-1 : ℝ)), (0 : ℝ))
    z0 ∉
      ({z : Fin 2 → ℝ |
          ∀ i : Fin 1, (i : ℕ) < 1 →
            dotProduct z (Fin.cases (-1 : ℝ) (fun _ : Fin 1 => (0 : ℝ))) ≤ (0 : ℝ)} ∩
        {z : Fin 2 → ℝ |
          ∀ i : Fin 1, 1 ≤ (i : ℕ) →
            dotProduct z (Fin.cases (0 : ℝ) (fun _ : Fin 1 => (0 : ℝ))) ≤ (0 : ℝ)}) := by
  intro z0 hz
  have hlt : (((0 : Fin 1) : Fin 1) : ℕ) < 1 := by simp
  have hineq :
      dotProduct z0 (Fin.cases (-1 : ℝ) (fun _ : Fin 1 => (0 : ℝ))) ≤ (0 : ℝ) :=
    hz.1 0 hlt
  have hdot :
      dotProduct z0 (Fin.cases (-1 : ℝ) (fun _ : Fin 1 => (0 : ℝ))) = (1 : ℝ) := by
    have h0 : z0 0 = (-1 : ℝ) := by
      simpa [z0, prodLinearEquiv_append_coord] using
        (helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
          (n := 1) (x0 := fun _ : Fin 1 => (-1 : ℝ)) (μ0 := (0 : ℝ)) (j0 := (0 : Fin 1))).symm
    calc
      dotProduct z0 (Fin.cases (-1 : ℝ) (fun _ : Fin 1 => (0 : ℝ)))
          = z0 0 * (-1 : ℝ) + ∑ j : Fin 1, z0 j.succ * (0 : ℝ) := by
              simpa using
                (helperForText_19_0_9_dotFinCasesNormals_unpacked_normalForm
                  (n := 1) (m := 1) (b := fun _ : Fin 1 => (fun _ : Fin 1 => (0 : ℝ)))
                  (i := (0 : Fin 1)) z0).1
      _ = (1 : ℝ) := by simp [h0]
  linarith [hineq, hdot]

Helper for Text 19.0.9: the concrete one-dimensional witness separates the transformed epigraph image from the split Fin.cases.{u_1} {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) : motive iFin.cases constraints.

lemma helperForText_19_0_9_counterexample_transformedImage_ne_finCases_split
    :
    let g : (Fin 1 → ℝ) → EReal :=
      fun x =>
        ((sSup {r : ℝ |
            ∃ i : Fin 1, (i : ℕ) < 1 ∧ r = (∑ j, x j * (0 : ℝ)) - (0 : ℝ)} : ℝ) : EReal) +
          indicatorFunction
            (C := {y : Fin 1 → ℝ | ∀ i : Fin 1, 1 ≤ (i : ℕ) →
              (∑ j, y j * (0 : ℝ)) ≤ (0 : ℝ)})
            x
    let Simg : Set (Fin 2 → ℝ) :=
      ((fun p => prodLinearEquiv_append (n := 1) p) ''
        epigraph (Set.univ : Set (Fin 1 → ℝ)) g)
    let Ssplit : Set (Fin 2 → ℝ) :=
      ({z : Fin 2 → ℝ |
          ∀ i : Fin 1, (i : ℕ) < 1 →
            dotProduct z (Fin.cases (-1 : ℝ) (fun _ : Fin 1 => (0 : ℝ))) ≤ (0 : ℝ)} ∩
        {z : Fin 2 → ℝ |
          ∀ i : Fin 1, 1 ≤ (i : ℕ) →
            dotProduct z (Fin.cases (0 : ℝ) (fun _ : Fin 1 => (0 : ℝ))) ≤ (0 : ℝ)})
    Simg ≠ Ssplit := by
  intro g Simg Ssplit hEq
  let z0 : Fin 2 → ℝ :=
    prodLinearEquiv_append (n := 1) ((fun _ : Fin 1 => (-1 : ℝ)), (0 : ℝ))
  have hzSimg : z0 ∈ Simg := by
    simpa [Simg, z0, g] using helperForText_19_0_9_counterexample_mem_transformedImage
  have hzSsplit : z0 ∈ Ssplit := by
    simpa [hEq] using hzSimg
  have hzNotSsplit : z0 ∉ Ssplit := by
    simpa [Ssplit, z0] using helperForText_19_0_9_counterexample_not_mem_finCases_split
  exact hzNotSsplit hzSsplit

Helper for Text 19.0.9: a max-affine-plus-indicator representation has transformed epigraph image equal to packed-normal constraints with the Unknown identifier `k`sorry = 0 : Propk = 0 last-coordinate guard.

lemma helperForText_19_0_9_representation_transformedImage_eq_constraints_with_lastCoord_guard
    {n k m : ℕ} (hk : k ≤ m) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ) :
    let g : (Fin n → ℝ) → EReal :=
      fun x =>
        ((sSup {r : ℝ |
            ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
          indicatorFunction
            (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
              (∑ j, y j * b i j) ≤ β i})
            x
    let Simg : Set (Fin (n + 1) → ℝ) :=
      ((fun p => prodLinearEquiv_append (n := n) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) g)
    let Ssplit : Set (Fin (n + 1) → ℝ) :=
      ({z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, (i : ℕ) < k →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m, k ≤ (i : ℕ) →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i})
    let Sguard : Set (Fin (n + 1) → ℝ) :=
      {z : Fin (n + 1) → ℝ |
        0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
    Simg = Ssplit ∩ (if k = 0 then Sguard else Set.univ) := by
  intro g Simg Ssplit Sguard
  ext z
  constructor
  · intro hzImg
    let xμ : (Fin n → ℝ) × ℝ := (prodLinearEquiv_append_coord (n := n)).symm z
    let x : Fin n → ℝ := xμ.1
    let μ : ℝ := xμ.2
    let C : Set (Fin n → ℝ) :=
      {y | ∀ i : Fin m, k ≤ (i : ℕ) → (∑ j, y j * b i j) ≤ β i}
    have hzPackedCoord :
        prodLinearEquiv_append_coord (n := n) (x, μ) = z := by
      change
        prodLinearEquiv_append_coord (n := n)
            ((prodLinearEquiv_append_coord (n := n)).symm z) = z
      simp
    have hzImgCoord :
        z ∈
          ((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) g) := by
      simpa [Simg, prodLinearEquiv_append_coord] using hzImg
    have hzImgPackedCoord :
        prodLinearEquiv_append_coord (n := n) (x, μ) ∈
          ((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) g) := by
      simpa [hzPackedCoord] using hzImgCoord
    have hxμEpi : (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) g := by
      rcases hzImgPackedCoord with ⟨p, hpEpi, hpMap⟩
      have hp : p = (x, μ) :=
        (prodLinearEquiv_append_coord (n := n)).injective hpMap
      simpa [hp] using hpEpi
    have hgμ : g x ≤ (μ : EReal) :=
      (mem_epigraph_univ_iff (f := g)).1 hxμEpi
    have hxC : x ∈ C := by
      exact
        helperForText_19_0_9_representation_le_implies_domain_membership
          (n := n) (k := k) (m := m) (b := b) (β := β) (x := x) (μ := μ)
          (by simpa [g, C] using hgμ)
    have hzActive :
        ∀ i : Fin m, (i : ℕ) < k →
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i := by
      intro i hi
      have hAffine :
          (∑ j, x j * b i j) - β i ≤ μ := by
        exact
          helperForText_19_0_9_representation_le_implies_active_affine_bound
            (n := n) (k := k) (m := m) (b := b) (β := β) (x := x) (μ := μ)
            (by simpa [g, C] using hgμ) i hi
      have hdot :
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) =
            (∑ j, x j * b i j) - μ := by
        calc
          dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ)))
              = dotProduct (b i) x - μ := by
                  simpa [x, μ] using
                    (helperForText_19_0_9_dotPacked_point
                      (n := n) (m := m) (b := b) i z)
          _ = dotProduct x (b i) - μ := by rw [dotProduct_comm]
          _ = (∑ j, x j * b i j) - μ := by simp [dotProduct]
      linarith [hAffine, hdot]
    have hzDomain :
        ∀ i : Fin m, k ≤ (i : ℕ) →
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i := by
      intro i hi
      have hDomainIneq : (∑ j, x j * b i j) ≤ β i := hxC i hi
      have hdot :
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) =
            (∑ j, x j * b i j) := by
        calc
          dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ)))
              = dotProduct (b i) x := by
                  simpa [x] using
                    (helperForText_19_0_9_dotPacked_direction
                      (n := n) (m := m) (b := b) i z)
          _ = dotProduct x (b i) := by rw [dotProduct_comm]
          _ = (∑ j, x j * b i j) := by simp [dotProduct]
      simpa [hdot] using hDomainIneq
    have hzSplit : z ∈ Ssplit := by
      exact ⟨hzActive, hzDomain⟩
    have hzGuard :
        z ∈ (if k = 0 then Sguard else Set.univ) := by
      by_cases hk0 : k = 0
      · have hsSupLe :
          sSup {r : ℝ |
              ∃ i : Fin m, (i : ℕ) < k ∧
                r = (∑ j, x j * b i j) - β i} ≤ μ := by
          exact
            helperForText_19_0_9_representation_le_implies_sup_bound
              (n := n) (k := k) (m := m) (b := b) (β := β) (x := x) (μ := μ)
              (by simpa [g, C] using hgμ)
        have hμ_nonneg : 0 ≤ μ := by
          have hsSupZero :
              sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} = 0 := by
            simp [hk0]
          simpa [hsSupZero] using hsSupLe
        have hzSguard : z ∈ Sguard := by
          simpa [Sguard, x, μ, xμ] using hμ_nonneg
        simpa [hk0] using hzSguard
      · simp [hk0]
    exact ⟨hzSplit, hzGuard⟩
  · intro hz
    have hzSplit : z ∈ Ssplit := hz.1
    have hzGuard : z ∈ (if k = 0 then Sguard else Set.univ) := hz.2
    let xμ : (Fin n → ℝ) × ℝ := (prodLinearEquiv_append_coord (n := n)).symm z
    let x : Fin n → ℝ := xμ.1
    let μ : ℝ := xμ.2
    let C : Set (Fin n → ℝ) :=
      {y | ∀ i : Fin m, k ≤ (i : ℕ) → (∑ j, y j * b i j) ≤ β i}
    let A : Set ℝ :=
      {r : ℝ | ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i}
    have hzActive :
        ∀ i : Fin m, (i : ℕ) < k →
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i :=
      hzSplit.1
    have hzDomain :
        ∀ i : Fin m, k ≤ (i : ℕ) →
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i :=
      hzSplit.2
    have hxC : x ∈ C := by
      intro i hi
      have hPacked :
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i :=
        hzDomain i hi
      have hdot :
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) =
            (∑ j, x j * b i j) := by
        calc
          dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ)))
              = dotProduct (b i) x := by
                  simpa [x] using
                    (helperForText_19_0_9_dotPacked_direction
                      (n := n) (m := m) (b := b) i z)
          _ = dotProduct x (b i) := by rw [dotProduct_comm]
          _ = (∑ j, x j * b i j) := by simp [dotProduct]
      simpa [hdot] using hPacked
    have hμ_nonneg_if_k0 : k = 0 → 0 ≤ μ := by
      intro hk0
      have hzSguard : z ∈ Sguard := by
        simpa [hk0] using hzGuard
      simpa [Sguard, μ, xμ] using hzSguard
    have hA_upper : ∀ r ∈ A, r ≤ μ := by
      intro r hr
      rcases hr with ⟨i, hi, rfl⟩
      have hPacked :
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i :=
        hzActive i hi
      have hdot :
          dotProduct z
            (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) =
            (∑ j, x j * b i j) - μ := by
        calc
          dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ)))
              = dotProduct (b i) x - μ := by
                  simpa [x, μ] using
                    (helperForText_19_0_9_dotPacked_point
                      (n := n) (m := m) (b := b) i z)
          _ = dotProduct x (b i) - μ := by rw [dotProduct_comm]
          _ = (∑ j, x j * b i j) - μ := by simp [dotProduct]
      linarith [hPacked, hdot]
    have hsSup_le : sSup A ≤ μ := by
      by_cases hk0 : k = 0
      · have hμ_nonneg : 0 ≤ μ := hμ_nonneg_if_k0 hk0
        have hAempty : A = ∅ := by
          ext r
          constructor
          · intro hr
            rcases hr with ⟨i, hi, _⟩
            have hi0 : (i : ℕ) < 0 := by simp [hk0] at hi ⊢
            exact (Nat.not_lt_zero (i : ℕ)) hi0
          · intro hr
            exact False.elim (Set.notMem_empty r hr)
        have hsSupZero : sSup A = 0 := by
          simp [hAempty]
        simpa [hsSupZero] using hμ_nonneg
      · have hkpos : 0 < k := Nat.pos_of_ne_zero hk0
        have hmpos : 0 < m := lt_of_lt_of_le hkpos hk
        let i0 : Fin m := ⟨0, hmpos⟩
        have hi0 : (i0 : ℕ) < k := by
          simpa [i0] using hkpos
        have hA_nonempty : A.Nonempty := by
          refine ⟨(∑ j, x j * b i0 j) - β i0, ?_⟩
          exact ⟨i0, hi0, rfl⟩
        exact csSup_le hA_nonempty hA_upper
    have hsSup_le_EReal : ((sSup A : ℝ) : EReal) ≤ (μ : EReal) := by
      exact_mod_cast hsSup_le
    have hIndicator_zero : indicatorFunction (C := C) x = (0 : EReal) := by
      simp [indicatorFunction, hxC]
    have hgμ : g x ≤ (μ : EReal) := by
      simpa [g, A, C, hIndicator_zero] using hsSup_le_EReal
    have hxμEpi : (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) g :=
      (mem_epigraph_univ_iff (f := g)).2 hgμ
    have hzPackedCoord :
        prodLinearEquiv_append_coord (n := n) (x, μ) = z := by
      change
        prodLinearEquiv_append_coord (n := n)
            ((prodLinearEquiv_append_coord (n := n)).symm z) = z
      simp
    have hzImageCoord :
        prodLinearEquiv_append_coord (n := n) (x, μ) ∈
          ((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) g) := by
      exact ⟨(x, μ), hxμEpi, rfl⟩
    have hzImgCoord :
        z ∈
          ((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) g) := by
      simpa [hzPackedCoord] using hzImageCoord
    simpa [Simg, prodLinearEquiv_append_coord] using hzImgCoord

Helper for Text 19.0.9: polyhedrality of the transformed-epigraph image implies convexity of the represented function on Unknown identifier `univ`univ.

lemma helperForText_19_0_9_convexFunctionOn_of_polyhedralTransformedEpigraph
    {n : ℕ} {g : (Fin n → ℝ) → EReal}
    (hpoly :
      IsPolyhedralConvexSet (n + 1)
        (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ))) :
    ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) g := by
  let e := prodLinearEquiv_append_coord (n := n)
  have hpolyCoord :
      IsPolyhedralConvexSet (n + 1)
        ((fun p => e p) '' epigraph (Set.univ : Set (Fin n → ℝ)) g) := by
    simpa [e, prodLinearEquiv_append_coord] using hpoly
  have hconvImage :
      Convex ℝ ((fun p => e p) '' epigraph (Set.univ : Set (Fin n → ℝ)) g) :=
    helperForTheorem_19_1_polyhedral_isConvex
      (n := n + 1)
      (C := ((fun p => e p) '' epigraph (Set.univ : Set (Fin n → ℝ)) g))
      hpolyCoord
  have hconvPreimage :
      Convex ℝ (((fun p => e p) ⁻¹'
        (((fun p => e p) '' epigraph (Set.univ : Set (Fin n → ℝ)) g)))) := by
    simpa using hconvImage.linear_preimage e.toLinearMap
  have hpreimageEq :
      ((fun p => e p) ⁻¹' (((fun p => e p) '' epigraph (Set.univ : Set (Fin n → ℝ)) g))) =
        epigraph (Set.univ : Set (Fin n → ℝ)) g :=
    Set.preimage_image_eq _ e.injective
  simpa [ConvexFunctionOn, e, hpreimageEq] using hconvPreimage

Helper for Text 19.0.9: in a nonempty raw halfspace presentation of the transformed epigraph image, each raw normal has nonpositive last coordinate.

lemma helperForText_19_0_9_rawHalfspaces_lastCoord_nonpos
    {n m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin (n + 1) → ℝ} {α : Fin m → ℝ}
    (hRaw :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        ⋂ i, closedHalfSpaceLE (n + 1) (a i) (α i))
    (hNonempty :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)).Nonempty) :
    ∀ i : Fin m, a i (Fin.last n) ≤ 0 := by
  have hRawCoord :
      (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        ⋂ i, closedHalfSpaceLE (n + 1) (a i) (α i) := by
    simpa [prodLinearEquiv_append_coord] using hRaw
  have hNonemptyCoord :
      (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)).Nonempty := by
    simpa [prodLinearEquiv_append_coord] using hNonempty
  rcases
    helperForText_19_0_9_nonempty_transformedEpigraphImage_unpack
      (n := n) (f := f) hNonempty with
    ⟨x0, μ0, hx0μ0⟩
  have hz0 :
      prodLinearEquiv_append_coord (n := n) (x0, μ0) ∈
        (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) := by
    refine ⟨(x0, μ0), ?_, rfl⟩
    exact (mem_epigraph_univ_iff (f := f)).2 hx0μ0
  intro i
  by_contra hnonpos
  have hcpos : 0 < a i (Fin.last n) := lt_of_not_ge hnonpos
  let c : ℝ := a i (Fin.last n)
  let d : ℝ := dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i)
  have hz0Inter :
      prodLinearEquiv_append_coord (n := n) (x0, μ0) ∈
        ⋂ j : Fin m, closedHalfSpaceLE (n + 1) (a j) (α j) := by
    simpa [hRawCoord] using hz0
  have hz0Ineq :
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i) ≤ α i := by
    have hz0i :
        prodLinearEquiv_append_coord (n := n) (x0, μ0) ∈
          closedHalfSpaceLE (n + 1) (a i) (α i) :=
      Set.mem_iInter.1 hz0Inter i
    simpa [closedHalfSpaceLE] using hz0i
  have hnum_nonneg : 0 ≤ α i - d := by
    have hd_le : d ≤ α i := by
      simpa [d] using hz0Ineq
    linarith
  let t : ℝ := (α i - d) / c + 1
  have hcpos_c : 0 < c := by
    simpa [c] using hcpos
  have ht_nonneg : 0 ≤ t := by
    have hdiv_nonneg : 0 ≤ (α i - d) / c := by
      exact div_nonneg hnum_nonneg (le_of_lt hcpos_c)
    have ht_eq : t = (α i - d) / c + 1 := rfl
    linarith [hdiv_nonneg, ht_eq]
  have hz_t_append :
      prodLinearEquiv_append (n := n) (x0, μ0 + t) ∈
        ((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) :=
    helperForText_19_0_9_transformedEpigraphImage_upwardClosed_lastCoord
      (n := n) (f := f) (x := x0) (μ := μ0) (t := t)
      (by simpa [prodLinearEquiv_append_coord] using hz0) ht_nonneg
  have hz_t :
      prodLinearEquiv_append_coord (n := n) (x0, μ0 + t) ∈
        ((fun p => prodLinearEquiv_append_coord (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
    simpa [prodLinearEquiv_append_coord] using hz_t_append
  have hz_tInter :
      prodLinearEquiv_append_coord (n := n) (x0, μ0 + t) ∈
        ⋂ j : Fin m, closedHalfSpaceLE (n + 1) (a j) (α j) := by
    simpa [hRawCoord] using hz_t
  have hz_tIneq :
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0 + t)) (a i) ≤ α i := by
    have hz_ti :
        prodLinearEquiv_append_coord (n := n) (x0, μ0 + t) ∈
          closedHalfSpaceLE (n + 1) (a i) (α i) :=
      Set.mem_iInter.1 hz_tInter i
    simpa [closedHalfSpaceLE] using hz_ti
  let q : (Fin n → ℝ) × ℝ := (prodLinearEquiv_append_coord (n := n)).symm (a i)
  have hdot_t_coord :
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0 + t)) (a i) =
        dotProduct x0 q.1 + (μ0 + t) * q.2 := by
    calc
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0 + t)) (a i)
          = dotProduct
              (prodLinearEquiv_append_coord (n := n) (x0, μ0 + t))
              (prodLinearEquiv_append_coord (n := n) q) := by
              simp [q]
      _ = dotProduct x0 q.1 + (μ0 + t) * q.2 := by
            simpa [q] using
              helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord
                (n := n) (p := (x0, μ0 + t)) (q := q)
  have hdot_0_coord :
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i) =
        dotProduct x0 q.1 + μ0 * q.2 := by
    calc
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i)
          = dotProduct
              (prodLinearEquiv_append_coord (n := n) (x0, μ0))
              (prodLinearEquiv_append_coord (n := n) q) := by
              simp [q]
      _ = dotProduct x0 q.1 + μ0 * q.2 := by
            simpa [q] using
              helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord
                (n := n) (p := (x0, μ0)) (q := q)
  have hd_eq : d = dotProduct x0 q.1 + μ0 * q.2 := by
    simpa [d, prodLinearEquiv_append_coord] using hdot_0_coord
  have hq2_eq_c : q.2 = c := by
    have hqlast :
        q.2 = (prodLinearEquiv_append_coord (n := n) q) (Fin.last n) := by
      simpa using
        helperForText_19_0_9_prodLinearEquivAppendCoord_last
          (n := n) (x0 := q.1) (μ0 := q.2)
    have hqa :
        (prodLinearEquiv_append_coord (n := n) q) (Fin.last n) = a i (Fin.last n) := by
      have hqa_all :
          prodLinearEquiv_append_coord (n := n) q = a i := by
        simp [q]
      exact congrArg (fun v : Fin (n + 1) → ℝ => v (Fin.last n)) hqa_all
    calc
      q.2 = (prodLinearEquiv_append_coord (n := n) q) (Fin.last n) := hqlast
      _ = a i (Fin.last n) := hqa
      _ = c := by rfl
  have hdot_t :
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0 + t)) (a i) = d + t * c := by
    calc
      dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0 + t)) (a i)
          = dotProduct x0 q.1 + (μ0 + t) * q.2 := by
              exact hdot_t_coord
      _ = (dotProduct x0 q.1 + μ0 * q.2) + t * q.2 := by ring
      _ = d + t * q.2 := by rw [hd_eq]
      _ = d + t * c := by rw [hq2_eq_c]
  have hbound : d + t * c ≤ α i := by
    simpa [hdot_t] using hz_tIneq
  have hc_ne : c ≠ 0 := ne_of_gt hcpos_c
  have ht_mul : t * c = (α i - d) + c := by
    calc
      t * c = (((α i - d) / c + 1) * c) := by
        simp [t]
      _ = (α i - d) + c := by
        field_simp [hc_ne]
  have hstrict : α i < d + t * c := by
    have hEq : d + t * c = α i + c := by
      calc
        d + t * c = d + ((α i - d) + c) := by rw [ht_mul]
        _ = α i + c := by ring
    linarith [hEq, hcpos_c]
  linarith [hbound, hstrict]

Helper for Text 19.0.9: from a nonempty transformed epigraph image and the repaired polyhedral/non-⊥ : ?m.1⊥ hypotheses, reconstruct a max-affine-plus-indicator representation.

lemma helperForText_19_0_9_nonempty_nonbot_forces_negative_lastCoeff_constraint
    {n m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin (n + 1) → ℝ} {α : Fin m → ℝ}
    (hRaw :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        ⋂ i, closedHalfSpaceLE (n + 1) (a i) (α i))
    (hNonempty :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)).Nonempty)
    (hnonbot : ∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal)) :
    ∃ i : Fin m, a i (Fin.last n) < 0 := by
  by_contra hNoNeg
  have hLastCoeffNonpos :
      ∀ i : Fin m, a i (Fin.last n) ≤ 0 :=
    helperForText_19_0_9_rawHalfspaces_lastCoord_nonpos
      (n := n) (m := m) (f := f) (a := a) (α := α) hRaw hNonempty
  have hLastCoeffZero :
      ∀ i : Fin m, a i (Fin.last n) = 0 := by
    intro i
    have hnotlt : ¬ a i (Fin.last n) < 0 := by
      intro hi
      exact hNoNeg ⟨i, hi⟩
    exact le_antisymm (hLastCoeffNonpos i) (le_of_not_gt hnotlt)
  rcases
    helperForText_19_0_9_nonempty_transformedEpigraphImage_unpack
      (n := n) (f := f) hNonempty with
    ⟨x0, μ0, hx0μ0⟩
  have hRawCoord :
      (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        ⋂ i, closedHalfSpaceLE (n + 1) (a i) (α i) := by
    simpa [prodLinearEquiv_append_coord] using hRaw
  have hz0Coord :
      prodLinearEquiv_append_coord (n := n) (x0, μ0) ∈
        (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) := by
    refine ⟨(x0, μ0), ?_, rfl⟩
    exact (mem_epigraph_univ_iff (f := f)).2 hx0μ0
  have hz0Inter :
      prodLinearEquiv_append_coord (n := n) (x0, μ0) ∈
        ⋂ i : Fin m, closedHalfSpaceLE (n + 1) (a i) (α i) := by
    simpa [hRawCoord] using hz0Coord
  have hAllMu : ∀ μ : ℝ, f x0 ≤ (μ : EReal) := by
    intro μ
    have hzμInter :
        prodLinearEquiv_append_coord (n := n) (x0, μ) ∈
          ⋂ i : Fin m, closedHalfSpaceLE (n + 1) (a i) (α i) := by
      refine Set.mem_iInter.2 ?_
      intro i
      have hz0i :
          prodLinearEquiv_append_coord (n := n) (x0, μ0) ∈
            closedHalfSpaceLE (n + 1) (a i) (α i) :=
        Set.mem_iInter.1 hz0Inter i
      have hz0ineq :
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i) ≤ α i := by
        simpa [closedHalfSpaceLE] using hz0i
      let q : (Fin n → ℝ) × ℝ := (prodLinearEquiv_append_coord (n := n)).symm (a i)
      have hdotμ :
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ)) (a i) =
            dotProduct x0 q.1 + μ * q.2 := by
        calc
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ)) (a i)
              = dotProduct
                  (prodLinearEquiv_append_coord (n := n) (x0, μ))
                  (prodLinearEquiv_append_coord (n := n) q) := by
                  simp [q]
          _ = dotProduct x0 q.1 + μ * q.2 := by
                simpa [q] using
                  helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord
                    (n := n) (p := (x0, μ)) (q := q)
      have hdotμ0 :
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i) =
            dotProduct x0 q.1 + μ0 * q.2 := by
        calc
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i)
              = dotProduct
                  (prodLinearEquiv_append_coord (n := n) (x0, μ0))
                  (prodLinearEquiv_append_coord (n := n) q) := by
                  simp [q]
          _ = dotProduct x0 q.1 + μ0 * q.2 := by
                simpa [q] using
                  helperForText_19_0_9_dotProduct_prodLinearEquivAppendCoord
                    (n := n) (p := (x0, μ0)) (q := q)
      have hq2_eq0 : q.2 = 0 := by
        have hqlast :
            q.2 = (prodLinearEquiv_append_coord (n := n) q) (Fin.last n) := by
          simpa using
            helperForText_19_0_9_prodLinearEquivAppendCoord_last
              (n := n) (x0 := q.1) (μ0 := q.2)
        have hqa :
            (prodLinearEquiv_append_coord (n := n) q) (Fin.last n) = a i (Fin.last n) := by
          have hqa_all :
              prodLinearEquiv_append_coord (n := n) q = a i := by
            simp [q]
          exact congrArg (fun v : Fin (n + 1) → ℝ => v (Fin.last n)) hqa_all
        calc
          q.2 = (prodLinearEquiv_append_coord (n := n) q) (Fin.last n) := hqlast
          _ = a i (Fin.last n) := hqa
          _ = 0 := hLastCoeffZero i
      have hdot_eq :
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ)) (a i) =
            dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i) := by
        calc
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ)) (a i)
              = dotProduct x0 q.1 + μ * q.2 := hdotμ
          _ = dotProduct x0 q.1 := by simp [hq2_eq0]
          _ = dotProduct x0 q.1 + μ0 * q.2 := by simp [hq2_eq0]
          _ = dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ0)) (a i) := by
              simpa using hdotμ0.symm
      have hzμineq :
          dotProduct (prodLinearEquiv_append_coord (n := n) (x0, μ)) (a i) ≤ α i := by
        simpa [hdot_eq] using hz0ineq
      simpa [closedHalfSpaceLE] using hzμineq
    have hzμCoord :
        prodLinearEquiv_append_coord (n := n) (x0, μ) ∈
          (((fun p => prodLinearEquiv_append_coord (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) := by
      simpa [hRawCoord] using hzμInter
    have hxμEpi : (x0, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f :=
      (helperForText_19_0_9_mem_transformedEpigraphImage_iff_mem_epigraph_univ
        (n := n) (f := f) (x := x0) (μ := μ)).1 (by
          simpa [prodLinearEquiv_append_coord] using hzμCoord)
    exact (mem_epigraph_univ_iff (f := f)).1 hxμEpi
  have hfx0Bot : f x0 = (⊥ : EReal) := by
    by_contra hNotBot
    by_cases hTop : f x0 = (⊤ : EReal)
    · have hleTop : (⊤ : EReal) ≤ (0 : EReal) := by
        simpa [hTop] using hAllMu 0
      exact (not_le_of_gt (EReal.coe_lt_top (0 : ℝ))) hleTop
    · have hcoe : (((f x0).toReal : ℝ) : EReal) = f x0 := by
        simpa using (EReal.coe_toReal hTop hNotBot)
      have hleToReal :
          (((f x0).toReal : ℝ) : EReal) ≤ (((f x0).toReal - 1 : ℝ) : EReal) := by
        calc
          (((f x0).toReal : ℝ) : EReal) = f x0 := hcoe
          _ ≤ (((f x0).toReal - 1 : ℝ) : EReal) := hAllMu ((f x0).toReal - 1)
      have hleToRealReal : (f x0).toReal ≤ (f x0).toReal - 1 := by
        exact_mod_cast hleToReal
      linarith
  exact (hnonbot x0) hfx0Bot

Helper for Text 19.0.9: under a nonpositive last-coordinate hypothesis, each raw normal is classified as either strictly negative or exactly zero on the last coordinate.

lemma helperForText_19_0_9_lastCoord_nonpos_partition_neg_or_zero
    {n m : ℕ} {a : Fin m → Fin (n + 1) → ℝ}
    (hLastCoeffNonpos : ∀ i : Fin m, a i (Fin.last n) ≤ 0) :
    ∀ i : Fin m, a i (Fin.last n) < 0 ∨ a i (Fin.last n) = 0 := by
  intro i
  exact lt_or_eq_of_le (hLastCoeffNonpos i)

Helper for Text 19.0.9: if one raw halfspace has strictly negative last coefficient, then the subtype of negative-index constraints is nonempty, so its finite cardinal is nonzero.

lemma helperForText_19_0_9_negativeIndex_nonempty_implies_k_ne_zero_for_blockData
    {n m : ℕ} {a : Fin m → Fin (n + 1) → ℝ}
    (hHasNegativeLastCoeff : ∃ i : Fin m, a i (Fin.last n) < 0) :
    let Ineg : Type := {i : Fin m // a i (Fin.last n) < 0}
    let k : ℕ := Fintype.card Ineg
    k ≠ 0 := by
  intro Ineg k
  rcases hHasNegativeLastCoeff with ⟨i0, hi0⟩
  have hIneg_nonempty : Nonempty Ineg := ⟨⟨i0, hi0⟩⟩
  have hk_pos : 0 < Fintype.card Ineg :=
    (Fintype.card_pos_iff).2 hIneg_nonempty
  exact Nat.ne_of_gt hk_pos

Helper for Text 19.0.9: convert a nonempty transformed-epigraph raw halfspace presentation with nonpositive/negative last-coordinate data into finite split packed constraints in the exact guarded normal form.

lemma helperForText_19_0_9_rawHalfspaces_to_finBlockPackedRepresentationData
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    {m : ℕ} {a : Fin m → Fin (n + 1) → ℝ} {α : Fin m → ℝ}
    (hRawPresentation :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        ⋂ i, closedHalfSpaceLE (n + 1) (a i) (α i))
    (hLastCoeffNonpos : ∀ i : Fin m, a i (Fin.last n) ≤ 0)
    (hHasNegativeLastCoeff : ∃ i : Fin m, a i (Fin.last n) < 0) :
    ∃ (k m' : ℕ) (b : Fin m' → Fin n → ℝ) (β : Fin m' → ℝ),
      0 < k ∧ k ≤ m' ∧
        (((fun p => prodLinearEquiv_append (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
          (({z : Fin (n + 1) → ℝ |
              ∀ i : Fin m', (i : ℕ) < k →
                dotProduct z
                  (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
            {z : Fin (n + 1) → ℝ |
              ∀ i : Fin m', k ≤ (i : ℕ) →
                dotProduct z
                  (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
            (if k = 0 then
              {z : Fin (n + 1) → ℝ |
                0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
            else Set.univ)) := by
  classical
  let Ineg : Type := {i : Fin m // a i (Fin.last n) < 0}
  let Izero : Type := {i : Fin m // a i (Fin.last n) = 0}
  let k : ℕ := Fintype.card Ineg
  let l : ℕ := Fintype.card Izero
  let m' : ℕ := k + l
  let eNeg : Fin k ≃ Ineg := (Fintype.equivFin Ineg).symm
  let eZero : Fin l ≃ Izero := (Fintype.equivFin Izero).symm
  let b : Fin m' → Fin n → ℝ :=
    Fin.addCases
      (fun i j =>
        let ii : Ineg := eNeg i
        a ii.1 (Fin.castSucc j) / (-(a ii.1 (Fin.last n))))
      (fun i j =>
        let ii : Izero := eZero i
        a ii.1 (Fin.castSucc j))
  let β : Fin m' → ℝ :=
    Fin.addCases
      (fun i =>
        let ii : Ineg := eNeg i
        α ii.1 / (-(a ii.1 (Fin.last n))))
      (fun i =>
        let ii : Izero := eZero i
        α ii.1)
  have hk_ne_zero : k ≠ 0 :=
    helperForText_19_0_9_negativeIndex_nonempty_implies_k_ne_zero_for_blockData
      (n := n) (m := m) (a := a) hHasNegativeLastCoeff
  have hk_pos : 0 < k := Nat.pos_of_ne_zero hk_ne_zero
  have hk_le_m' : k ≤ m' := by
    dsimp [m']
    exact Nat.le_add_right k l
  have hRawEqSplitCore :
      (⋂ i : Fin m, closedHalfSpaceLE (n + 1) (a i) (α i)) =
        ({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', (i : ℕ) < k →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', k ≤ (i : ℕ) →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) := by
    ext z
    have hActive_iff :
        ∀ j : Fin k,
          (dotProduct z
              (prodLinearEquiv_append_coord (n := n)
                (b (Fin.castAdd l j), (-1 : ℝ))) ≤
            β (Fin.castAdd l j))
            ↔ dotProduct z (a (eNeg j).1) ≤ α (eNeg j).1 := by
      intro j
      let ii : Ineg := eNeg j
      let t : ℝ := -(a ii.1 (Fin.last n))
      have ht_pos : 0 < t := by
        dsimp [t]
        linarith [ii.2]
      have hβ : β (Fin.castAdd l j) = α ii.1 / t := by
        simp [β, ii, t]
      have hnormal :
          prodLinearEquiv_append_coord (n := n)
              (b (Fin.castAdd l j), (-1 : ℝ)) =
            (1 / t) • a ii.1 := by
        ext u
        refine Fin.lastCases ?_ ?_ u
        · have hlastL :
              (prodLinearEquiv_append_coord (n := n)
                  (b (Fin.castAdd l j), (-1 : ℝ))) (Fin.last n) = (-1 : ℝ) := by
            have hlastPacked :=
              helperForText_19_0_9_prodLinearEquivAppendCoord_last
                (n := n) (x0 := b (Fin.castAdd l j)) (μ0 := (-1 : ℝ))
            simpa using hlastPacked.symm
          have ht_ne : t ≠ 0 := ne_of_gt ht_pos
          calc
            (prodLinearEquiv_append_coord (n := n)
                (b (Fin.castAdd l j), (-1 : ℝ))) (Fin.last n)
                = (-1 : ℝ) := hlastL
            _ = (1 / t) * a ii.1 (Fin.last n) := by
                  have hlast : a ii.1 (Fin.last n) = -t := by
                    simp [t]
                  rw [hlast]
                  field_simp [ht_ne]
            _ = ((1 / t) • a ii.1) (Fin.last n) := by
                  simp [Pi.smul_apply]
        · intro u0
          have hcastL :
              (prodLinearEquiv_append_coord (n := n)
                  (b (Fin.castAdd l j), (-1 : ℝ))) (Fin.castSucc u0) =
                b (Fin.castAdd l j) u0 := by
            have hcastPacked :=
              helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
                (n := n) (x0 := b (Fin.castAdd l j)) (μ0 := (-1 : ℝ)) (j0 := u0)
            simpa using hcastPacked.symm
          have hbcast :
              b (Fin.castAdd l j) u0 =
                a ii.1 (Fin.castSucc u0) / (-(a ii.1 (Fin.last n))) := by
            simp [b, ii]
          calc
            (prodLinearEquiv_append_coord (n := n)
                (b (Fin.castAdd l j), (-1 : ℝ))) (Fin.castSucc u0)
                = b (Fin.castAdd l j) u0 := hcastL
            _ = a ii.1 (Fin.castSucc u0) / (-(a ii.1 (Fin.last n))) := hbcast
            _ = (1 / t) * a ii.1 (Fin.castSucc u0) := by
                  rw [show -(a ii.1 (Fin.last n)) = t by simp [t]]
                  ring
            _ = ((1 / t) • a ii.1) (Fin.castSucc u0) := by
                  simp [Pi.smul_apply]
      have hdot :
          dotProduct z
              (prodLinearEquiv_append_coord (n := n)
                (b (Fin.castAdd l j), (-1 : ℝ))) =
            dotProduct z (a ii.1) / t := by
        calc
          dotProduct z
              (prodLinearEquiv_append_coord (n := n)
                (b (Fin.castAdd l j), (-1 : ℝ)))
              = dotProduct z ((1 / t) • a ii.1) := by rw [hnormal]
          _ = (1 / t) * dotProduct z (a ii.1) := by
                rw [dotProduct_smul, smul_eq_mul]
          _ = dotProduct z (a ii.1) / t := by ring
      constructor
      · intro hsplit
        have hdiv : dotProduct z (a ii.1) / t ≤ α ii.1 / t := by
          simpa [hβ, hdot] using hsplit
        have hmul : dotProduct z (a ii.1) ≤ (α ii.1 / t) * t :=
          (div_le_iff₀ ht_pos).1 hdiv
        have ht_ne : t ≠ 0 := ne_of_gt ht_pos
        have hrt : (α ii.1 / t) * t = α ii.1 := by
          field_simp [ht_ne]
        simpa [hrt] using hmul
      · intro hraw
        have hdiv : dotProduct z (a ii.1) / t ≤ α ii.1 / t :=
          div_le_div_of_nonneg_right hraw (le_of_lt ht_pos)
        simpa [hβ, hdot] using hdiv
    have hDomain_iff :
        ∀ j : Fin l,
          (dotProduct z
              (prodLinearEquiv_append_coord (n := n)
                (b (Fin.natAdd k j), (0 : ℝ))) ≤
            β (Fin.natAdd k j))
            ↔ dotProduct z (a (eZero j).1) ≤ α (eZero j).1 := by
      intro j
      let ii : Izero := eZero j
      have hβ : β (Fin.natAdd k j) = α ii.1 := by
        simp [β, ii]
      have hnormal :
          prodLinearEquiv_append_coord (n := n)
              (b (Fin.natAdd k j), (0 : ℝ)) =
            a ii.1 := by
        ext u
        refine Fin.lastCases ?_ ?_ u
        · have hlastL :
              (prodLinearEquiv_append_coord (n := n)
                  (b (Fin.natAdd k j), (0 : ℝ))) (Fin.last n) = (0 : ℝ) := by
            have hlastPacked :=
              helperForText_19_0_9_prodLinearEquivAppendCoord_last
                (n := n) (x0 := b (Fin.natAdd k j)) (μ0 := (0 : ℝ))
            simpa using hlastPacked.symm
          calc
            (prodLinearEquiv_append_coord (n := n)
                (b (Fin.natAdd k j), (0 : ℝ))) (Fin.last n)
                = (0 : ℝ) := hlastL
            _ = a ii.1 (Fin.last n) := by simpa [ii] using (eZero j).2.symm
        · intro u0
          have hcastL :
              (prodLinearEquiv_append_coord (n := n)
                  (b (Fin.natAdd k j), (0 : ℝ))) (Fin.castSucc u0) =
                b (Fin.natAdd k j) u0 := by
            have hcastPacked :=
              helperForText_19_0_9_prodLinearEquivAppendCoord_castSucc
                (n := n) (x0 := b (Fin.natAdd k j)) (μ0 := (0 : ℝ)) (j0 := u0)
            simpa using hcastPacked.symm
          have hbcast :
              b (Fin.natAdd k j) u0 = a ii.1 (Fin.castSucc u0) := by
            simp [b, ii]
          calc
            (prodLinearEquiv_append_coord (n := n)
                (b (Fin.natAdd k j), (0 : ℝ))) (Fin.castSucc u0)
                = b (Fin.natAdd k j) u0 := hcastL
            _ = a ii.1 (Fin.castSucc u0) := hbcast
      constructor
      · intro hsplit
        have hraw : dotProduct z (a ii.1) ≤ α ii.1 := by
          simpa [hnormal, hβ] using hsplit
        exact hraw
      · intro hraw
        simpa [hnormal, hβ] using hraw
    constructor
    · intro hzRaw
      have hzAll : ∀ i : Fin m, dotProduct z (a i) ≤ α i := by
        intro i
        have hzi : z ∈ closedHalfSpaceLE (n + 1) (a i) (α i) :=
          Set.mem_iInter.1 hzRaw i
        simpa [closedHalfSpaceLE] using hzi
      have hzActiveCast :
          ∀ j : Fin k,
            dotProduct z
              (prodLinearEquiv_append_coord (n := n)
                (b (Fin.castAdd l j), (-1 : ℝ))) ≤ β (Fin.castAdd l j) := by
        intro j
        exact (hActive_iff j).2 (hzAll (eNeg j).1)
      have hzDomainNat :
          ∀ j : Fin l,
            dotProduct z
              (prodLinearEquiv_append_coord (n := n)
                (b (Fin.natAdd k j), (0 : ℝ))) ≤ β (Fin.natAdd k j) := by
        intro j
        exact (hDomain_iff j).2 (hzAll (eZero j).1)
      refine ⟨?_, ?_⟩
      · intro i hi
        let j : Fin k := ⟨(i : ℕ), hi⟩
        have hji : (Fin.castAdd l j : Fin m') = i := by
          ext
          simp [j]
        simpa [hji] using hzActiveCast j
      · intro i hi
        have him : (i : ℕ) < k + l := by
          change (i : ℕ) < m'
          exact i.is_lt
        have hjlt : (i : ℕ) - k < l := by
          omega
        let j : Fin l := ⟨(i : ℕ) - k, hjlt⟩
        have hji : (Fin.natAdd k j : Fin m') = i := by
          ext
          simp [j]
          omega
        simpa [hji] using hzDomainNat j
    · intro hzSplit
      rcases hzSplit with ⟨hzActive, hzDomain⟩
      refine Set.mem_iInter.2 ?_
      intro i
      have hpart : a i (Fin.last n) < 0 ∨ a i (Fin.last n) = 0 :=
        (helperForText_19_0_9_lastCoord_nonpos_partition_neg_or_zero
          (n := n) (m := m) (a := a) hLastCoeffNonpos) i
      have hineq : dotProduct z (a i) ≤ α i := by
        cases hpart with
        | inl hneg =>
            let ii : Ineg := ⟨i, hneg⟩
            let j : Fin k := eNeg.symm ii
            have hlt : ((Fin.castAdd l j : Fin m') : ℕ) < k := by
              exact j.is_lt
            have hzj :
                dotProduct z
                    (prodLinearEquiv_append_coord (n := n)
                      (b (Fin.castAdd l j), (-1 : ℝ))) ≤
                  β (Fin.castAdd l j) :=
              hzActive (Fin.castAdd l j) hlt
            have hrawj : dotProduct z (a (eNeg j).1) ≤ α (eNeg j).1 :=
              (hActive_iff j).1 hzj
            have hej : eNeg j = ii := by
              dsimp [j]
              exact Equiv.apply_symm_apply eNeg ii
            simpa [ii, hej] using hrawj
        | inr hzero =>
            let ii : Izero := ⟨i, hzero⟩
            let j : Fin l := eZero.symm ii
            have hge : k ≤ ((Fin.natAdd k j : Fin m') : ℕ) := by
              exact Nat.le_add_right k (j : ℕ)
            have hzj :
                dotProduct z
                    (prodLinearEquiv_append_coord (n := n)
                      (b (Fin.natAdd k j), (0 : ℝ))) ≤
                  β (Fin.natAdd k j) :=
              hzDomain (Fin.natAdd k j) hge
            have hrawj : dotProduct z (a (eZero j).1) ≤ α (eZero j).1 :=
              (hDomain_iff j).1 hzj
            have hej : eZero j = ii := by
              dsimp [j]
              exact Equiv.apply_symm_apply eZero ii
            simpa [ii, hej] using hrawj
      simpa [closedHalfSpaceLE] using hineq
  have hGuardUniv :
      (if k = 0 then
        {z : Fin (n + 1) → ℝ |
          0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
      else Set.univ) = Set.univ := by
    have hk0 : k ≠ 0 := hk_ne_zero
    simp [hk0]
  refine ⟨k, m', b, β, hk_pos, hk_le_m', ?_⟩
  calc
    (((fun p => prodLinearEquiv_append (n := n) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ))
        = (⋂ i : Fin m, closedHalfSpaceLE (n + 1) (a i) (α i)) := by
            simpa using hRawPresentation
    _ =
      ({z : Fin (n + 1) → ℝ |
          ∀ i : Fin m', (i : ℕ) < k →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m', k ≤ (i : ℕ) →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) :=
      hRawEqSplitCore
    _ =
      (({z : Fin (n + 1) → ℝ |
          ∀ i : Fin m', (i : ℕ) < k →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
        {z : Fin (n + 1) → ℝ |
          ∀ i : Fin m', k ≤ (i : ℕ) →
            dotProduct z
              (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
        (if k = 0 then
          {z : Fin (n + 1) → ℝ |
            0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
        else Set.univ)) := by
          simp [hGuardUniv, Set.inter_univ]

Helper for Text 19.0.9: once finite split packed-constraint data is available for the transformed epigraph image, transport through the representation-image identity and conclude equality of functions.

lemma helperForText_19_0_9_nonempty_forward_branch_finish_from_finBlockData
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    {k m' : ℕ} {b : Fin m' → Fin n → ℝ} {β : Fin m' → ℝ}
    (hk_le_m' : k ≤ m')
    (hSimgEqGuarded :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        (({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', (i : ℕ) < k →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', k ≤ (i : ℕ) →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
          (if k = 0 then
            {z : Fin (n + 1) → ℝ |
              0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
          else Set.univ))) :
    ∃ (k' m'' : ℕ) (b' : Fin m'' → Fin n → ℝ) (β' : Fin m'' → ℝ),
      k' ≤ m'' ∧
        f =
          fun x =>
            ((sSup {r : ℝ |
                ∃ i : Fin m'', (i : ℕ) < k' ∧ r = (∑ j, x j * b' i j) - β' i} : ℝ) : EReal) +
              indicatorFunction
                (C := {y | ∀ i : Fin m'', k' ≤ (i : ℕ) →
                  (∑ j, y j * b' i j) ≤ β' i})
                x := by
  let g : (Fin n → ℝ) → EReal :=
    fun x =>
      ((sSup {r : ℝ |
          ∃ i : Fin m', (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
        indicatorFunction
          (C := {y | ∀ i : Fin m', k ≤ (i : ℕ) →
            (∑ j, y j * b i j) ≤ β i})
          x
  have hSimgG :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ)) =
        (({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', (i : ℕ) < k →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', k ≤ (i : ℕ) →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
          (if k = 0 then
            {z : Fin (n + 1) → ℝ |
              0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
          else Set.univ)) := by
    simpa [g] using
      (helperForText_19_0_9_representation_transformedImage_eq_constraints_with_lastCoord_guard
        (n := n) (k := k) (m := m') (hk := hk_le_m') (b := b) (β := β))
  have hSimgEq :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ)) := by
    calc
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ))
          =
        (({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', (i : ℕ) < k →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m', k ≤ (i : ℕ) →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
          (if k = 0 then
            {z : Fin (n + 1) → ℝ |
              0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
          else Set.univ)) := hSimgEqGuarded
      _ =
        (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ)) := hSimgG.symm
  have hfg : f = g :=
    helperForText_19_0_9_transformedImageCoord_eq_implies_function_eq
      (n := n) (f := f) (g := g) hSimgEq
  refine ⟨k, m', b, β, hk_le_m', ?_⟩
  simpa [g] using hfg

Helper for Text 19.0.9: from a nonempty transformed epigraph image and the repaired polyhedral/non-⊥ : ?m.1⊥ hypotheses, reconstruct a max-affine-plus-indicator representation.

lemma helperForText_19_0_9_polyhedral_nonbot_implies_representation_of_nonempty_transformedEpigraph
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hpolyNonbot :
      IsPolyhedralConvexFunction n f ∧
        (∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal)))
    (hNonempty :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)).Nonempty) :
    ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
      k ≤ m ∧
        f =
          fun x =>
            ((sSup {r : ℝ |
                ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
              indicatorFunction
                (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                  (∑ j, y j * b i j) ≤ β i})
                x := by
  rcases hpolyNonbot with ⟨hpoly, hnonbot⟩
  rcases
    helperForText_19_0_9_nonempty_transformedEpigraphImage_unpack
      (n := n) (f := f) hNonempty with
    ⟨x0, μ0, hx0μ0⟩
  rcases
    helperForText_19_0_9_nonempty_polyhedral_transformedImage_extract_rawHalfspaces
      (n := n) (f := f) hpoly with
    ⟨m, a, α, hRawHalfspaces⟩
  have hpolyData : IsPolyhedralConvexFunction n f := hpoly
  have hnonbotData : ∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal) := hnonbot
  have hWitnessFinite : f x0 ≤ (μ0 : EReal) := hx0μ0
  have hRawPresentation :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)) =
        ⋂ i, closedHalfSpaceLE (n + 1) (a i) (α i) := hRawHalfspaces
  have hNonemptyData :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) : Set (Fin (n + 1) → ℝ)).Nonempty :=
    hNonempty
  have hLastCoeffNonpos :
      ∀ i : Fin m, a i (Fin.last n) ≤ 0 :=
    helperForText_19_0_9_rawHalfspaces_lastCoord_nonpos
      (n := n) (m := m) (f := f) (a := a) (α := α)
      hRawPresentation hNonemptyData
  have hHasNegativeLastCoeff :
      ∃ i : Fin m, a i (Fin.last n) < 0 :=
    helperForText_19_0_9_nonempty_nonbot_forces_negative_lastCoeff_constraint
      (n := n) (m := m) (f := f) (a := a) (α := α)
      hRawPresentation hNonemptyData hnonbotData
  let Ineg : Type := {i : Fin m // a i (Fin.last n) < 0}
  let Izero : Type := {i : Fin m // a i (Fin.last n) = 0}
  let k : ℕ := Fintype.card Ineg
  let l : ℕ := Fintype.card Izero
  let m' : ℕ := k + l
  have hk_ne_zero : k ≠ 0 :=
    helperForText_19_0_9_negativeIndex_nonempty_implies_k_ne_zero_for_blockData
      (n := n) (m := m) (a := a) hHasNegativeLastCoeff
  have hk_pos : 0 < k := Nat.pos_of_ne_zero hk_ne_zero
  have hk_le_m' : k ≤ m' := by
    dsimp [m']
    exact Nat.le_add_right k l
  have hPartitionNegOrZero :
      ∀ i : Fin m, a i (Fin.last n) < 0 ∨ a i (Fin.last n) = 0 :=
    helperForText_19_0_9_lastCoord_nonpos_partition_neg_or_zero
      (n := n) (m := m) (a := a) hLastCoeffNonpos
  have hRepresentationSkeletonReady :
      0 < k ∧ k ≤ m' ∧
        (∀ i : Fin m, a i (Fin.last n) < 0 ∨ a i (Fin.last n) = 0) := by
    exact ⟨hk_pos, hk_le_m', hPartitionNegOrZero⟩
  have hpolyDataKeep : IsPolyhedralConvexFunction n f := hpolyData
  have hWitnessFiniteKeep : f x0 ≤ (μ0 : EReal) := hWitnessFinite
  have hRepresentationSkeletonReadyKeep :
      0 < k ∧ k ≤ m' ∧
        (∀ i : Fin m, a i (Fin.last n) < 0 ∨ a i (Fin.last n) = 0) :=
    hRepresentationSkeletonReady
  rcases
    helperForText_19_0_9_rawHalfspaces_to_finBlockPackedRepresentationData
      (n := n) (f := f) (m := m) (a := a) (α := α)
      hRawPresentation hLastCoeffNonpos hHasNegativeLastCoeff with
    ⟨k', m'', b', β', _hk'_pos, hk'_le_m'', hSimgEqGuarded⟩
  exact
    helperForText_19_0_9_nonempty_forward_branch_finish_from_finBlockData
      (n := n) (f := f) (k := k') (m' := m'') (b := b') (β := β')
      hk'_le_m'' hSimgEqGuarded

Helper for Text 19.0.9: any max-affine-plus-indicator representation induces IsPolyhedralConvexFunction (n : ℕ) (f : (Fin n → ℝ) → EReal) : PropIsPolyhedralConvexFunction via transformed-epigraph polyhedrality.

lemma helperForText_19_0_9_representation_implies_polyhedralConvexFunction_via_transformedImage
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hrepr :
      ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          f =
            (fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧
                    r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x)) :
    IsPolyhedralConvexFunction n f := by
  rcases hrepr with ⟨k, m, b, β, hk, hEq⟩
  subst hEq
  let g : (Fin n → ℝ) → EReal :=
    fun x =>
      ((sSup {r : ℝ |
          ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
        indicatorFunction
          (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
            (∑ j, y j * b i j) ≤ β i})
          x
  have hpointwise_nonbot : ∀ x : Fin n → ℝ, g x ≠ (⊥ : EReal) := by
    intro x
    simpa [g] using
      (helperForText_19_0_9_rhsRepresentation_ne_bot
        (n := n) (k := k) (m := m) (b := b) (β := β) (x := x))
  have hpolyLifted :
      IsPolyhedralConvexSet (n + 1)
        ({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, (i : ℕ) < k →
              dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, k ≤ (i : ℕ) →
              dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i}) :=
    helperForText_19_0_9_liftedConstraintIntersection_polyhedral
      (n := n) (k := k) (m := m) b β
  have hconvLifted :
      Convex ℝ
        ({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, (i : ℕ) < k →
              dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, k ≤ (i : ℕ) →
              dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i}) :=
    helperForTheorem_19_1_polyhedral_isConvex
      (n := n + 1)
      (C :=
        {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, (i : ℕ) < k →
              dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, k ≤ (i : ℕ) →
              dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i})
      hpolyLifted
  have hnonbotG : ∀ x : Fin n → ℝ, g x ≠ (⊥ : EReal) := hpointwise_nonbot
  have hkData : k ≤ m := hk
  have hconvLiftedData :
      Convex ℝ
        ({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, (i : ℕ) < k →
              dotProduct z (Fin.cases (-1 : ℝ) (b i)) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, k ≤ (i : ℕ) →
              dotProduct z (Fin.cases (0 : ℝ) (b i)) ≤ β i}) :=
    hconvLifted
  have hImageEqGuarded :
      (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ)) =
        (({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, (i : ℕ) < k →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, k ≤ (i : ℕ) →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
          (if k = 0 then
            {z : Fin (n + 1) → ℝ |
              0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
          else Set.univ)) :=
    helperForText_19_0_9_representation_transformedImage_eq_constraints_with_lastCoord_guard
      (n := n) (k := k) (m := m) hk b β
  have hpolyGuarded :
      IsPolyhedralConvexSet (n + 1)
        (({z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, (i : ℕ) < k →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (-1 : ℝ))) ≤ β i} ∩
          {z : Fin (n + 1) → ℝ |
            ∀ i : Fin m, k ≤ (i : ℕ) →
              dotProduct z
                (prodLinearEquiv_append_coord (n := n) (b i, (0 : ℝ))) ≤ β i}) ∩
          (if k = 0 then
            {z : Fin (n + 1) → ℝ |
              0 ≤ ((prodLinearEquiv_append_coord (n := n)).symm z).2}
          else Set.univ)) :=
    helperForText_19_0_9_guardedSplitConstraintSet_polyhedral
      (n := n) (k := k) (m := m) b β
  have hpolyImage :
      IsPolyhedralConvexSet (n + 1)
        (((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) g) : Set (Fin (n + 1) → ℝ)) := by
    simpa [hImageEqGuarded] using hpolyGuarded
  have hconvG : ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) g :=
    helperForText_19_0_9_convexFunctionOn_of_polyhedralTransformedEpigraph
      (n := n) (g := g) hpolyImage
  exact ⟨hconvG, hpolyImage⟩

Text 19.0.9: A convex function Unknown identifier `f`f on ℝ ^ sorry : Typeℝ^Unknown identifier `n`n is polyhedral convex iff it can be expressed as , where is the maximum of finitely many affine functions Invalid `⟨...⟩` notation: The expected type of this term could not be determinedsorry - sorry : ?m.6⟨x, b_i⟩ - Unknown identifier `β_i`β_i, and Unknown identifier `C`C is the intersection of finitely many closed half-spaces Invalid `⟨...⟩` notation: The expected type of this term could not be determinedsorry ≤ sorry : Prop⟨x, b_i⟩ ≤ Unknown identifier `β_i`β_i. In this EReal : TypeEReal formalization, the codomain condition is encoded by the pointwise non-⊥ : ?m.1⊥ hypothesis.

theorem polyhedral_convex_function_iff_max_affine_plus_indicator
    (n : ℕ) (f : (Fin n → ℝ) → EReal) :
    (IsPolyhedralConvexFunction n f ∧
      (∀ x : Fin n → ℝ, f x ≠ (⊥ : EReal))) ↔
      ∃ (k m : ℕ) (b : Fin m → Fin n → ℝ) (β : Fin m → ℝ),
        k ≤ m ∧
          f =
            fun x =>
              ((sSup {r : ℝ |
                  ∃ i : Fin m, (i : ℕ) < k ∧ r = (∑ j, x j * b i j) - β i} : ℝ) : EReal) +
                indicatorFunction
                  (C := {y | ∀ i : Fin m, k ≤ (i : ℕ) →
                    (∑ j, y j * b i j) ≤ β i})
                  x := by
  constructor
  · intro hpolyNonbot
    by_cases hEmpty :
        ((fun p => prodLinearEquiv_append (n := n) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f) = ∅
    · exact
        helperForText_19_0_9_polyhedral_nonbot_implies_representation_of_empty_transformedEpigraph
          (n := n) (f := f) hpolyNonbot hEmpty
    · exact
        let S : Set (Fin (n + 1) → ℝ) :=
          ((fun p => prodLinearEquiv_append (n := n) p) ''
            epigraph (Set.univ : Set (Fin n → ℝ)) f)
        let hNonempty : S.Nonempty := by
              by_contra hNotNonempty
              have hSempty : S = ∅ := Set.not_nonempty_iff_eq_empty.1 hNotNonempty
              have hSempty' :
                  ((fun p => prodLinearEquiv_append (n := n) p) ''
                    epigraph (Set.univ : Set (Fin n → ℝ)) f) = ∅ := by
                simpa [S] using hSempty
              exact hEmpty hSempty'
        have hImageNonempty :
            (((fun p => prodLinearEquiv_append (n := n) p) ''
              epigraph (Set.univ : Set (Fin n → ℝ)) f) :
                Set (Fin (n + 1) → ℝ)).Nonempty := by
          simpa [S] using hNonempty
        helperForText_19_0_9_polyhedral_nonbot_implies_representation_of_nonempty_transformedEpigraph
          (n := n) (f := f) hpolyNonbot hImageNonempty
  · intro hrepr
    refine ⟨?_, ?_⟩
    · exact
        helperForText_19_0_9_representation_implies_polyhedralConvexFunction_via_transformedImage
          (n := n) (f := f) hrepr
    · exact
        helperForText_19_0_9_representation_implies_pointwise_nonbot_sideCondition
          (n := n) (f := f) hrepr

Text 19.0.10: A convex function Unknown identifier `f`f is finitely generated if there exist vectors and scalars Unknown identifier `α_i`α_i such that for every Unknown identifier `x`x, Unknown identifier `f`f x is the infimum of over coefficients with , , and for all .

def IsFinitelyGeneratedConvexFunction (n : ℕ) (f : (Fin n → ℝ) → EReal) : Prop :=
  ConvexFunctionOn (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)}

Helper for Text 19.0.10: the coefficient constraints appearing in the finitely generated representation can be read as one bundled conjunction.

lemma helperForText_19_0_10_constraintBundle_wellTyped
    {n k m : ℕ} {a : Fin m → Fin n → ℝ} {x : Fin n → ℝ} {lam : Fin m → ℝ}
    (hlin : ∀ j, (∑ i, lam i * a i j) = x j)
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
        (fun i => lam i)) = 1)
    (hnonneg : ∀ i, 0 ≤ lam i) :
    (∀ 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) := by
  exact ⟨hlin, hnorm, hnonneg⟩

Helper for Text 19.0.10: the linear objective naturally provides an EReal : TypeEReal value via coercion from ℝ : Typeℝ.

lemma helperForText_19_0_10_objective_cast_toEReal
    {m : ℕ} {lam α : Fin m → ℝ} {r : EReal}
    (hr : r = ((∑ i, lam i * α i : ℝ) : EReal)) :
    ∃ q : ℝ, r = (q : EReal) := by
  refine ⟨∑ i, lam i * α i, ?_⟩
  simp [hr]

Helper for Text 19.0.10: any feasible coefficient family contributes its linear objective value as an element of the representation infimum set.

lemma helperForText_19_0_10_objective_mem_representationSet
    {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    {x : Fin n → ℝ} {lam : Fin m → ℝ}
    (hlin : ∀ j, (∑ i, lam i * a i j) = x j)
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
        (fun i => lam i)) = 1)
    (hnonneg : ∀ i, 0 ≤ lam i) :
    (((∑ i, lam i * α i : ℝ) : EReal) ∈
      {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
  exact ⟨lam, hlin, hnorm, hnonneg, rfl⟩

Helper for Text 19.0.10: unpacking the definition immediately yields convexity on Unknown identifier `univ`univ, so this definition introduces no extra proof obligation beyond its fields.

lemma helperForText_19_0_10_noProofObligation
    {n : ℕ} {f : (Fin n → ℝ) → EReal} :
    IsFinitelyGeneratedConvexFunction n f →
      ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f := by
  intro hf
  exact hf.1

Helper for Corollary 19.1.2: unpack the global finite-generation data from the definition.

lemma helperForCorollary_19_1_2_unpack_finitelyGeneratedData
    {n : ℕ} {f : (Fin n → ℝ) → EReal} :
    IsFinitelyGeneratedConvexFunction 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
  intro hf
  exact hf.2

Helper for Corollary 19.1.2: strict epigraph inequality at (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `μ`μ) yields feasible Text 19.0.10 coefficients whose objective value is strictly below Unknown identifier `μ`μ.

lemma helperForCorollary_19_1_2_exists_feasibleCoeffs_lt_mu
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    (hfx_lt : f x < (μ : 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) ∧
      ((∑ i, lam i * α i : ℝ) : EReal) < (μ : EReal) := by
  let Sx : Set EReal :=
    {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)}
  have hsInf_lt : sInf Sx < (μ : EReal) := by
    simpa [Sx, hrepr x] using hfx_lt
  by_contra hNo
  have hmu_lower : (μ : EReal) ≤ sInf Sx := by
    refine le_sInf ?_
    intro r hrSx
    rcases hrSx with ⟨lam, hlin, hnorm, hnonneg, hrObj⟩
    have hr_not_lt : ¬ r < (μ : EReal) := by
      intro hrlt
      have hWitness :
          ∃ (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) ∧
            ((∑ i, lam i * α i : ℝ) : EReal) < (μ : EReal) := by
        refine ⟨lam, hlin, hnorm, hnonneg, ?_⟩
        simpa [hrObj] using hrlt
      exact hNo hWitness
    exact le_of_not_gt hr_not_lt
  exact (not_lt_of_ge hmu_lower hsInf_lt).elim

Helper for Corollary 19.1.2: any feasible Text 19.0.10 coefficients whose objective value is bounded above by Unknown identifier `μ`μ certify epigraph membership at (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `μ`μ).

lemma helperForCorollary_19_1_2_mem_epigraph_univ_of_feasible_obj_le
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    {lam : Fin m → ℝ}
    (hlin : ∀ j, (∑ i, lam i * a i j) = x j)
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
        (fun i => lam i)) = 1)
    (hnonneg : ∀ i, 0 ≤ lam i)
    (hobj_le : (∑ i, lam i * α i : ℝ) ≤ μ) :
    (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f := by
  let Sx : Set EReal :=
    {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)}
  have hsInf_le_obj : sInf Sx ≤ ((∑ i, lam i * α i : ℝ) : EReal) := by
    exact sInf_le ⟨lam, hlin, hnorm, hnonneg, rfl⟩
  have hfx_le_obj : f x ≤ ((∑ i, lam i * α i : ℝ) : EReal) := by
    simpa [Sx, hrepr x] using hsInf_le_obj
  have hobj_leE : ((∑ i, lam i * α i : ℝ) : EReal) ≤ (μ : EReal) := by
    exact_mod_cast hobj_le
  have hfx_le_mu : f x ≤ (μ : EReal) := le_trans hfx_le_obj hobj_leE
  exact (mem_epigraph_univ_iff (f := f)).2 hfx_le_mu

Helper for Corollary 19.1.2: any feasible Text 19.0.10 coefficients whose objective value is strictly below Unknown identifier `μ`μ certify epigraph membership at (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `μ`μ).

lemma helperForCorollary_19_1_2_mem_epigraph_univ_of_feasible_obj_lt
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    {lam : Fin m → ℝ}
    (hlin : ∀ j, (∑ i, lam i * a i j) = x j)
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
        (fun i => lam i)) = 1)
    (hnonneg : ∀ i, 0 ≤ lam i)
    (hobj_lt : ((∑ i, lam i * α i : ℝ) : EReal) < (μ : EReal)) :
    (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f := by
  have hobj_leE : ((∑ i, lam i * α i : ℝ) : EReal) ≤ (μ : EReal) := le_of_lt hobj_lt
  have hobj_le : (∑ i, lam i * α i : ℝ) ≤ μ := by
    exact_mod_cast hobj_leE
  exact
    helperForCorollary_19_1_2_mem_epigraph_univ_of_feasible_obj_le
      (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
      hrepr (x := x) (μ := μ) (lam := lam)
      hlin hnorm hnonneg hobj_le

Helper for Corollary 19.1.2: membership of (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `μ`μ) in the transformed epigraph image is equivalent to ordinary epigraph membership at (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `μ`μ) via the append-coordinate linear equivalence.

lemma helperForCorollary_19_1_2_mem_transformedEpigraphImage_iff_mem_epigraph_univ
    {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} :
    (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
      ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) ↔
      (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f := by
  constructor
  · intro hmem
    rcases hmem with ⟨p, hpEpi, hpImage⟩
    have hp : p = (x, μ) :=
      (prodLinearEquiv_append_coord (n := n)).injective hpImage
    simpa [hp] using hpEpi
  · intro hmem
    exact ⟨(x, μ), hmem, rfl⟩

Helper for Corollary 19.1.2: transformed-epigraph image membership directly yields ordinary epigraph membership at (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `μ`μ).

lemma helperForCorollary_19_1_2_mem_epigraph_univ_of_mem_transformedEpigraphImage
    {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ}
    (hmem :
      (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
        ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f)) :
    (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f := by
  exact
    (helperForCorollary_19_1_2_mem_transformedEpigraphImage_iff_mem_epigraph_univ
      (n := n) (f := f) (x := x) (μ := μ)).1 hmem

Helper for Corollary 19.1.2: transformed-epigraph image membership implies the defining epigraph inequality Unknown identifier `f`sorry ≤ sorry : Propf x ≤ Unknown identifier `μ`μ after coercion to EReal : TypeEReal.

lemma helperForCorollary_19_1_2_fx_leEReal_of_mem_transformedEpigraphImage
    {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ}
    (hmem :
      (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
        ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
          epigraph (Set.univ : Set (Fin n → ℝ)) f)) :
    f x ≤ (μ : EReal) := by
  have hmemEpi : (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f :=
    helperForCorollary_19_1_2_mem_epigraph_univ_of_mem_transformedEpigraphImage
      (n := n) (f := f) (x := x) (μ := μ) hmem
  exact (mem_epigraph_univ_iff (f := f)).1 hmemEpi

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

lemma helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_decodedFeasible
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    (hdecode :
      ∃ (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) ∧
        ((∑ i, lam i * α i : ℝ) : EReal) ≤ (μ : EReal)) :
    (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
      ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
  rcases hdecode with ⟨lam, hlin, hnorm, hnonneg, hobj_le⟩
  have hobj_le_real : (∑ i, lam i * α i : ℝ) ≤ μ := by
    exact_mod_cast hobj_le
  have hqepi : (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f :=
    helperForCorollary_19_1_2_mem_epigraph_univ_of_feasible_obj_le
      (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
      hrepr (x := x) (μ := μ) (lam := lam)
      hlin hnorm hnonneg hobj_le_real
  exact
    (helperForCorollary_19_1_2_mem_transformedEpigraphImage_iff_mem_epigraph_univ
      (n := n) (f := f) (x := x) (μ := μ)).2 hqepi

Helper for Corollary 19.1.2: non-strict direct feasible objective data yields membership in the transformed epigraph image.

lemma helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_directFeasible_le
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    {lam : Fin m → ℝ}
    (hlin : ∀ j, (∑ i, lam i * a i j) = x j)
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
        (fun i => lam i)) = 1)
    (hnonneg : ∀ i, 0 ≤ lam i)
    (hobj_le : ((∑ i, lam i * α i : ℝ) : EReal) ≤ (μ : EReal)) :
    (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
      ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
  have hdecode :
      ∃ (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) ∧
        ((∑ i, lam' i * α i : ℝ) : EReal) ≤ (μ : EReal) := by
    exact ⟨lam, hlin, hnorm, hnonneg, hobj_le⟩
  exact
    helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_decodedFeasible
      (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
      hrepr (x := x) (μ := μ) hdecode

Helper for Corollary 19.1.2: strict objective feasibility data directly yields membership in the transformed epigraph image.

lemma helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_directFeasible_lt
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    {lam : Fin m → ℝ}
    (hlin : ∀ j, (∑ i, lam i * a i j) = x j)
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
        (fun i => lam i)) = 1)
    (hnonneg : ∀ i, 0 ≤ lam i)
    (hobj_lt : ((∑ i, lam i * α i : ℝ) : EReal) < (μ : EReal)) :
    (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
      ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
  have hqepi : (x, μ) ∈ epigraph (Set.univ : Set (Fin n → ℝ)) f :=
    helperForCorollary_19_1_2_mem_epigraph_univ_of_feasible_obj_lt
      (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
      hrepr (x := x) (μ := μ) (lam := lam)
      hlin hnorm hnonneg hobj_lt
  exact
    (helperForCorollary_19_1_2_mem_transformedEpigraphImage_iff_mem_epigraph_univ
      (n := n) (f := f) (x := x) (μ := μ)).2 hqepi

Helper for Corollary 19.1.2: strict epigraph inequality gives feasible coefficients with a non-strict objective upper bound.

lemma helperForCorollary_19_1_2_exists_feasibleCoeffs_le_mu_of_strictIneq
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    (hfx_lt : f x < (μ : 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) ∧
      ((∑ i, lam i * α i : ℝ) : EReal) ≤ (μ : EReal) := by
  rcases
      helperForCorollary_19_1_2_exists_feasibleCoeffs_lt_mu
        (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
        hrepr (x := x) (μ := μ) hfx_lt with
    ⟨lam, hlin, hnorm, hnonneg, hobj_lt⟩
  exact ⟨lam, hlin, hnorm, hnonneg, le_of_lt hobj_lt⟩

Helper for Corollary 19.1.2: strict epigraph inequality yields transformed-epigraph membership by extracting feasible coefficients and weakening to .

lemma helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_strictIneq
    {n k m : ℕ} {f : (Fin n → ℝ) → EReal}
    {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ}
    (hrepr :
      ∀ 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)})
    {x : Fin n → ℝ} {μ : ℝ}
    (hfx_lt : f x < (μ : EReal)) :
    (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
      ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
  have hdecode :
      ∃ (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) ∧
        ((∑ i, lam i * α i : ℝ) : EReal) ≤ (μ : EReal) :=
    helperForCorollary_19_1_2_exists_feasibleCoeffs_le_mu_of_strictIneq
      (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
      hrepr (x := x) (μ := μ) hfx_lt
  exact
    helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_decodedFeasible
      (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
      hrepr (x := x) (μ := μ) hdecode

Helper for Corollary 19.1.2: unpacking finite-generation data and applying the strict inequality decode step yields transformed-epigraph membership.

lemma helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_finitelyGenerated_strictIneq
    {n : ℕ} {f : (Fin n → ℝ) → EReal}
    (hfg : IsFinitelyGeneratedConvexFunction n f)
    {x : Fin n → ℝ} {μ : ℝ}
    (hfx_lt : f x < (μ : EReal)) :
    (prodLinearEquiv_append_coord (n := n)) (x, μ) ∈
      ((fun p => (prodLinearEquiv_append_coord (n := n)) p) ''
        epigraph (Set.univ : Set (Fin n → ℝ)) f) := by
  rcases
      helperForCorollary_19_1_2_unpack_finitelyGeneratedData
        (n := n) (f := f) hfg with
    ⟨k, m, a, α, hk, hrepr⟩
  exact
    helperForCorollary_19_1_2_mem_transformedEpigraphImage_of_strictIneq
      (n := n) (k := k) (m := m) (f := f) (a := a) (α := α)
      hrepr (x := x) (μ := μ) hfx_lt

Helper for Corollary 19.1.2: dropping a nonnegative vertical term from an objective decomposition preserves an upper bound, both in ℝ : Typeℝ and after coercion to EReal : TypeEReal.

lemma helperForCorollary_19_1_2_objective_dropVertical_le
    {qCore tVert μ : ℝ}
    (hdecomp : qCore + tVert ≤ μ)
    (htVert_nonneg : 0 ≤ tVert) :
    qCore ≤ μ ∧ ((qCore : EReal) ≤ (μ : EReal)) := by
  have hreal : qCore ≤ μ := by linarith
  refine ⟨hreal, ?_⟩
  exact_mod_cast hreal

Helper for Corollary 19.1.2: summing over indices in Fin (sorry + sorry) : TypeFin (Unknown identifier `k`k + Unknown identifier `m`m) is the same as summing over Fin sorry : TypeFin Unknown identifier `k`k via Fin.castAdd {n : ℕ} (m : ℕ) : Fin n → Fin (n + m)Fin.castAdd.

lemma helperForCorollary_19_1_2_sum_filter_lt_eq_sum_castAdd
    {k m : ℕ} (g : Fin (k + m) → ℝ) :
    Finset.sum (Finset.univ.filter (fun i : Fin (k + m) => (i : ℕ) < k)) (fun i => g i) =
      ∑ i : Fin k, g (Fin.castAdd m i) := by
  let h : Fin (k + m) → ℝ := fun i => if (i : ℕ) < k then g i else 0
  have hfilter :
      Finset.sum (Finset.univ.filter (fun i : Fin (k + m) => (i : ℕ) < k)) (fun i => g i) =
        ∑ i : Fin (k + m), h i := by
    simp [h, Finset.sum_filter]
  have hsplit :
      (∑ i : Fin (k + m), h i) =
        (∑ i : Fin k, h (Fin.castAdd m i)) + (∑ j : Fin m, h (Fin.natAdd k j)) := by
    simpa using (Fin.sum_univ_add (f := h))
  have hright_zero : (∑ j : Fin m, h (Fin.natAdd k j)) = 0 := by
    refine Finset.sum_eq_zero ?_
    intro j hj
    have hnot : ¬ ((Fin.natAdd k j : Fin (k + m)) : ℕ) < k := by
      exact Nat.not_lt.mpr (Nat.le_add_right k (j : ℕ))
    simp [h]
  have hleft : (∑ i : Fin k, h (Fin.castAdd m i)) = ∑ i : Fin k, g (Fin.castAdd m i) := by
    refine Finset.sum_congr rfl ?_
    intro i hi
    simp [h]
  calc
    Finset.sum (Finset.univ.filter (fun i : Fin (k + m) => (i : ℕ) < k)) (fun i => g i)
        = ∑ i : Fin (k + m), h i := hfilter
    _ = (∑ i : Fin k, h (Fin.castAdd m i)) + (∑ j : Fin m, h (Fin.natAdd k j)) := hsplit
    _ = (∑ i : Fin k, h (Fin.castAdd m i)) := by rw [hright_zero, add_zero]
    _ = ∑ i : Fin k, g (Fin.castAdd m i) := hleft

Helper for Corollary 19.1.2: transport the filtered sum on Fin sorry : TypeFin Unknown identifier `m`m to the left block of Fin (sorry + (sorry - sorry)) : TypeFin (Unknown identifier `k`k + (Unknown identifier `m`m - Unknown identifier `k`k)) via the canonical cast induced by Unknown identifier `k`sorry ≤ sorry : Propk ≤ Unknown identifier `m`m.

lemma helperForCorollary_19_1_2_sum_filter_lt_eq_sum_leftBlock_cast
    {k m : ℕ} (hk : k ≤ m) (lam : Fin m → ℝ) :
    (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k)) (fun i => lam i)) =
      ∑ i : Fin k, lam ((Fin.cast (Nat.add_sub_of_le hk)) (Fin.castAdd (m - k) i)) := by
  let hkm : k + (m - k) = m := Nat.add_sub_of_le hk
  let castKM : Fin (k + (m - k)) → Fin m := Fin.cast hkm
  have hleft_from_cast :
      (∑ i : Fin k, lam (castKM (Fin.castAdd (m - k) i))) =
        (Finset.sum (Finset.univ.filter (fun i : Fin (k + (m - k)) => (i : ℕ) < k))
          (fun i => lam (castKM i))) := by
    rw [helperForCorollary_19_1_2_sum_filter_lt_eq_sum_castAdd
      (k := k) (m := m - k) (g := fun i => lam (castKM i))]
  let e : Fin (k + (m - k)) ≃ Fin m := finCongr hkm
  have htransport :
      (∑ i : Fin (k + (m - k)), if ((e i : Fin m) : ℕ) < k then lam (e i) else 0) =
        (∑ j : Fin m, if (j : ℕ) < k then lam j else 0) := by
    simpa [e] using
      (Equiv.sum_comp e (fun j : Fin m => if (j : ℕ) < k then lam j else 0))
  have htransport' :
      (∑ i : Fin (k + (m - k)), if (i : ℕ) < k then lam (castKM i) else 0) =
        (∑ i : Fin (k + (m - k)), if ((e i : Fin m) : ℕ) < k then lam (e i) else 0) := by
    simp [e, castKM]
  have hfilter_cast :
      (Finset.sum (Finset.univ.filter (fun i : Fin (k + (m - k)) => (i : ℕ) < k))
        (fun i => lam (castKM i))) =
        (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
          (fun i => lam i)) := by
    calc
      (Finset.sum (Finset.univ.filter (fun i : Fin (k + (m - k)) => (i : ℕ) < k))
        (fun i => lam (castKM i)))
          = (∑ i : Fin (k + (m - k)), if (i : ℕ) < k then lam (castKM i) else 0) := by
              simp [Finset.sum_filter]
      _ = (∑ i : Fin (k + (m - k)), if ((e i : Fin m) : ℕ) < k then lam (e i) else 0) :=
            htransport'
      _ = (∑ j : Fin m, if (j : ℕ) < k then lam j else 0) := htransport
      _ =
          (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
            (fun i => lam i)) := by
              simp [Finset.sum_filter]
  exact (hleft_from_cast.trans hfilter_cast).symm

Helper for Corollary 19.1.2: summing over indices not in Fin (sorry + sorry) : TypeFin (Unknown identifier `k`k + Unknown identifier `m`m) is the same as summing over the right block via Fin.natAdd {m : ℕ} (n : ℕ) (i : Fin m) : Fin (n + m)Fin.natAdd.

lemma helperForCorollary_19_1_2_sum_filter_not_lt_eq_sum_natAdd
    {k m : ℕ} (g : Fin (k + m) → ℝ) :
    Finset.sum (Finset.univ.filter (fun i : Fin (k + m) => ¬ ((i : ℕ) < k))) (fun i => g i) =
      ∑ j : Fin m, g (Fin.natAdd k j) := by
  let h : Fin (k + m) → ℝ := fun i => if ¬ ((i : ℕ) < k) then g i else 0
  have hfilter :
      Finset.sum (Finset.univ.filter (fun i : Fin (k + m) => ¬ ((i : ℕ) < k))) (fun i => g i) =
        ∑ i : Fin (k + m), h i := by
    simp [h, Finset.sum_filter]
  have hsplit :
      (∑ i : Fin (k + m), h i) =
        (∑ i : Fin k, h (Fin.castAdd m i)) + (∑ j : Fin m, h (Fin.natAdd k j)) := by
    simpa using (Fin.sum_univ_add (f := h))
  have hleft_zero : (∑ i : Fin k, h (Fin.castAdd m i)) = 0 := by
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp [h]
  have hright : (∑ j : Fin m, h (Fin.natAdd k j)) = ∑ j : Fin m, g (Fin.natAdd k j) := by
    refine Finset.sum_congr rfl ?_
    intro j hj
    have hnot : ¬ ((Fin.natAdd k j : Fin (k + m)) : ℕ) < k := by
      exact Nat.not_lt.mpr (Nat.le_add_right k (j : ℕ))
    simp [h]
  calc
    Finset.sum (Finset.univ.filter (fun i : Fin (k + m) => ¬ ((i : ℕ) < k))) (fun i => g i)
        = ∑ i : Fin (k + m), h i := hfilter
    _ = (∑ i : Fin k, h (Fin.castAdd m i)) + (∑ j : Fin m, h (Fin.natAdd k j)) := hsplit
    _ = (∑ j : Fin m, h (Fin.natAdd k j)) := by rw [hleft_zero, zero_add]
    _ = ∑ j : Fin m, g (Fin.natAdd k j) := hright

Helper for Corollary 19.1.2: transport the filtered sum on Fin sorry : TypeFin Unknown identifier `m`m to the right block of Fin (sorry + (sorry - sorry)) : TypeFin (Unknown identifier `k`k + (Unknown identifier `m`m - Unknown identifier `k`k)) via the canonical cast induced by Unknown identifier `k`sorry ≤ sorry : Propk ≤ Unknown identifier `m`m.

lemma helperForCorollary_19_1_2_sum_filter_not_lt_eq_sum_rightBlock_cast
    {k m : ℕ} (hk : k ≤ m) (lam : Fin m → ℝ) :
    (Finset.sum (Finset.univ.filter (fun i : Fin m => ¬ ((i : ℕ) < k))) (fun i => lam i)) =
      ∑ j : Fin (m - k), lam ((Fin.cast (Nat.add_sub_of_le hk)) (Fin.natAdd k j)) := by
  let hkm : k + (m - k) = m := Nat.add_sub_of_le hk
  let castKM : Fin (k + (m - k)) → Fin m := Fin.cast hkm
  have hright_from_cast :
      (Finset.sum (Finset.univ.filter (fun i : Fin (k + (m - k)) => ¬ ((i : ℕ) < k))
        ) (fun i => lam (castKM i))) =
        (∑ j : Fin (m - k), lam (castKM (Fin.natAdd k j))) := by
    simpa using
      (helperForCorollary_19_1_2_sum_filter_not_lt_eq_sum_natAdd
        (k := k) (m := m - k) (g := fun i => lam (castKM i)))
  let e : Fin (k + (m - k)) ≃ Fin m := finCongr hkm
  have htransport :
      (∑ i : Fin (k + (m - k)), if ¬ (((e i : Fin m) : ℕ) < k) then lam (e i) else 0) =
        (∑ j : Fin m, if ¬ ((j : ℕ) < k) then lam j else 0) := by
    simpa [e] using
      (Equiv.sum_comp e (fun j : Fin m => if ¬ ((j : ℕ) < k) then lam j else 0))
  have htransport' :
      (∑ i : Fin (k + (m - k)), if ¬ ((i : ℕ) < k) then lam (castKM i) else 0) =
        (∑ i : Fin (k + (m - k)), if ¬ (((e i : Fin m) : ℕ) < k) then lam (e i) else 0) := by
    simp [e, castKM]
  have hfilter_cast :
      (Finset.sum (Finset.univ.filter (fun i : Fin (k + (m - k)) => ¬ ((i : ℕ) < k))
        ) (fun i => lam (castKM i))) =
        (Finset.sum (Finset.univ.filter (fun i : Fin m => ¬ ((i : ℕ) < k)))
          (fun i => lam i)) := by
    calc
      (Finset.sum (Finset.univ.filter (fun i : Fin (k + (m - k)) => ¬ ((i : ℕ) < k))
        ) (fun i => lam (castKM i)))
          = (∑ i : Fin (k + (m - k)), if ¬ ((i : ℕ) < k) then lam (castKM i) else 0) := by
              simp [Finset.sum_filter]
      _ = (∑ i : Fin (k + (m - k)), if ¬ (((e i : Fin m) : ℕ) < k) then lam (e i) else 0) :=
            htransport'
      _ = (∑ j : Fin m, if ¬ ((j : ℕ) < k) then lam j else 0) := htransport
      _ =
          (Finset.sum (Finset.univ.filter (fun i : Fin m => ¬ ((i : ℕ) < k)))
            (fun i => lam i)) := by
              simp [Finset.sum_filter]
  exact hfilter_cast.symm.trans hright_from_cast

Helper for Corollary 19.1.2: transport both filtered coefficient sums from Fin sorry : TypeFin Unknown identifier `m`m to the left and right packed blocks in one statement via the canonical cast from Unknown identifier `k`sorry ≤ sorry : Propk ≤ Unknown identifier `m`m.

lemma helperForCorollary_19_1_2_sum_filter_split_eq_pair_leftRight_cast
    {k m : ℕ} (hk : k ≤ m) (lam : Fin m → ℝ) :
    ((Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k)) (fun i => lam i)) =
      ∑ i : Fin k, lam ((Fin.cast (Nat.add_sub_of_le hk)) (Fin.castAdd (m - k) i))) ∧
      ((Finset.sum (Finset.univ.filter (fun i : Fin m => ¬ ((i : ℕ) < k)))
        (fun i => lam i)) =
        ∑ j : Fin (m - k), lam ((Fin.cast (Nat.add_sub_of_le hk)) (Fin.natAdd k j))) := by
  refine ⟨?_, ?_⟩
  · exact
      helperForCorollary_19_1_2_sum_filter_lt_eq_sum_leftBlock_cast
        (k := k) (m := m) hk lam
  · exact
      helperForCorollary_19_1_2_sum_filter_not_lt_eq_sum_rightBlock_cast
        (k := k) (m := m) hk lam

Helper for Corollary 19.1.2: the Text 19.0.10 normalization constraint transports to the left packed block via the canonical cast induced by Unknown identifier `k`sorry ≤ sorry : Propk ≤ Unknown identifier `m`m.

lemma helperForCorollary_19_1_2_transport_normalization_to_leftBlock
    {k m : ℕ} (hk : k ≤ m) {lam : Fin m → ℝ}
    (hnorm :
      (Finset.sum (Finset.univ.filter (fun i : Fin m => (i : ℕ) < k))
        (fun i => lam i)) = 1) :
    (∑ i : Fin k, lam ((Fin.cast (Nat.add_sub_of_le hk)) (Fin.castAdd (m - k) i))) = 1 := by
  rw [← helperForCorollary_19_1_2_sum_filter_lt_eq_sum_leftBlock_cast
    (k := k) (m := m) hk lam]
  exact hnorm

Helper for Corollary 19.1.2: decoding second coordinates after packing by Fin.append.{u_1} {m n : ℕ} {α : Sort u_1} (a : Fin m → α) (b : Fin n → α) : Fin (m + n) → αFin.append and prodLinearEquiv_append_coord (n : ℕ) : ((Fin n → ℝ) × ℝ) ≃ₗ[ℝ] Fin (n + 1) → ℝprodLinearEquiv_append_coord recovers the appended second-coordinate family.

lemma helperForCorollary_19_1_2_decodeSymmSecondCoord_of_appendPacked
    {n r : ℕ}
    (uLeft : Fin 1 → (Fin n → ℝ) × ℝ)
    (uRight : Fin r → (Fin n → ℝ) × ℝ) :
    (fun j : Fin (1 + r) =>
      ((prodLinearEquiv_append_coord (n := n)).symm
        (Fin.append
          (fun i : Fin 1 => (prodLinearEquiv_append_coord (n := n)) (uLeft i))
          (fun i : Fin r => (prodLinearEquiv_append_coord (n := n)) (uRight i))
          j)).2) =
      Fin.append (fun i : Fin 1 => (uLeft i).2) (fun i : Fin r => (uRight i).2) := by
  funext j
  refine Fin.addCases ?_ ?_ j
  · intro i
    simp
  · intro i
    simp

Helper for Corollary 19.1.2: split a packed-index sum into the left block, the vertical singleton slot, and the right block.

lemma helperForCorollary_19_1_2_splitPackedIndexSums_atVertical
    {k m : ℕ} (g : Fin (k + (1 + (m - k))) → ℝ) :
    (∑ i, g i) =
      (∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i)) +
        g (Fin.natAdd k (Fin.castAdd (m - k) (0 : Fin 1))) +
          (∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j))) := by
  have hsplitOuter :
      (∑ i, g i) =
        (∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i)) +
          (∑ u : Fin (1 + (m - k)), g (Fin.natAdd k u)) := by
    simpa using (Fin.sum_univ_add (f := g))
  have hsplitInner :
      (∑ u : Fin (1 + (m - k)), g (Fin.natAdd k u)) =
        (∑ u : Fin 1, g (Fin.natAdd k (Fin.castAdd (m - k) u))) +
          (∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j))) := by
    simpa using
      (Fin.sum_univ_add (f := fun u : Fin (1 + (m - k)) => g (Fin.natAdd k u)))
  have hone :
      (∑ u : Fin 1, g (Fin.natAdd k (Fin.castAdd (m - k) u))) =
        g (Fin.natAdd k (Fin.castAdd (m - k) (0 : Fin 1))) := by
    simp
  calc
    (∑ i, g i)
        =
          (∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i)) +
            ((∑ u : Fin 1, g (Fin.natAdd k (Fin.castAdd (m - k) u))) +
              (∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j)))) := by
            rw [hsplitOuter, hsplitInner]
    _ =
          (∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i)) +
            (g (Fin.natAdd k (Fin.castAdd (m - k) (0 : Fin 1))) +
              (∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j)))) := by
            rw [hone]
    _ =
          (∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i)) +
            g (Fin.natAdd k (Fin.castAdd (m - k) (0 : Fin 1))) +
              (∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j))) := by
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [add_assoc]

Helper for Corollary 19.1.2: decoding a packed three-block linear sum (left points, vertical singleton, right directions) recovers the original first-coordinate linear sum, since the vertical block contributes 0 : ℕ0.

lemma helperForCorollary_19_1_2_packedLinearSum_eq_originalLinearSum
    {n k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (uLeft : Fin k → Fin n → ℝ)
    (uRight : Fin (m - k) → Fin n → ℝ)
    (j0 : Fin n) :
    (∑ i : Fin (k + (1 + (m - k))),
      (Fin.append aFix bFix i) *
        (Fin.append uLeft (Fin.append (fun _ : Fin 1 => (0 : Fin n → ℝ)) uRight) i) j0) =
      (∑ i : Fin k, aFix i * uLeft i j0) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * uRight j j0) := by
  let g : Fin (k + (1 + (m - k))) → ℝ :=
    fun i =>
      (Fin.append aFix bFix i) *
        (Fin.append uLeft (Fin.append (fun _ : Fin 1 => (0 : Fin n → ℝ)) uRight) i) j0
  have hsplit :=
    helperForCorollary_19_1_2_splitPackedIndexSums_atVertical (k := k) (m := m) g
  calc
    (∑ i : Fin (k + (1 + (m - k))),
      (Fin.append aFix bFix i) *
        (Fin.append uLeft (Fin.append (fun _ : Fin 1 => (0 : Fin n → ℝ)) uRight) i) j0)
        = (∑ i, g i) := by rfl
    _ =
          (∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i)) +
            g (Fin.natAdd k (Fin.castAdd (m - k) (0 : Fin 1))) +
              (∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j))) := hsplit
    _ =
          (∑ i : Fin k, aFix i * uLeft i j0) +
            (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * uRight j j0) := by
          simp [g]

Helper for Corollary 19.1.2: decoding a packed three-block objective sum yields the original objective plus the vertical coefficient contribution.

lemma helperForCorollary_19_1_2_packedObjectiveSum_eq_originalPlusVertical
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ) :
    (∑ i : Fin (k + (1 + (m - k))),
      (Fin.append aFix bFix i) *
        (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) =
      (∑ i : Fin k, aFix i * αLeft i) +
        bFix (Fin.castAdd (m - k) (0 : Fin 1)) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) := by
  let g : Fin (k + (1 + (m - k))) → ℝ :=
    fun i =>
      (Fin.append aFix bFix i) *
        (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)
  have hsplit :=
    helperForCorollary_19_1_2_splitPackedIndexSums_atVertical (k := k) (m := m) g
  calc
    (∑ i : Fin (k + (1 + (m - k))),
      (Fin.append aFix bFix i) *
        (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i))
        = (∑ i, g i) := by rfl
    _ =
          (∑ i : Fin k, g (Fin.castAdd (1 + (m - k)) i)) +
            g (Fin.natAdd k (Fin.castAdd (m - k) (0 : Fin 1))) +
              (∑ j : Fin (m - k), g (Fin.natAdd k (Fin.natAdd 1 j))) := hsplit
    _ =
          (∑ i : Fin k, aFix i * αLeft i) +
            bFix (Fin.castAdd (m - k) (0 : Fin 1)) +
            (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) := by
          simp [g, add_assoc]

Helper for Corollary 19.1.2: a packed-objective equality is equivalent to equality of the decoded left-plus-vertical-plus-right objective decomposition.

lemma helperForCorollary_19_1_2_packedObjective_eq_iff_originalPlusVertical_eq
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ} :
    ((∑ i : Fin (k + (1 + (m - k))),
      (Fin.append aFix bFix i) *
        (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ) ↔
      ((∑ i : Fin k, aFix i * αLeft i) +
        bFix (Fin.castAdd (m - k) (0 : Fin 1)) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) = μ) := by
  constructor <;> intro hEq
  ·
    simpa [helperForCorollary_19_1_2_packedObjectiveSum_eq_originalPlusVertical
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)] using hEq
  ·
    simpa [helperForCorollary_19_1_2_packedObjectiveSum_eq_originalPlusVertical
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)] using hEq

Helper for Corollary 19.1.2: a packed-objective upper bound and nonnegativity of the vertical singleton coefficient imply the corresponding upper bound for the original objective, both in ℝ : Typeℝ and after coercion to EReal : TypeEReal.

lemma helperForCorollary_19_1_2_originalObjective_le_of_packedObjective_le
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_le :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) ≤ μ)
    (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1))) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) ∧
      (((((∑ i : Fin k, aFix i * αLeft i) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤ (μ : EReal)) := by
  let qLeft : ℝ := ∑ i : Fin k, aFix i * αLeft i
  let qRight : ℝ := ∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j
  let tVert : ℝ := bFix (Fin.castAdd (m - k) (0 : Fin 1))
  let qCore : ℝ := qLeft + qRight
  have hdecomp_raw :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) =
        qLeft + tVert + qRight := by
    simpa [qLeft, tVert, qRight] using
      helperForCorollary_19_1_2_packedObjectiveSum_eq_originalPlusVertical
        (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
  have hpacked_as : qLeft + tVert + qRight ≤ μ := by
    simpa [hdecomp_raw] using hpacked_le
  have hqCore_plus_tVert : qCore + tVert ≤ μ := by
    calc
      qCore + tVert = qLeft + tVert + qRight := by
        calc
          qCore + tVert = (qLeft + qRight) + tVert := by rfl
          _ = qLeft + (qRight + tVert) := by rw [add_assoc]
          _ = qLeft + (tVert + qRight) := by rw [add_comm qRight tVert]
          _ = qLeft + tVert + qRight := by rw [← add_assoc]
      _ ≤ μ := hpacked_as
  have htVert_nonneg : 0 ≤ tVert := by
    simpa [tVert] using hvertical_nonneg
  have hdrop : qCore ≤ μ ∧ ((qCore : EReal) ≤ (μ : EReal)) :=
    helperForCorollary_19_1_2_objective_dropVertical_le
      (qCore := qCore) (tVert := tVert) (μ := μ)
      hqCore_plus_tVert htVert_nonneg
  simpa [qCore, qLeft, qRight] using hdrop

Helper for Corollary 19.1.2: if the packed objective equals Unknown identifier `μ`μ and the vertical singleton coefficient is nonnegative, then the decoded original objective is at most Unknown identifier `μ`μ both in ℝ : Typeℝ and, after coercion, in EReal : TypeEReal.

lemma helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1))) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) ∧
      (((((∑ i : Fin k, aFix i * αLeft i) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤
          (μ : EReal)) := by
  have hpacked_le :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) ≤ μ := by
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hpacked_eq]
  exact
    helperForCorollary_19_1_2_originalObjective_le_of_packedObjective_le
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_le hvertical_nonneg

Helper for Corollary 19.1.2: nonnegativity of all packed right-block coefficients yields both nonnegativity of the distinguished vertical singleton and nonnegativity of every shifted right-block coefficient.

lemma helperForCorollary_19_1_2_verticalAndRightBlock_nonneg_of_allPackedNonneg
    {k m : ℕ}
    (bFix : Fin (1 + (m - k)) → ℝ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1)) ∧
      (∀ j : Fin (m - k), 0 ≤ bFix (Fin.natAdd 1 j)) := by
  refine ⟨?_, ?_⟩
  · exact hpacked_nonneg (Fin.castAdd (m - k) (0 : Fin 1))
  · intro j
    exact hpacked_nonneg (Fin.natAdd 1 j)

Helper for Corollary 19.1.2: if all packed right-block coefficients are nonnegative, then the distinguished vertical singleton coefficient is nonnegative.

lemma helperForCorollary_19_1_2_verticalSingleton_nonneg_of_allPackedNonneg
    {k m : ℕ}
    (bFix : Fin (1 + (m - k)) → ℝ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1)) := by
  exact
    (helperForCorollary_19_1_2_verticalAndRightBlock_nonneg_of_allPackedNonneg
      (k := k) (m := m) (bFix := bFix) hpacked_nonneg).1

Helper for Corollary 19.1.2: a packed objective equality together with nonnegativity of all packed right-block coefficients yields the decoded original-objective bounds in ℝ : Typeℝ and EReal : TypeEReal.

lemma helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq_of_allPackedNonneg
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) ∧
      (((((∑ i : Fin k, aFix i * αLeft i) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤
          (μ : EReal)) := by
  have hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1)) :=
    helperForCorollary_19_1_2_verticalSingleton_nonneg_of_allPackedNonneg
      (bFix := bFix) hpacked_nonneg
  exact
    helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hvertical_nonneg

Helper for Corollary 19.1.2: if the packed objective equals Unknown identifier `μ`μ and all packed right-block coefficients are nonnegative, then the decoded original objective is at most Unknown identifier `μ`μ in ℝ : Typeℝ.

lemma helperForCorollary_19_1_2_originalObjective_le_of_packedObjective_eq_of_allPackedNonneg
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) := by
  exact
    (helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq_of_allPackedNonneg
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hpacked_nonneg).1

lemma helperForCorollary_19_1_2_originalObjective_leEReal_of_packedObjective_eq_of_allPackedNonneg
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    (((((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤ (μ : EReal)) := by
  exact
    (helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq_of_allPackedNonneg
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hpacked_nonneg).2

Helper for Corollary 19.1.2: transporting a packed decoded objective equality and nonnegative vertical singleton coefficient yields the decoded original-objective bound in both ℝ : Typeℝ and EReal : TypeEReal.

lemma helperForCorollary_19_1_2_transport_originalCoeffs_of_packedDecode
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1))) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) ∧
      (((((∑ i : Fin k, aFix i * αLeft i) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤
          (μ : EReal)) := by
  exact
    helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hvertical_nonneg

Helper for Corollary 19.1.2: transporting a packed decoded objective equality together with nonnegativity of all packed right-block coefficients yields the decoded original-objective bound in both ℝ : Typeℝ and EReal : TypeEReal.

lemma helperForCorollary_19_1_2_transport_originalCoeffs_of_packedDecode_of_allPackedNonneg
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) ∧
      (((((∑ i : Fin k, aFix i * αLeft i) +
        (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤
          (μ : EReal)) := by
  have hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1)) :=
    helperForCorollary_19_1_2_verticalSingleton_nonneg_of_allPackedNonneg
      (bFix := bFix) hpacked_nonneg
  exact
    helperForCorollary_19_1_2_transport_originalCoeffs_of_packedDecode
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hvertical_nonneg

Helper for Corollary 19.1.2: transporting packed decoded objective data together with nonnegativity of all packed right-block coefficients yields the decoded original-objective bound in ℝ : Typeℝ.

lemma helperForCorollary_19_1_2_transport_originalCoeffs_le_of_packedDecode_of_allPackedNonneg
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) := by
  exact
    (helperForCorollary_19_1_2_transport_originalCoeffs_of_packedDecode_of_allPackedNonneg
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hpacked_nonneg).1

lemma helperForCorollary_19_1_2_transport_originalCoeffs_leEReal_of_packedDecode_of_allPackedNonneg
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hpacked_nonneg : ∀ i : Fin (1 + (m - k)), 0 ≤ bFix i) :
    (((((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤
        (μ : EReal)) := by
  exact
    (helperForCorollary_19_1_2_transport_originalCoeffs_of_packedDecode_of_allPackedNonneg
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hpacked_nonneg).2

lemma helperForCorollary_19_1_2_originalObjective_le_of_packedObjective_eq
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1))) :
    ((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j) ≤ μ) := by
  exact
    (helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hvertical_nonneg).1

lemma helperForCorollary_19_1_2_originalObjective_leEReal_of_packedObjective_eq
    {k m : ℕ}
    (aFix : Fin k → ℝ)
    (bFix : Fin (1 + (m - k)) → ℝ)
    (αLeft : Fin k → ℝ)
    (αRight : Fin (m - k) → ℝ)
    {μ : ℝ}
    (hpacked_eq :
      (∑ i : Fin (k + (1 + (m - k))),
        (Fin.append aFix bFix i) *
          (Fin.append αLeft (Fin.append (fun _ : Fin 1 => (1 : ℝ)) αRight) i)) = μ)
    (hvertical_nonneg : 0 ≤ bFix (Fin.castAdd (m - k) (0 : Fin 1))) :
    (((((∑ i : Fin k, aFix i * αLeft i) +
      (∑ j : Fin (m - k), bFix (Fin.natAdd 1 j) * αRight j)) : ℝ) : EReal) ≤ (μ : EReal)) := by
  exact
    (helperForCorollary_19_1_2_originalObjective_le_pair_of_packedObjective_eq
      (aFix := aFix) (bFix := bFix) (αLeft := αLeft) (αRight := αRight)
      (μ := μ) hpacked_eq hvertical_nonneg).2

end Section19end Chap19