Convex Analysis (Rockafellar, 1970) -- Chapter 03 -- Section 14 -- Part 3

section Chap03section Section14open scoped Pointwiseopen scoped Topologyvariable {E : Type*} [AddCommGroup E] [Module ℝ E]

-- The weak topology on the algebraic dual induced by evaluation (see also `section14_part1`).
noncomputable local instance section14_instTopologicalSpace_dualWeak_part3 :
    TopologicalSpace (Module.Dual ℝ E) :=
  WeakBilin.instTopologicalSpace
    (B := (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)).flip)

-- Basic topological vector space structure on the dual, induced by the weak topology above.
noncomputable local instance section14_instIsTopologicalAddGroup_dualWeak_part3 :
    IsTopologicalAddGroup (Module.Dual ℝ E) :=
  WeakBilin.instIsTopologicalAddGroup
    (B := (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)).flip)

noncomputable local instance section14_instContinuousSMul_dualWeak_part3 :
    ContinuousSMul ℝ (Module.Dual ℝ E) :=
  WeakBilin.instContinuousSMul (B := (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)).flip)

noncomputable local instance section14_instLocallyConvexSpace_dualWeak_part3 :
    LocallyConvexSpace ℝ (Module.Dual ℝ E) :=
  WeakBilin.locallyConvexSpace (B := (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)).flip)

If is in the recession cone of and is finite somewhere, then is nonpositive on erealDom sorry : Set ?m.1erealDom Unknown identifier `f`f.

lemma section14_le_zero_on_dom_of_mem_recessionCone_fenchelConjugate {f : E → EReal}
    (hf : ProperERealFunction f) {yStar : Module.Dual ℝ E}
    (hy :
      yStar ∈
        recessionConeEReal
          (F := Module.Dual ℝ E)
          (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f))
    (hxStar0 :
      ∃ xStar0 : Module.Dual ℝ E,
        fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f xStar0 < ⊤) :
    ∀ x, x ∈ erealDom f → yStar x ≤ 0 := by
  classical
  set p : E →ₗ[ℝ] (Module.Dual ℝ E) →ₗ[ℝ] ℝ :=
    (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))
  set g : Module.Dual ℝ E → EReal := fenchelConjugateBilin p f
  have hneBot : ∀ xStar : Module.Dual ℝ E, g xStar ≠ ⊥ := by
    intro xStar
    simpa [g, p] using (section14_fenchelConjugate_ne_bot (E := E) (f := f) hf xStar)

  rcases hxStar0 with ⟨xStar0, hxStar0lt⟩
  have hxStar0dom : xStar0 ∈ erealDom g := by simpa [erealDom, g, p] using hxStar0lt

  have hind :
      ∀ n : ℕ,
        g (xStar0 + n • yStar) ≤ g xStar0 ∧ xStar0 + n • yStar ∈ erealDom g := by
    intro n
    induction n with
    | zero =>
        simp [hxStar0dom]
    | succ n ih =>
        have hxNdom : xStar0 + n • yStar ∈ erealDom g := ih.2
        have hstep :
            g ((xStar0 + n • yStar) + yStar) ≤ g (xStar0 + n • yStar) ∧
              (xStar0 + n • yStar) + yStar ∈ erealDom g := by
          simpa [g, p] using
            (section14_step_le_of_mem_recessionCone (g := g) (x := xStar0 + n • yStar)
                  (y := yStar) hy hxNdom)
        refine ⟨?_, ?_⟩
        ·
          have : g ((xStar0 + n • yStar) + yStar) ≤ g xStar0 := hstep.1.trans ih.1
          simpa [succ_nsmul, add_assoc] using this
        ·
          have : (xStar0 + n • yStar) + yStar ∈ erealDom g := hstep.2
          simpa [succ_nsmul, add_assoc] using this

  intro x hx
  rcases section14_eq_coe_of_lt_top (z := f x) hx (hf.1 x) with ⟨rf, hrf⟩
  rcases section14_eq_coe_of_lt_top (z := g xStar0) (by simpa [g, p] using hxStar0lt)
      (hneBot xStar0) with ⟨rg, hrg⟩

  have hmul_le : ∀ n : ℕ, (n : ℝ) * yStar x ≤ rg + rf - xStar0 x := by
    intro n
    have hle1 :
        (((xStar0 + n • yStar) x : EReal) - f x) ≤ g xStar0 := by
      have hleSup :
          (((xStar0 + n • yStar) x : EReal) - f x) ≤ g (xStar0 + n • yStar) := by
        -- Use the definition of the Fenchel conjugate at a single point.
        have :
            ((p x (xStar0 + n • yStar) : EReal) - f x) ≤
              sSup (Set.range fun z : E => (p z (xStar0 + n • yStar) : EReal) - f z) :=
          le_sSup ⟨x, rfl⟩
        simpa [g, fenchelConjugateBilin, p] using this
      exact hleSup.trans (hind n).1
    have hle2 :
        ((xStar0 x + (n : ℝ) * yStar x - rf : ℝ) : EReal) ≤ (rg : EReal) := by
      simpa [g, p, hrf, hrg, LinearMap.add_apply, nsmul_eq_mul, sub_eq_add_neg] using hle1
    have hreal : xStar0 x + (n : ℝ) * yStar x - rf ≤ rg :=
      (EReal.coe_le_coe_iff).1 hle2
    linarith

  exact section14_real_nonpos_of_nat_mul_le (r := yStar x) (C := rg + rf - xStar0 x) hmul_le

Theorem 14.2. Let Unknown identifier `f`f be a proper convex function. The polar of the convex cone generated by Unknown identifier `dom`dom f is the recession cone of the Fenchel conjugate . Dually, if Unknown identifier `f`f is closed, the polar of the recession cone of Unknown identifier `f`f is the closure of the convex cone generated by .

theorem polar_coneGenerated_dom_eq_recessionCone_fenchelConjugate {f : E → EReal}
    (hf : ProperConvexERealFunction (F := E) f)
    (hdom :
      ∃ xStar0 : Module.Dual ℝ E,
        fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f xStar0 < ⊤) :
    polarCone (E := E) ((ConvexCone.hull ℝ (erealDom f) : ConvexCone ℝ E) : Set E) =
      recessionConeEReal
        (F := Module.Dual ℝ E)
        (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f) := by
  classical
  ext yStar
  constructor
  · intro hy
    have hyDom : ∀ x, x ∈ erealDom f → yStar x ≤ 0 :=
      (section14_mem_polarCone_hull_erealDom_iff (E := E) (f := f) (φ := yStar)).1 hy
    refine (section14_mem_recessionConeEReal_iff
          (g := fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)
          (y := yStar)).2 ?_
    intro xStar _
    have hle :
        fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f (xStar + yStar) ≤
          fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f xStar :=
      section14_fenchelConjugate_add_le_of_le_zero_on_dom (E := E) (f := f) (yStar := yStar)
        hyDom xStar
    -- `a - b ≤ 0 ↔ a ≤ b` on `EReal`.
    exact (EReal.sub_nonpos).2 hle
  · intro hy
    have hyDom : ∀ x, x ∈ erealDom f → yStar x ≤ 0 := by
      exact
        section14_le_zero_on_dom_of_mem_recessionCone_fenchelConjugate (E := E) (f := f)
          (hf := hf.1) (yStar := yStar) hy hdom
    exact (section14_mem_polarCone_hull_erealDom_iff (E := E) (f := f) (φ := yStar)).2 hyDom

The polar cone of a set, packaged as a ConvexCone.{u_2, u_4} (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : Type u_4ConvexCone, so that we can use ConvexCone.hull.{u_2, u_4} (R : Type u_2) {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (s : Set M) : ConvexCone R MConvexCone.hull minimality arguments.

def section14_polarConeConvexCone (K : Set E) : ConvexCone ℝ (Module.Dual ℝ E) where
  carrier := polarCone (E := E) K
  smul_mem' a ha φ hφ := by
    refine (mem_polarCone_iff (E := E) (K := K) (φ := a • φ)).2 ?_
    intro x hx
    have hφx : φ x ≤ 0 := (mem_polarCone_iff (E := E) (K := K) (φ := φ)).1 hφ x hx
    simpa [LinearMap.smul_apply, smul_eq_mul] using
      mul_nonpos_of_nonneg_of_nonpos (le_of_lt ha) hφx
  add_mem' φ₁ hφ₁ φ₂ hφ₂ := by
    refine (mem_polarCone_iff (E := E) (K := K) (φ := φ₁ + φ₂)).2 ?_
    intro x hx
    have h₁ : φ₁ x ≤ 0 := (mem_polarCone_iff (E := E) (K := K) (φ := φ₁)).1 hφ₁ x hx
    have h₂ : φ₂ x ≤ 0 := (mem_polarCone_iff (E := E) (K := K) (φ := φ₂)).1 hφ₂ x hx
    simpa [LinearMap.add_apply] using add_nonpos h₁ h₂

If is in the effective domain of , then lies in the polar cone of the recession cone of Unknown identifier `f`f.

lemma section14_mem_polar_recessionCone_of_mem_dom_fenchelConjugate {f : E → EReal}
    (hf : ProperERealFunction f) {xStar : Module.Dual ℝ E}
    (hxStar :
      xStar ∈
        erealDom (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
    xStar ∈ polarCone (E := E) (recessionConeEReal (F := E) f) := by
  classical
  -- Unpack polar membership: show `xStar y ≤ 0` for all recession directions `y`.
  refine (mem_polarCone_iff (E := E) (K := recessionConeEReal (F := E) f) (φ := xStar)).2 ?_
  intro y hy
  -- Choose a finite point `x0` of `f` from properness.
  rcases hf.2 with ⟨x0, hx0neTop⟩
  have hx0dom : x0 ∈ erealDom f := lt_top_iff_ne_top.2 hx0neTop
  rcases section14_eq_coe_of_lt_top (z := f x0) hx0dom (hf.1 x0) with ⟨r0, hr0⟩

  set p : E →ₗ[ℝ] (Module.Dual ℝ E) →ₗ[ℝ] ℝ :=
    (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))
  set g : Module.Dual ℝ E → EReal := fenchelConjugateBilin p f
  have hneBot : ∀ z : Module.Dual ℝ E, g z ≠ ⊥ := by
    intro z
    simpa [g, p] using (section14_fenchelConjugate_ne_bot (E := E) (f := f) hf z)
  rcases section14_eq_coe_of_lt_top (z := g xStar) (by simpa [erealDom, g, p] using hxStar)
      (hneBot xStar) with ⟨rg, hrg⟩

  -- Iterate the recession step to get uniform bounds along `n • y`.
  have hind :
      ∀ n : ℕ, f (x0 + n • y) ≤ f x0 ∧ x0 + n • y ∈ erealDom f := by
    intro n
    induction n with
    | zero =>
        simp [hx0dom]
    | succ n ih =>
        have hstep :=
          section14_step_le_of_mem_recessionCone (g := f) (x := x0 + n • y) (y := y) hy ih.2
        refine ⟨?_, ?_⟩
        ·
          have : f ((x0 + n • y) + y) ≤ f x0 := hstep.1.trans ih.1
          simpa [succ_nsmul, add_assoc] using this
        -- `x0 + (n+1)•y = (x0 + n•y) + y`.
        simpa [succ_nsmul, add_assoc] using hstep.2

  -- Use the Fenchel conjugate bound at `x0 + n•y` to bound `(n : ℝ) * (xStar y)`.
  have hmul_le : ∀ n : ℕ, (n : ℝ) * xStar y ≤ rg + r0 - xStar x0 := by
    intro n
    set xn : E := x0 + n • y
    have hxn_dom : xn ∈ erealDom f := by simpa [xn] using (hind n).2
    -- `xStar xn - f xn ≤ g xStar`.
    have hle_xn : ((p xn xStar : EReal) - f xn) ≤ g xStar := by
      have :
          (p xn xStar : EReal) - f xn ≤ sSup (Set.range fun z : E => (p z xStar : EReal) - f z) :=
        le_sSup ⟨xn, rfl⟩
      simpa [g, fenchelConjugateBilin, p] using this
    -- Coerce `f xn` to a real `rn` and use `f xn ≤ f x0` to compare to `r0`.
    rcases section14_eq_coe_of_lt_top (z := f xn) hxn_dom (hf.1 xn) with ⟨rn, hrn⟩
    have hrn_le : rn ≤ r0 := by
      have : (f xn : EReal) ≤ f x0 := (hind n).1
      have : ((rn : ℝ) : EReal) ≤ (r0 : EReal) := by simpa [hrn, hr0, xn] using this
      exact (EReal.coe_le_coe_iff).1 this
    -- Turn the Fenchel bound into a real inequality `xStar xn - rn ≤ rg`.
    have hreal_xn_rn : xStar xn - rn ≤ rg := by
      have hE : ((xStar xn - rn : ℝ) : EReal) ≤ g xStar := by
        simpa [xn, p, hrn, LinearMap.applyₗ, sub_eq_add_neg] using hle_xn
      have hE' : ((xStar xn - rn : ℝ) : EReal) ≤ (rg : EReal) := by
        simpa [hrg] using hE
      exact (EReal.coe_le_coe_iff).1 hE'
    -- Since `rn ≤ r0`, get `xStar xn - r0 ≤ rg`.
    have hreal_xn_r0 : xStar xn - r0 ≤ rg := by
      have : xStar xn - r0 ≤ xStar xn - rn := by
        -- Subtracting a larger number yields a smaller result.
        simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using
          (sub_le_sub_left hrn_le (xStar xn))
      exact this.trans hreal_xn_rn
    -- Expand `xStar xn` and solve for `(n : ℝ) * xStar y`.
    have hxStar_xn : xStar xn = xStar x0 + (n : ℝ) * xStar y := by
      simp [xn, map_add, map_nsmul, nsmul_eq_mul]
    linarith [hreal_xn_r0, hxStar_xn]

  -- Conclude `xStar y ≤ 0` from the uniform bound on natural multiples.
  exact section14_real_nonpos_of_nat_mul_le (r := xStar y) (C := rg + r0 - xStar x0) hmul_le

The closed conic hull of is contained in the polar of the recession cone of Unknown identifier `f`f.

lemma section14_closure_coneHull_dom_fenchelConjugate_subset_polar_recessionCone [TopologicalSpace E]
    {f : E → EReal} (hf : ProperConvexERealFunction (F := E) f) :
    closure
        ((ConvexCone.hull ℝ
              (erealDom
                (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
              ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) ⊆
      polarCone (E := E) (recessionConeEReal (F := E) f) := by
  classical
  -- First show the (non-closed) conic hull is contained.
  have hHull :
      ((ConvexCone.hull ℝ
            (erealDom
              (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
          ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) ⊆
        polarCone (E := E) (recessionConeEReal (F := E) f) := by
    -- Use the hull-minimality into the convex cone `polarConeConvexCone`.
    have :
        (ConvexCone.hull ℝ
              (erealDom
                (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
            ConvexCone ℝ (Module.Dual ℝ E)) ≤
          section14_polarConeConvexCone (E := E) (K := recessionConeEReal (F := E) f) := by
      refine (ConvexCone.hull_le_iff (C := section14_polarConeConvexCone (E := E)
          (K := recessionConeEReal (F := E) f))).2 ?_
      intro xStar hxStar
      exact
        section14_mem_polar_recessionCone_of_mem_dom_fenchelConjugate (E := E) (f := f) hf.1
          hxStar
    exact this
  -- Now use closedness of the polar cone in the weak topology to absorb the closure.
  have hclosed : IsClosed (polarCone (E := E) (recessionConeEReal (F := E) f)) :=
    section14_isClosed_polarCone (E := E) (K := recessionConeEReal (F := E) f)
  exact closure_minimal hHull hclosed

Any continuous linear functional on Module.Dual ℝ Unknown identifier `E`E equipped with the weak topology induced by evaluation is itself an evaluation at some .

lemma section14_exists_eval_of_continuousLinearMap_dualWeak
    (ℓ : (Module.Dual ℝ E) →L[ℝ] ℝ) :
    ∃ y : E, ∀ xStar : Module.Dual ℝ E, ℓ xStar = xStar y := by
  classical
  let evalLM : E →ₗ[ℝ] (Module.Dual ℝ E →ₗ[ℝ] ℝ) :=
    (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))
  have ht :
      (section14_instTopologicalSpace_dualWeak_part3 (E := E) : TopologicalSpace (Module.Dual ℝ E)) =
        ⨅ y : E, TopologicalSpace.induced (evalLM y) inferInstance := by
    -- Expand the weak topology as the infimum of the induced topologies from the evaluations.
    simp [section14_instTopologicalSpace_dualWeak_part3, WeakBilin.instTopologicalSpace,
      Pi.topologicalSpace, evalLM, induced_iInf, induced_compose]
    refine iInf_congr fun y => ?_
    -- `Pi.topologicalSpace` uses the default topology on `ℝ`.
    change
      TopologicalSpace.induced
          ((fun f : E → ℝ => f y) ∘ fun x : Module.Dual ℝ E => fun z : E => x z)
          (inferInstance : TopologicalSpace ℝ) =
        TopologicalSpace.induced (fun x : Module.Dual ℝ E => x y) (inferInstance : TopologicalSpace ℝ)
    rfl
  have hcont :
      @Continuous (Module.Dual ℝ E) ℝ
        (⨅ y : E, TopologicalSpace.induced (evalLM y) inferInstance) inferInstance
        (fun xStar : Module.Dual ℝ E => ℓ xStar) := by
    have h0 :
        @Continuous (Module.Dual ℝ E) ℝ
          (section14_instTopologicalSpace_dualWeak_part3 (E := E) : TopologicalSpace (Module.Dual ℝ E))
          inferInstance (fun xStar : Module.Dual ℝ E => ℓ xStar) :=
      ℓ.continuous
    simpa [ht] using h0
  have hmem :
      (ℓ : Module.Dual ℝ E →ₗ[ℝ] ℝ) ∈ Submodule.span ℝ (Set.range evalLM) := by
    -- Continuous linear maps for the weak topology lie in the span of the evaluations.
    exact
      (LinearMap.mem_span_iff_continuous (f := fun y : E => evalLM y)
            (φ := (ℓ : Module.Dual ℝ E →ₗ[ℝ] ℝ))).2 hcont
  have hspan_le_range : Submodule.span ℝ (Set.range evalLM) ≤ LinearMap.range evalLM := by
    refine Submodule.span_le.2 ?_
    rintro _ ⟨y, rfl⟩
    exact ⟨y, rfl⟩
  have hrange : (ℓ : Module.Dual ℝ E →ₗ[ℝ] ℝ) ∈ LinearMap.range evalLM :=
    hspan_le_range hmem
  rcases hrange with ⟨y, hy⟩
  refine ⟨y, ?_⟩
  intro xStar
  -- Unpack the identity `evalLM y = ℓ` pointwise.
  have := congrArg (fun m : Module.Dual ℝ E →ₗ[ℝ] ℝ => m xStar) hy
  simpa [evalLM, LinearMap.applyₗ] using this.symm

If is not in the (weak) closure of the conic hull of , then one can separate it from that cone by evaluation at some .

lemma section14_exists_eval_sep_of_not_mem_closure_coneHull_dom_fenchelConjugate {f : E → EReal}
    {xStar : Module.Dual ℝ E}
    (hDom :
      (erealDom
          (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)).Nonempty)
    (hxStar :
      xStar ∉
        closure
          ((ConvexCone.hull ℝ
                (erealDom
                  (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
                ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E))) :
    ∃ y : E,
      (∀ z : Module.Dual ℝ E,
          z ∈
              closure
                ((ConvexCone.hull ℝ
                      (erealDom
                        (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
                    ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) →
            z y ≤ 0) ∧
        0 < xStar y := by
  classical
  set K : ConvexCone ℝ (Module.Dual ℝ E) :=
    ConvexCone.hull ℝ
      (erealDom (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f))
  have hKne : (K : Set (Module.Dual ℝ E)).Nonempty := by
    rcases hDom with ⟨xStar0, hxStar0⟩
    refine ⟨xStar0, ?_⟩
    exact (ConvexCone.subset_hull (s :=
      erealDom (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f))) hxStar0
  have hKcl_ne : ((K.closure : ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)).Nonempty :=
    by simpa [ConvexCone.coe_closure] using hKne.closure
  have hKcl_closed :
      IsClosed ((K.closure : ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) := by
    simp [ConvexCone.coe_closure]
  rcases
      (ConvexCone.canLift (𝕜 := ℝ) (E := Module.Dual ℝ E)).prf K.closure
        ⟨hKcl_ne, hKcl_closed⟩ with
    ⟨C, hCeq⟩
  have hxC : xStar ∉ (C : Set (Module.Dual ℝ E)) := by
    intro hxC
    have hxC' : xStar ∈ ((↑C : ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) := by
      simpa using hxC
    have hxKcl : xStar ∈ (K.closure : Set (Module.Dual ℝ E)) := by
      simpa [hCeq] using hxC'
    have hxcl' : xStar ∈ closure (K : Set (Module.Dual ℝ E)) := by
      simpa [ConvexCone.coe_closure] using hxKcl
    exact hxStar (by simpa [K] using hxcl')
  obtain ⟨fSep, hfSepC, hfSepx⟩ :=
    ProperCone.hyperplane_separation_point (C := C) (x₀ := xStar) hxC
  -- Flip the sign so that the separator is nonpositive on the cone and strictly positive at `xStar`.
  let ℓ : (Module.Dual ℝ E) →L[ℝ] ℝ := -fSep
  rcases section14_exists_eval_of_continuousLinearMap_dualWeak (E := E) (ℓ := ℓ) with ⟨y, hy⟩
  refine ⟨y, ?_, ?_⟩
  · intro z hz
    have hz' : z ∈ (C : Set (Module.Dual ℝ E)) := by
      have hzKcl : z ∈ (K.closure : Set (Module.Dual ℝ E)) := by
        -- `hz : z ∈ closure (K : Set _)` by unfolding `K`.
        simpa [K] using hz
      have hzKcl' : z ∈ ((K.closure : ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) :=
        hzKcl
      have : z ∈ ((↑C : ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) := by
        simpa [hCeq] using hzKcl'
      simpa using this
    have hfnonneg : 0 ≤ fSep z := hfSepC z hz'
    have : ℓ z ≤ 0 := by
      -- `ℓ z = - fSep z`.
      simpa [ℓ] using (neg_nonpos.2 hfnonneg)
    simpa [hy z, ℓ] using this
  · have : 0 < ℓ xStar := by
      have : fSep xStar < 0 := hfSepx
      simpa [ℓ] using (neg_pos.2 this)
    simpa [hy xStar] using this

A Hahn–Banach separation gadget for a proper convex lower semicontinuous function: given a point (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x0`x0, Unknown identifier `μ0`μ0) strictly below the epigraph of Unknown identifier `f`f, produce a continuous affine minorant that lies below Unknown identifier `f`f everywhere and is strictly above Unknown identifier `μ0`μ0 at Unknown identifier `x0`x0. In particular, the Fenchel conjugate is finite at .

lemma section14_exists_affine_minorant_strict_of_lt [TopologicalSpace E] [IsTopologicalAddGroup E]
    [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal}
    (hf : ProperConvexERealFunction (F := E) f) (hf_closed : LowerSemicontinuous f) {x0 : E}
    {μ0 : ℝ} (hμ0 : (μ0 : EReal) < f x0) :
    ∃ (xStar : Module.Dual ℝ E) (β : ℝ),
      (∀ x : E, ((xStar x - β : ℝ) : EReal) ≤ f x) ∧ (μ0 : ℝ) < xStar x0 - β ∧
        fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f xStar < ⊤ := by
  classical
  -- Work with the real epigraph of `f` in `E × ℝ`.
  let epi : Set (E × ℝ) := {p | f p.1 ≤ (p.2 : EReal)}
  have hEpiConvex : Convex ℝ epi := by
    intro p hp q hq a b ha hb hab
    have hp' : f p.1 ≤ (p.2 : EReal) := hp
    have hq' : f q.1 ≤ (q.2 : EReal) := hq
    have hfconv : ConvexERealFunction (F := E) f := hf.2
    have hfconv' := hfconv (x := p.1) (y := q.1) (a := a) (b := b) ha hb hab
    have haE : (0 : EReal) ≤ (a : EReal) := by simpa [EReal.coe_nonneg] using ha
    have hbE : (0 : EReal) ≤ (b : EReal) := by simpa [EReal.coe_nonneg] using hb
    have hmul_p : (a : EReal) * f p.1 ≤ (a : EReal) * (p.2 : EReal) :=
      mul_le_mul_of_nonneg_left hp' haE
    have hmul_q : (b : EReal) * f q.1 ≤ (b : EReal) * (q.2 : EReal) :=
      mul_le_mul_of_nonneg_left hq' hbE
    have hsum :
        (a : EReal) * f p.1 + (b : EReal) * f q.1 ≤
          (a : EReal) * (p.2 : EReal) + (b : EReal) * (q.2 : EReal) :=
      add_le_add hmul_p hmul_q
    have hfst : (a • p + b • q).1 = a • p.1 + b • q.1 := by rfl
    have hsnd : (a • p + b • q).2 = a • p.2 + b • q.2 := by rfl
    have hle :
        f (a • p.1 + b • q.1) ≤ (a : EReal) * (p.2 : EReal) + (b : EReal) * (q.2 : EReal) :=
      hfconv'.trans hsum
    have hrhs :
        (a : EReal) * (p.2 : EReal) + (b : EReal) * (q.2 : EReal) =
          ((a • p.2 + b • q.2 : ℝ) : EReal) := by
      simp [smul_eq_mul]
    have hle' : f (a • p.1 + b • q.1) ≤ ((a • p.2 + b • q.2 : ℝ) : EReal) :=
      hle.trans_eq hrhs
    have : f ((a • p + b • q).1) ≤ ((a • p + b • q).2 : EReal) := by
      simpa [hfst, hsnd] using hle'
    simpa [epi] using this
  have hEpiClosed : IsClosed epi := by
    -- Use the closedness of the epigraph of `f : E → EReal` and pull back along `ℝ → EReal`.
    let epi' : Set (E × EReal) := {p | f p.1 ≤ p.2}
    have hEpi'Closed : IsClosed epi' := hf_closed.isClosed_epigraph
    have hcont :
        Continuous (fun p : E × ℝ => (p.1, (p.2 : EReal))) :=
      Continuous.prodMk continuous_fst (continuous_coe_real_ereal.comp continuous_snd)
    have hpre :
        epi = (fun p : E × ℝ => (p.1, (p.2 : EReal))) ⁻¹' epi' := by
      ext p
      rfl
    simpa [hpre, epi'] using hEpi'Closed.preimage hcont

  have hx0not : (x0, μ0) ∉ epi := by
    intro hx0
    have hx0' : f x0 ≤ (μ0 : EReal) := by simpa [epi] using hx0
    exact (not_le_of_gt hμ0) hx0'

  -- Separate the point `(x0, μ0)` from the epigraph.
  obtain ⟨L0, u0, hL0u0, hu0⟩ :=
    geometric_hahn_banach_closed_point (E := E × ℝ) (s := epi) (x := (x0, μ0)) hEpiConvex
      hEpiClosed hx0not

  -- Pick a finite point `x1` of `f` from properness; it will control the vertical coefficients.
  rcases hf.1.2 with ⟨x1, hx1neTop⟩
  have hx1dom : x1 ∈ erealDom f := lt_top_iff_ne_top.2 hx1neTop
  rcases section14_eq_coe_of_lt_top (z := f x1) hx1dom (hf.1.1 x1) with ⟨r1, hr1⟩

  -- A separator bounded above on the epigraph must have nonpositive `ℝ`-coefficient.
  have ht_nonpos (L : StrongDual ℝ (E × ℝ)) (u : ℝ) (hLu : ∀ p ∈ epi, L p < u) :
      L ((0 : E), (1 : ℝ)) ≤ 0 := by
    by_contra ht
    have htpos : 0 < L ((0 : E), (1 : ℝ)) := lt_of_not_ge ht
    have hx1mem : (x1, r1) ∈ epi := by
      have : f x1 ≤ (r1 : EReal) := by simp [hr1]
      simpa [epi] using this
    have hbase : L (x1, r1) < u := hLu (x1, r1) hx1mem
    obtain ⟨n : ℕ, hn⟩ :
        ∃ n : ℕ, (u - L (x1, r1)) / L ((0 : E), (1 : ℝ)) < n :=
      exists_nat_gt ((u - L (x1, r1)) / L ((0 : E), (1 : ℝ)))
    have hmul : u - L (x1, r1) < (n : ℝ) * L ((0 : E), (1 : ℝ)) := by
      have : (u - L (x1, r1)) / L ((0 : E), (1 : ℝ)) < (n : ℝ) := by simpa using hn
      exact (div_lt_iff₀ htpos).1 this
    have hn0 : (0 : ℝ) ≤ (n : ℝ) := by exact_mod_cast (Nat.cast_nonneg n)
    have hx1memn : (x1, r1 + (n : ℝ)) ∈ epi := by
      have : (r1 : EReal) ≤ ((r1 + (n : ℝ) : ℝ) : EReal) :=
        EReal.coe_le_coe (by linarith [hn0])
      have : f x1 ≤ ((r1 + (n : ℝ) : ℝ) : EReal) := by simpa [hr1] using this
      simpa [epi] using this
    have hlt : L (x1, r1 + (n : ℝ)) < u := hLu (x1, r1 + (n : ℝ)) hx1memn
    have hLr :
        L (x1, r1 + (n : ℝ)) =
          L (x1, r1) + (n : ℝ) * L ((0 : E), (1 : ℝ)) := by
      have hr : (x1, r1 + (n : ℝ)) = (x1, r1) + ((0 : E), (n : ℝ)) := by
        ext <;> simp
      have hn : ((0 : E), (n : ℝ)) = (n : ℝ) • ((0 : E), (1 : ℝ)) := by
        ext <;> simp [Prod.smul_mk, smul_eq_mul]
      have h0 : L ((0 : E), (n : ℝ)) = (n : ℝ) * L ((0 : E), (1 : ℝ)) := by
        calc
          L ((0 : E), (n : ℝ)) = L ((n : ℝ) • ((0 : E), (1 : ℝ))) := congrArg L hn
          _ = (n : ℝ) • L ((0 : E), (1 : ℝ)) := by
            simpa using (map_smul L (n : ℝ) ((0 : E), (1 : ℝ)))
          _ = (n : ℝ) * L ((0 : E), (1 : ℝ)) := by simp [smul_eq_mul]
      calc
        L (x1, r1 + (n : ℝ)) = L ((x1, r1) + ((0 : E), (n : ℝ))) := congrArg L hr
        _ = L (x1, r1) + L ((0 : E), (n : ℝ)) := by
          simpa using (map_add L (x1, r1) ((0 : E), (n : ℝ)))
        _ = L (x1, r1) + (n : ℝ) * L ((0 : E), (1 : ℝ)) := by simp [h0]
    have hlt' : L (x1, r1) + (n : ℝ) * L ((0 : E), (1 : ℝ)) < u := by
      simpa [hLr] using hlt
    have hgt' : u < L (x1, r1) + (n : ℝ) * L ((0 : E), (1 : ℝ)) := by
      linarith [hmul]
    exact (not_lt_of_gt hgt') hlt'

  have ht0_le : L0 ((0 : E), (1 : ℝ)) ≤ 0 := ht_nonpos L0 u0 hL0u0

  -- Build a second separator with negative vertical coefficient, then scale it so `g(0,1)=-1`.
  set μ1 : ℝ := r1 - 1
  have hμ1 : (μ1 : EReal) < f x1 := by
    have : (μ1 : ℝ) < r1 := by linarith
    simpa [μ1, hr1] using (EReal.coe_lt_coe this)
  have hx1not : (x1, μ1) ∉ epi := by
    intro hx1mem
    have : f x1 ≤ (μ1 : EReal) := by simpa [epi] using hx1mem
    exact (not_le_of_gt hμ1) this
  obtain ⟨L1, u1, hL1u1, hu1⟩ :=
    geometric_hahn_banach_closed_point (E := E × ℝ) (s := epi) (x := (x1, μ1)) hEpiConvex
      hEpiClosed hx1not
  have ht1_le : L1 ((0 : E), (1 : ℝ)) ≤ 0 := ht_nonpos L1 u1 hL1u1
  have ht1_ne : L1 ((0 : E), (1 : ℝ)) ≠ 0 := by
    intro ht1
    have hx1mem : (x1, r1) ∈ epi := by
      have : f x1 ≤ (r1 : EReal) := by simp [hr1]
      simpa [epi] using this
    have hL1x1r1 : L1 (x1, r1) < u1 := hL1u1 (x1, r1) hx1mem
    have hEq : L1 (x1, μ1) = L1 (x1, r1) := by
      have hr : (x1, μ1) = (x1, r1) + ((0 : E), (μ1 - r1)) := by
        ext <;> simp [μ1, sub_eq_add_neg, add_comm, add_left_comm]
      have hn : ((0 : E), (μ1 - r1)) = (μ1 - r1) • ((0 : E), (1 : ℝ)) := by
        ext <;> simp [Prod.smul_mk, smul_eq_mul]
      have h0 : L1 ((0 : E), (μ1 - r1)) = (μ1 - r1) * L1 ((0 : E), (1 : ℝ)) := by
        calc
          L1 ((0 : E), (μ1 - r1)) = L1 ((μ1 - r1) • ((0 : E), (1 : ℝ))) := congrArg L1 hn
          _ = (μ1 - r1) • L1 ((0 : E), (1 : ℝ)) := by
            simpa using (map_smul L1 (μ1 - r1) ((0 : E), (1 : ℝ)))
          _ = (μ1 - r1) * L1 ((0 : E), (1 : ℝ)) := by simp [smul_eq_mul]
      calc
        L1 (x1, μ1) = L1 ((x1, r1) + ((0 : E), (μ1 - r1))) := congrArg L1 hr
        _ = L1 (x1, r1) + L1 ((0 : E), (μ1 - r1)) := by
          simpa using (map_add L1 (x1, r1) ((0 : E), (μ1 - r1)))
        _ = L1 (x1, r1) + (μ1 - r1) * L1 ((0 : E), (1 : ℝ)) := by simp [h0]
        _ = L1 (x1, r1) := by simp [ht1]
    have : u1 < u1 := lt_trans hu1 (by simpa [hEq] using hL1x1r1)
    exact (lt_irrefl _ this)
  have ht1 : L1 ((0 : E), (1 : ℝ)) < 0 := lt_of_le_of_ne ht1_le ht1_ne

  set a : ℝ := (-1) / L1 ((0 : E), (1 : ℝ))
  have ha_pos : 0 < a := by
    have hnum : (-1 : ℝ) < 0 := by norm_num
    simpa [a] using (div_pos_of_neg_of_neg hnum ht1)
  let g : StrongDual ℝ (E × ℝ) := a • L1
  set M : ℝ := a * u1
  have hg_bound : ∀ p ∈ epi, g p ≤ M := by
    intro p hp
    have : L1 p < u1 := hL1u1 p hp
    have : a * L1 p < a * u1 := mul_lt_mul_of_pos_left this ha_pos
    have : g p < M := by simpa [g, M, smul_eq_mul, mul_assoc] using this
    exact le_of_lt this
  have hg01 : g ((0 : E), (1 : ℝ)) = -1 := by
    have ht1ne : L1 ((0 : E), (1 : ℝ)) ≠ 0 := ht1_ne
    simp [g, a, smul_eq_mul, div_eq_mul_inv, ht1ne]

  -- Perturb `L0` in the direction `g` to ensure a strictly negative vertical coefficient.
  set x0μ : E × ℝ := (x0, μ0)
  have hΔ : 0 < L0 x0μ - u0 := sub_pos.2 hu0
  set denom : ℝ := 2 * (|M - g x0μ| + 1)
  have hdenom_pos : 0 < denom := by
    have : 0 < |M - g x0μ| + 1 := by linarith [abs_nonneg (M - g x0μ)]
    have : 0 < (2 : ℝ) * (|M - g x0μ| + 1) := mul_pos (by norm_num) this
    simpa [denom, mul_assoc] using this
  set ε : ℝ := (L0 x0μ - u0) / denom
  have hε_pos : 0 < ε := div_pos hΔ hdenom_pos
  have hε_nonneg : 0 ≤ ε := le_of_lt hε_pos
  let L : StrongDual ℝ (E × ℝ) := L0 + ε • g
  let u : ℝ := u0 + ε * M

  have hLuEpi : ∀ p ∈ epi, L p < u := by
    intro p hp
    have hL0 : L0 p < u0 := hL0u0 p hp
    have hg : g p ≤ M := hg_bound p hp
    have hgmul : ε * g p ≤ ε * M := mul_le_mul_of_nonneg_left hg hε_nonneg
    have : L0 p + ε * g p < u0 + ε * M := add_lt_add_of_lt_of_le hL0 hgmul
    simpa [L, u, smul_eq_mul, add_assoc, add_left_comm, add_comm] using this

  have hu : u < L x0μ := by
    have habs_lt : |M - g x0μ| < |M - g x0μ| + 1 := by
      linarith [abs_nonneg (M - g x0μ)]
    have hmul_lt : ε * |M - g x0μ| < ε * (|M - g x0μ| + 1) :=
      mul_lt_mul_of_pos_left habs_lt hε_pos
    have hmul_eq : ε * (|M - g x0μ| + 1) = (L0 x0μ - u0) / 2 := by
      have hne : 2 * (|M - g x0μ| + 1) ≠ 0 := by linarith
      calc
        ε * (|M - g x0μ| + 1) = ((L0 x0μ - u0) / denom) * (|M - g x0μ| + 1) := by
          simp [ε]
        _ = (L0 x0μ - u0) / 2 := by
          field_simp [denom, hne]
          ring
    have hmul_abs : ε * |M - g x0μ| < L0 x0μ - u0 := by
      have : (L0 x0μ - u0) / 2 < (L0 x0μ - u0) := by linarith [hΔ]
      exact (hmul_lt.trans_eq hmul_eq).trans this
    have hmul :
        ε * (M - g x0μ) < L0 x0μ - u0 := by
      have hle : ε * (M - g x0μ) ≤ ε * |M - g x0μ| :=
        mul_le_mul_of_nonneg_left (le_abs_self _) hε_nonneg
      exact lt_of_le_of_lt hle hmul_abs
    have : u0 + ε * M < L0 x0μ + ε * g x0μ := by
      -- rearrange to `ε*(M - g x0μ) < L0 x0μ - u0`
      linarith [hmul]
    simpa [L, u, smul_eq_mul, add_assoc, add_left_comm, add_comm] using this

  have ht : L ((0 : E), (1 : ℝ)) < 0 := by
    have htle : L ((0 : E), (1 : ℝ)) ≤ -ε := by
      have hL01 :
          L ((0 : E), (1 : ℝ)) =
            L0 ((0 : E), (1 : ℝ)) + ε * g ((0 : E), (1 : ℝ)) := by
        simp [L, smul_eq_mul]
      have hL01' : L ((0 : E), (1 : ℝ)) = L0 ((0 : E), (1 : ℝ)) - ε := by
        calc
          L ((0 : E), (1 : ℝ)) = L0 ((0 : E), (1 : ℝ)) + ε * g ((0 : E), (1 : ℝ)) := hL01
          _ = L0 ((0 : E), (1 : ℝ)) - ε := by simp [hg01, sub_eq_add_neg]
      have hle : L0 ((0 : E), (1 : ℝ)) - ε ≤ -ε := by linarith [ht0_le]
      simpa [hL01'] using hle
    exact lt_of_le_of_lt htle (by linarith [hε_pos])

  -- Decompose `L` into an `E`-part and a vertical coefficient.
  let φ : E →L[ℝ] ℝ := (L : (E × ℝ) →L[ℝ] ℝ).comp (ContinuousLinearMap.inl ℝ E ℝ)
  set t : ℝ := L ((0 : E), (1 : ℝ))
  have ht' : t < 0 := by simpa [t] using ht
  have ht_ne : t ≠ 0 := ne_of_lt ht'

  have hdecomp : ∀ x r, L (x, r) = φ x + t * r := by
    intro x r
    have hr : (x, r) = (x, (0 : ℝ)) + ((0 : E), r) := by
      ext <;> simp
    have h0 : L ((0 : E), r) = r * t := by
      have hr0 : ((0 : E), r) = r • ((0 : E), (1 : ℝ)) := by
        ext <;> simp [Prod.smul_mk, smul_eq_mul]
      calc
        L ((0 : E), r) = L (r • ((0 : E), (1 : ℝ))) := congrArg L hr0
        _ = r • L ((0 : E), (1 : ℝ)) := by simpa using (map_smul L r ((0 : E), (1 : ℝ)))
        _ = r * t := by simp [t, smul_eq_mul]
    calc
      L (x, r) = L ((x, (0 : ℝ)) + ((0 : E), r)) := by
        exact congrArg L hr
      _ = L (x, (0 : ℝ)) + L ((0 : E), r) := by
        simpa using (map_add L (x, (0 : ℝ)) ((0 : E), r))
      _ = φ x + t * r := by
        -- `φ x = L (x,0)` by definition, and `L(0,r) = r*t`.
        simp [φ, h0, t]
        ring

  -- Use the positive constant `c = (-1)/t` to package the affine minorant.
  let c : ℝ := (-1) / t
  have hc_pos : 0 < c := by
    have hnum : (-1 : ℝ) < 0 := by norm_num
    simpa [c] using (div_pos_of_neg_of_neg hnum ht')
  let xStar : Module.Dual ℝ E := c • (φ : E →ₗ[ℝ] ℝ)
  let β : ℝ := c * u

  have hminor : ∀ x : E, ((xStar x - β : ℝ) : EReal) ≤ f x := by
    intro x
    by_cases hx : f x < ⊤
    · have hxDom : x ∈ erealDom f := hx
      rcases section14_eq_coe_of_lt_top (z := f x) hxDom (hf.1.1 x) with ⟨rx, hrx⟩
      have hxmem : (x, rx) ∈ epi := by
        have : f x ≤ (rx : EReal) := by simp [hrx]
        simpa [epi] using this
      have hlt : L (x, rx) < u := hLuEpi (x, rx) hxmem
      have hlt' : φ x + t * rx < u := by simpa [hdecomp] using hlt
      have hc_t : c * (-t) = 1 := by
        have htne : t ≠ 0 := ht_ne
        dsimp [c]
        calc
          ((-1 : ℝ) / t) * (-t) = ((-1 : ℝ) * (-t)) / t := by
            simpa using (div_mul_eq_mul_div (-1 : ℝ) t (-t))
          _ = t / t := by simp
          _ = (1 : ℝ) := div_self htne
      have hxStarβ : xStar x - β = c * (φ x - u) := by
        dsimp [xStar, β]
        simp [mul_sub]
      have hφ : φ x - u < (-t) * rx := by linarith [hlt']
      have : c * (φ x - u) < c * ((-t) * rx) := mul_lt_mul_of_pos_left hφ hc_pos
      have : c * (φ x - u) < rx := by
        -- Simplify the right-hand side using `c * (-t) = 1`.
        calc
          c * (φ x - u) < c * ((-t) * rx) := this
          _ = (c * (-t)) * rx := by simp [mul_assoc]
          _ = rx := by simp [hc_t]
      have hxlt : xStar x - β < rx := by simpa [hxStarβ] using this
      have hxle : (xStar x - β) ≤ rx := le_of_lt hxlt
      have hxleE : ((xStar x - β : ℝ) : EReal) ≤ (rx : EReal) := EReal.coe_le_coe hxle
      simpa [hrx] using hxleE
    · have hxTop : f x = ⊤ := by
        -- `¬ f x < ⊤` means `f x = ⊤`.
        simpa [lt_top_iff_ne_top] using hx
      rw [hxTop]
      exact le_top
  have hstrict : (μ0 : ℝ) < xStar x0 - β := by
    have hc_t : c * (-t) = 1 := by
      have htne : t ≠ 0 := ht_ne
      dsimp [c]
      calc
        ((-1 : ℝ) / t) * (-t) = ((-1 : ℝ) * (-t)) / t := by
          simpa using (div_mul_eq_mul_div (-1 : ℝ) t (-t))
        _ = t / t := by simp
        _ = (1 : ℝ) := div_self htne
    have hxStarβ : xStar x0 - β = c * (φ x0 - u) := by
      dsimp [xStar, β]
      simp [mul_sub]
    have hu' : u < L (x0, μ0) := hu
    have hu'' : u < φ x0 + t * μ0 := by simpa [hdecomp] using hu'
    have hφ : (-t) * μ0 < φ x0 - u := by linarith [hu'']
    have : c * ((-t) * μ0) < c * (φ x0 - u) := mul_lt_mul_of_pos_left hφ hc_pos
    have : μ0 < c * (φ x0 - u) := by
      calc
        μ0 = (c * (-t)) * μ0 := by simp [hc_t]
        _ = c * ((-t) * μ0) := by simp [mul_assoc]
        _ < c * (φ x0 - u) := this
    simpa [hxStarβ] using this

  have hxStar_finite :
      fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f xStar < ⊤ := by
    set p : E →ₗ[ℝ] (Module.Dual ℝ E) →ₗ[ℝ] ℝ :=
      (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))
    have hle : fenchelConjugateBilin p f xStar ≤ (β : EReal) := by
      unfold fenchelConjugateBilin
      refine sSup_le ?_
      rintro _ ⟨x, rfl⟩
      have hminor' : ((xStar x : ℝ) : EReal) - (β : EReal) ≤ f x := by
        simpa [EReal.coe_sub] using hminor x
      have hxle : ((xStar x : ℝ) : EReal) ≤ f x + (β : EReal) :=
        (EReal.sub_le_iff_le_add (h₁ := Or.inl (by simp : (β : EReal) ≠ ⊥))
              (h₂ := Or.inl (by simp : (β : EReal) ≠ ⊤))).1 hminor'
      have hxle' : ((xStar x : ℝ) : EReal) ≤ (β : EReal) + f x := by
        simpa [add_comm, add_left_comm, add_assoc] using hxle
      have : ((xStar x : ℝ) : EReal) - f x ≤ (β : EReal) :=
        (EReal.sub_le_iff_le_add (h₁ := Or.inl (hf.1.1 x)) (h₂ := Or.inr (by simp))).2
          (by simpa [add_comm] using hxle')
      simpa [p, LinearMap.applyₗ] using this
    have hβ : (β : EReal) < ⊤ := by simp
    exact lt_of_le_of_lt hle hβ

  exact ⟨xStar, β, hminor, hstrict, hxStar_finite⟩

For a proper convex lower semicontinuous function, the Fenchel conjugate is finite somewhere.

lemma section14_exists_mem_dom_fenchelConjugate_of_properConvex_lsc [TopologicalSpace E]
    [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E]
    {f : E → EReal} (hf : ProperConvexERealFunction (F := E) f) (hf_closed : LowerSemicontinuous f) :
    (erealDom (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)).Nonempty := by
  rcases hf.1.2 with ⟨x0, hx0neTop⟩
  have hx0 : f x0 < ⊤ := lt_top_iff_ne_top.2 hx0neTop
  rcases section14_eq_coe_of_lt_top (z := f x0) hx0 (hf.1.1 x0) with ⟨r0, hr0⟩
  set μ0 : ℝ := r0 - 1
  have hμ0 : (μ0 : EReal) < f x0 := by
    have : (μ0 : ℝ) < r0 := by linarith
    simpa [μ0, hr0] using (EReal.coe_lt_coe this)
  rcases
      section14_exists_affine_minorant_strict_of_lt (E := E) (f := f) hf hf_closed (x0 := x0)
        (μ0 := μ0) hμ0 with
    ⟨xStar, β, -, -, hxStarFin⟩
  refine ⟨xStar, ?_⟩
  simpa [erealDom] using hxStarFin

If Unknown identifier `y`y is nonpositive on and Unknown identifier `f`f is proper convex and closed, then Unknown identifier `y`y is a recession direction of Unknown identifier `f`f.

lemma section14_mem_recessionConeEReal_of_forall_mem_dom_fenchelConjugate_le_zero
    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E]
    {f : E → EReal} (hf : ProperConvexERealFunction (F := E) f)
    (hf_closed : LowerSemicontinuous f) {y : E}
    (hy : ∀ xStar : Module.Dual ℝ E,
      xStar ∈ erealDom (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f) →
        xStar y ≤ 0) :
    y ∈ recessionConeEReal (F := E) f := by
  classical
  refine (section14_mem_recessionConeEReal_iff (g := f) (y := y)).2 ?_
  intro x hxDom
  have hxBot : f x ≠ ⊥ := hf.1.1 x
  rcases section14_eq_coe_of_lt_top (z := f x) hxDom hxBot with ⟨rx, hrx⟩
  -- We show `f (x+y) ≤ f x` by contradiction using an affine minorant at `x+y`.
  have hxy_le : f (x + y) ≤ f x := by
    by_contra hnot
    have hlt : f x < f (x + y) := lt_of_not_ge hnot
    by_cases hxy : f (x + y) < ⊤
    · rcases section14_eq_coe_of_lt_top (z := f (x + y)) hxy (hf.1.1 (x + y)) with
        ⟨rxy, hrxy⟩
      have hr_lt : rx < rxy := by
        have : (rx : EReal) < (rxy : EReal) := by simpa [hrx, hrxy] using hlt
        exact (EReal.coe_lt_coe_iff).1 this
      let μ0 : ℝ := (rx + rxy) / 2
      have hμ0_gt : rx < μ0 := by
        dsimp [μ0]
        linarith [hr_lt]
      have hμ0_lt : (μ0 : EReal) < f (x + y) := by
        have : (μ0 : ℝ) < rxy := by
          dsimp [μ0]
          linarith [hr_lt]
        simpa [μ0, hrxy] using (EReal.coe_lt_coe this)
      rcases
          section14_exists_affine_minorant_strict_of_lt (E := E) (f := f) hf hf_closed
            (x0 := x + y) (μ0 := μ0) hμ0_lt with
        ⟨xStar, β, hminor, hstrict, hxStarFin⟩
      have hxStarDom :
          xStar ∈
            erealDom
              (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f) := by
        simpa [erealDom] using hxStarFin
      have hyx : xStar y ≤ 0 := hy xStar hxStarDom
      have hle_xy : xStar (x + y) - β ≤ xStar x - β := by
        have : xStar (x + y) = xStar x + xStar y := by simp [map_add]
        have hle : xStar x + xStar y ≤ xStar x := add_le_of_nonpos_right hyx
        have : xStar x + xStar y - β ≤ xStar x - β := sub_le_sub_right hle β
        simpa [this, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using this
      have hstrict' : (μ0 : ℝ) < xStar x - β := lt_of_lt_of_le hstrict hle_xy
      have hxminor : (xStar x - β : ℝ) ≤ rx := by
        have : ((xStar x - β : ℝ) : EReal) ≤ f x := hminor x
        have : ((xStar x - β : ℝ) : EReal) ≤ (rx : EReal) := by simpa [hrx] using this
        exact (EReal.coe_le_coe_iff).1 this
      have : (μ0 : ℝ) < rx := lt_of_lt_of_le hstrict' hxminor
      exact (not_lt_of_gt hμ0_gt) this
    · have hxyTop : f (x + y) = ⊤ := by
        simpa [lt_top_iff_ne_top] using hxy
      set μ0 : ℝ := rx + 1
      have hμ0_gt : rx < μ0 := by linarith
      have hμ0_lt : (μ0 : EReal) < f (x + y) := by simp [hxyTop]
      rcases
          section14_exists_affine_minorant_strict_of_lt (E := E) (f := f) hf hf_closed
            (x0 := x + y) (μ0 := μ0) hμ0_lt with
        ⟨xStar, β, hminor, hstrict, hxStarFin⟩
      have hxStarDom :
          xStar ∈
            erealDom
              (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f) := by
        simpa [erealDom] using hxStarFin
      have hyx : xStar y ≤ 0 := hy xStar hxStarDom
      have hle_xy : xStar (x + y) - β ≤ xStar x - β := by
        have : xStar (x + y) = xStar x + xStar y := by simp [map_add]
        have hle : xStar x + xStar y ≤ xStar x := add_le_of_nonpos_right hyx
        have : xStar x + xStar y - β ≤ xStar x - β := sub_le_sub_right hle β
        simpa [this, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using this
      have hstrict' : (μ0 : ℝ) < xStar x - β := lt_of_lt_of_le hstrict hle_xy
      have hxminor : (xStar x - β : ℝ) ≤ rx := by
        have : ((xStar x - β : ℝ) : EReal) ≤ f x := hminor x
        have : ((xStar x - β : ℝ) : EReal) ≤ (rx : EReal) := by simpa [hrx] using this
        exact (EReal.coe_le_coe_iff).1 this
      have : (μ0 : ℝ) < rx := lt_of_lt_of_le hstrict' hxminor
      exact (not_lt_of_gt hμ0_gt) this
  exact (EReal.sub_nonpos).2 hxy_le

If is in polarCone (recessionConeEReal sorry) : Set (Module.Dual ℝ ?m.4)polarCone (recessionConeEReal Unknown identifier `f`f), then lies in the weak closure of the conic hull of (dual part of Theorem 14.2).

lemma section14_polar_recessionCone_subset_closure_coneHull_dom_fenchelConjugate
    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E]
    {f : E → EReal} (hf : ProperConvexERealFunction (F := E) f) (hf_closed : LowerSemicontinuous f) :
    polarCone (E := E) (recessionConeEReal (F := E) f) ⊆
      closure
        ((ConvexCone.hull ℝ
              (erealDom
                (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
            ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) := by
  classical
  intro xStar hxStar
  by_contra hxStar_cl
  have hDom :
      (erealDom
          (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)).Nonempty :=
    section14_exists_mem_dom_fenchelConjugate_of_properConvex_lsc (E := E) (f := f) hf hf_closed
  rcases
      section14_exists_eval_sep_of_not_mem_closure_coneHull_dom_fenchelConjugate (E := E) (f := f)
        (xStar := xStar) hDom hxStar_cl with
    ⟨y, hy, hpos⟩
  have hyDom :
      ∀ z : Module.Dual ℝ E,
        z ∈ erealDom (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f) →
          z y ≤ 0 := by
    intro z hzDom
    have hzHull :
        z ∈
            ((ConvexCone.hull ℝ
                    (erealDom
                      (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
                ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) :=
      (ConvexCone.subset_hull (s :=
        erealDom (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f))) hzDom
    have hzCl :
        z ∈
            closure
              ((ConvexCone.hull ℝ
                    (erealDom
                      (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
                ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) :=
      subset_closure hzHull
    exact hy z hzCl
  have hyRec :
      y ∈ recessionConeEReal (F := E) f :=
    section14_mem_recessionConeEReal_of_forall_mem_dom_fenchelConjugate_le_zero (E := E) (f := f)
      (hf := hf) hf_closed hyDom
  have hxStar_ineq : xStar y ≤ 0 :=
    (mem_polarCone_iff (E := E) (K := recessionConeEReal (F := E) f) (φ := xStar)).1 hxStar y hyRec
  exact (not_lt_of_ge hxStar_ineq) hpos

Theorem 14.2 (dual statement). If Unknown identifier `f`f is closed, then the polar of the recession cone of Unknown identifier `f`f is the closure of the convex cone generated by .

theorem polar_recessionCone_eq_closure_coneGenerated_dom_fenchelConjugate [TopologicalSpace E]
    [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E]
    {f : E → EReal} (hf : ProperConvexERealFunction (F := E) f) (hf_closed : LowerSemicontinuous f) :
    polarCone (E := E) (recessionConeEReal (F := E) f) =
      closure
        ((ConvexCone.hull ℝ
              (erealDom
                (fenchelConjugateBilin (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)) f)) :
              ConvexCone ℝ (Module.Dual ℝ E)) : Set (Module.Dual ℝ E)) := by
  classical
  refine subset_antisymm ?_ ?_
  ·
    exact
      section14_polar_recessionCone_subset_closure_coneHull_dom_fenchelConjugate (E := E) (f := f)
        hf hf_closed
  ·
    exact section14_closure_coneHull_dom_fenchelConjugate_subset_polar_recessionCone (E := E)
      (f := f) hf

Membership in a dual cone with respect to the flipped evaluation pairing is exactly a pointwise nonpositivity condition.

lemma section14_mem_dual_flip_eval_iff_forall_le_zero (S : Set (Module.Dual ℝ E)) (x : E) :
    x ∈
        (PointedCone.dual (R := ℝ)
              ((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip S :
            Set E) ↔
      ∀ φ : Module.Dual ℝ E, φ ∈ S → φ x ≤ 0 := by
  constructor
  · intro hx φ hφ
    have hx' :
        ∀ ⦃ψ : Module.Dual ℝ E⦄,
          ψ ∈ S →
            0 ≤
              ((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip ψ x := by
      simpa [PointedCone.mem_dual] using hx
    have : 0 ≤ ((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip φ x := hx' hφ
    have : 0 ≤ -(φ x) := by
      simpa [LinearMap.neg_apply, LinearMap.applyₗ] using this
    exact (neg_nonneg).1 this
  · intro hx
    refine
      (PointedCone.mem_dual
            (p := ((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip) (s := S)
            (y := x)).2 ?_
    intro φ hφ
    have hxle : φ x ≤ 0 := hx φ hφ
    have : 0 ≤ -(φ x) := (neg_nonneg).2 hxle
    simpa [LinearMap.neg_apply, LinearMap.applyₗ] using this

Recession directions lie in the polar (with respect to flipped evaluation) of the barrier cone.

lemma section14_recessionCone_subset_polar_barrierCone {C : Set E} (hCne : C.Nonempty) :
    Set.recessionCone C ⊆
      (PointedCone.dual (R := ℝ)
            ((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip (Set.barrierCone (E := E) C) :
          Set E) := by
  classical
  intro y hy
  refine
    (section14_mem_dual_flip_eval_iff_forall_le_zero (E := E) (S := Set.barrierCone (E := E) C)
          (x := y)).2 ?_
  intro φ hφ
  rcases hφ with ⟨β, hβ⟩
  rcases hCne with ⟨x0, hx0C⟩
  have hmul_le : ∀ n : ℕ, (n : ℝ) * (φ y) ≤ β - φ x0 := by
    intro n
    have hn : (0 : ℝ) ≤ (n : ℝ) := by exact_mod_cast (Nat.zero_le n)
    have hxny : x0 + (n : ℝ) • y ∈ C := hy (x := x0) hx0C (t := (n : ℝ)) hn
    have hbound : φ (x0 + (n : ℝ) • y) ≤ β := hβ (x0 + (n : ℝ) • y) hxny
    have hcalc : φ (x0 + (n : ℝ) • y) = φ x0 + (n : ℝ) * (φ y) := by
      simp [map_add, smul_eq_mul]
    have : φ x0 + (n : ℝ) * (φ y) ≤ β := by simpa [hcalc] using hbound
    linarith
  exact section14_real_nonpos_of_nat_mul_le (r := φ y) (C := β - φ x0) hmul_le

end Section14end Chap03