Convex Analysis (Rockafellar, 1970) -- Chapter 01 -- Section 05 -- Part 4

open scoped Pointwisesection Chap01section Section05

Text 5.4.9 (Infimum representation of the positively homogeneous hull): Assume Unknown identifier `h`h is not identically and let Unknown identifier `f`f be the positively homogeneous convex function generated by Unknown identifier `h`h. Then for all Unknown identifier `x`x. Moreover, may be omitted from the infimum if Unknown identifier `x`sorry ≠ 0 : Propx ≠ 0 or if .

theorem infimumRepresentation_posHomogeneousHull {n : Nat} {h : (Fin n → Real) → EReal}
    (hh : ConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) h)
    (hfinite : ∃ x, h x ≠ (⊤ : EReal)) :
    let f := positivelyHomogeneousConvexFunctionGenerated h;
    (∀ x : Fin n → Real,
      f x = sInf { z : EReal | ∃ lam : Real, 0 ≤ lam ∧ z = rightScalarMultiple h lam x })
    ∧
    (∀ x : Fin n → Real, (x ≠ 0 ∨ h 0 < (⊤ : EReal)) →
      f x = sInf { z : EReal | ∃ lam : Real, 0 < lam ∧ z = rightScalarMultiple h lam x }) := by
  classical
  set f := positivelyHomogeneousConvexFunctionGenerated h
  have hne_epi :
      Set.Nonempty (epigraph (Set.univ : Set (Fin n → Real)) h) := by
    rcases hfinite with ⟨x0, hx0⟩
    have hx0lt : h x0 < (⊤ : EReal) := (lt_top_iff_ne_top).2 hx0
    have hx0mem :
        x0 ∈ {x | x ∈ (Set.univ : Set (Fin n → Real)) ∧ h x < (⊤ : EReal)} :=
      ⟨by simp, hx0lt⟩
    have hx0eff : x0 ∈ effectiveDomain (Set.univ : Set (Fin n → Real)) h := by
      simpa [effectiveDomain_eq] using hx0mem
    have hne_eff :
        Set.Nonempty (effectiveDomain (Set.univ : Set (Fin n → Real)) h) := ⟨x0, hx0eff⟩
    exact (nonempty_epigraph_iff_nonempty_effectiveDomain (S := Set.univ) (f := h)).2 hne_eff
  have h1 :
      ∀ x : Fin n → Real,
        f x = sInf { z : EReal | ∃ lam : Real, 0 ≤ lam ∧ z = rightScalarMultiple h lam x } := by
    intro x
    set S0 : Set EReal :=
      { z : EReal | ∃ lam : Real, 0 ≤ lam ∧ z = rightScalarMultiple h lam x }
    apply le_antisymm
    · refine le_sInf ?_
      intro z hz
      rcases hz with ⟨lam, hlam, rfl⟩
      have hsubset :
          (fun μ : ℝ => (μ : EReal)) '' { μ : ℝ |
            (x, μ) ∈ Set.image (fun p : (Fin n → Real) × Real => lam • p)
              (epigraph (Set.univ : Set (Fin n → Real)) h) } ⊆
          (fun μ : ℝ => (μ : EReal)) '' { μ : ℝ |
            (x, μ) ∈ convexConeGeneratedEpigraph h } := by
        intro z hz
        rcases hz with ⟨μ, hμ, rfl⟩
        have hmem : (x, μ) ∈ convexConeGeneratedEpigraph h := by
          by_cases hpos : 0 < lam
          · rcases hμ with ⟨p, hp, hpeq⟩
            have hp' :
                p ∈ convexConeGeneratedEpigraph h := by
              have hp'' :
                  p ∈ (ConvexCone.hull ℝ (epigraph (Set.univ : Set (Fin n → Real)) h)) :=
                ConvexCone.subset_hull hp
              exact (Set.mem_insert_iff).2 (Or.inr hp'')
            have hsmul :
                lam • p ∈ convexConeGeneratedEpigraph h :=
              smul_mem_convexConeGeneratedEpigraph (h := h) hpos hp'
            simpa [hpeq] using hsmul
          · have hlam0 : lam = 0 := by
              exact le_antisymm (le_of_not_gt hpos) hlam
            subst hlam0
            have hxμ : (x, μ) = 0 := by
              rcases hμ with ⟨p, hp, hpeq⟩
              simpa using hpeq.symm
            have h0mem : (0 : (Fin n → Real) × Real) ∈ convexConeGeneratedEpigraph h := by
              exact (Set.mem_insert_iff).2 (Or.inl rfl)
            simpa [hxμ] using h0mem
        exact ⟨μ, hmem, rfl⟩
      have hle :
          sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ |
              (x, μ) ∈ convexConeGeneratedEpigraph h }) ≤
            sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ |
              (x, μ) ∈ Set.image (fun p : (Fin n → Real) × Real => lam • p)
                (epigraph (Set.univ : Set (Fin n → Real)) h) }) :=
        sInf_le_sInf hsubset
      simpa [f, positivelyHomogeneousConvexFunctionGenerated, rightScalarMultiple, S0] using hle
    · refine le_sInf ?_
      intro z hz
      rcases hz with ⟨μ, hμ, rfl⟩
      have hmem := (mem_convexConeGeneratedEpigraph_iff (h := h) hh).1 hμ
      rcases hmem with hzero | ⟨lam, hlam, hmem⟩
      · have hx0 : x = 0 := by
          simpa using congrArg Prod.fst hzero
        have hμ0 : μ = 0 := by
          simpa using congrArg Prod.snd hzero
        subst hx0 hμ0
        have hval := rightScalarMultiple_zero_eval (f := h) hne_epi (0)
        have hmemS0 : (0 : EReal) ∈ S0 := by
          refine ⟨0, le_rfl, ?_⟩
          simp [hval]
        have hle : sInf S0 ≤ (0 : EReal) := sInf_le hmemS0
        simpa [S0] using hle
      · have hmemS0 : rightScalarMultiple h lam x ∈ S0 := by
          exact ⟨lam, le_of_lt hlam, rfl⟩
        have hleS0 : sInf S0 ≤ rightScalarMultiple h lam x := sInf_le hmemS0
        have hmem' :
            ((μ : Real) : EReal) ∈
              (fun μ : ℝ => (μ : EReal)) '' { μ : ℝ |
                (x, μ) ∈
                  Set.image (fun p : (Fin n → Real) × Real => lam • p)
                    (epigraph (Set.univ : Set (Fin n → Real)) h) } := by
          exact ⟨μ, hmem, rfl⟩
        have hleμ : rightScalarMultiple h lam x ≤ (μ : EReal) := by
          simpa [rightScalarMultiple] using (sInf_le hmem')
        exact le_trans hleS0 hleμ
  refine And.intro h1 ?_
  · intro x hx
    -- Now convert to the positive-lambda infimum
    set S0 : Set EReal :=
      { z : EReal | ∃ lam : Real, 0 ≤ lam ∧ z = rightScalarMultiple h lam x }
    set Spos : Set EReal :=
      { z : EReal | ∃ lam : Real, 0 < lam ∧ z = rightScalarMultiple h lam x }
    have hset : S0 = Set.insert (rightScalarMultiple h 0 x) Spos := by
      simpa [S0, Spos] using (rightScalarMultiple_set_eq_insert (h := h) x)
    have hS0 :
        sInf S0 = rightScalarMultiple h 0 x ⊓ sInf Spos := by
      rw [hset]
      exact sInf_insert
    have hle : sInf Spos ≤ rightScalarMultiple h 0 x := by
      by_cases hx' : x = 0
      · subst hx'
        have hval := rightScalarMultiple_zero_eval (f := h) hne_epi (0)
        have hx0 : h 0 < (⊤ : EReal) := by
          rcases hx with hx | hx
          · exact (hx rfl).elim
          · exact hx
        have hle0 : sInf Spos ≤ (0 : EReal) := by
          exact sInf_rightScalarMultiple_pos_le_zero (h := h) hh hx0
        simpa [hval, Spos] using hle0
      · have hval := rightScalarMultiple_zero_eval (f := h) hne_epi x
        have htop : rightScalarMultiple h 0 x = (⊤ : EReal) := by
          simpa [hx'] using hval
        simp [htop]
    have hS0' : sInf S0 = sInf Spos := by
      calc
        sInf S0 = rightScalarMultiple h 0 x ⊓ sInf Spos := hS0
        _ = sInf Spos := by
            exact inf_eq_right.mpr hle
    have hmain' :
        f x =
          sInf { z : EReal | ∃ lam : Real, 0 < lam ∧ z = rightScalarMultiple h lam x } := by
      have hfirst : f x = sInf S0 := by
        simpa [S0] using h1 x
      simpa [Spos, hS0'] using hfirst
    simpa [Spos] using hmain'

The perspective kernel is convex when Unknown identifier `f`f is convex.

lemma convexFunctionOn_perspective_h {n : Nat} {f : (Fin n → Real) → EReal}
    (hf : ConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) f) :
    ConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real)))
      (fun y =>
        if y 0 = (1 : Real) then
          f (fun i => y i.succ)
        else
          (⊤ : EReal)) := by
  classical
  unfold ConvexFunctionOn
  intro p hp q hq a b ha hb hab
  have hp' :
      (if p.1 0 = (1 : Real) then f (fun i => p.1 i.succ) else (⊤ : EReal)) ≤
        (p.2 : EReal) :=
    (mem_epigraph_univ_iff
      (f := fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))).1 hp
  have hq' :
      (if q.1 0 = (1 : Real) then f (fun i => q.1 i.succ) else (⊤ : EReal)) ≤
        (q.2 : EReal) :=
    (mem_epigraph_univ_iff
      (f := fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))).1 hq
  have hp0 : p.1 0 = (1 : Real) := by
    by_contra hp0
    have htop : (⊤ : EReal) ≤ (p.2 : EReal) := by
      have hp'' := hp'
      rw [if_neg hp0] at hp''
      exact hp''
    exact (not_top_le_coe p.2) htop
  have hq0 : q.1 0 = (1 : Real) := by
    by_contra hq0
    have htop : (⊤ : EReal) ≤ (q.2 : EReal) := by
      have hq'' := hq'
      rw [if_neg hq0] at hq''
      exact hq''
    exact (not_top_le_coe q.2) htop
  have hp_f : f (fun i => p.1 i.succ) ≤ (p.2 : EReal) := by
    simpa [hp0] using hp'
  have hq_f : f (fun i => q.1 i.succ) ≤ (q.2 : EReal) := by
    simpa [hq0] using hq'
  have hconv_f :
      Convex ℝ (epigraph (Set.univ : Set (Fin n → Real)) f) := by
    simpa [ConvexFunctionOn] using hf
  have hp_epi :
      ((fun i => p.1 i.succ), p.2) ∈
        epigraph (Set.univ : Set (Fin n → Real)) f := by
    exact (mem_epigraph_univ_iff (f := f)).2 hp_f
  have hq_epi :
      ((fun i => q.1 i.succ), q.2) ∈
        epigraph (Set.univ : Set (Fin n → Real)) f := by
    exact (mem_epigraph_univ_iff (f := f)).2 hq_f
  have hcomb_epi :
      a • ((fun i => p.1 i.succ), p.2) + b • ((fun i => q.1 i.succ), q.2) ∈
        epigraph (Set.univ : Set (Fin n → Real)) f :=
    hconv_f hp_epi hq_epi ha hb hab
  have hcomb_le :
      f (a • (fun i => p.1 i.succ) + b • (fun i => q.1 i.succ)) ≤
        ((a * p.2 + b * q.2 : Real) : EReal) := by
    simpa [smul_eq_mul, mul_add, add_mul] using
      (mem_epigraph_univ_iff (f := f)).1 hcomb_epi
  have hy0 : (a • p + b • q).1 0 = (1 : Real) := by
    simp [hp0, hq0, hab, smul_eq_mul]
  have hy_succ :
      (fun i : Fin n => (a • p + b • q).1 i.succ) =
        a • (fun i : Fin n => p.1 i.succ) + b • (fun i : Fin n => q.1 i.succ) := by
    funext (i : Fin n)
    simp [Pi.smul_apply, smul_eq_mul]
  have hle :
      (if (a • p + b • q).1 0 = (1 : Real) then
          f (fun i => (a • p + b • q).1 i.succ)
        else
          (⊤ : EReal)) ≤ (a • p + b • q).2 := by
    simpa [hy0, hy_succ, smul_eq_mul, mul_add, add_mul] using hcomb_le
  exact
    (mem_epigraph_univ_iff
      (f := fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))).2 hle

For positive Unknown identifier `lam`lam, the first coordinate of Unknown identifier `lam`sorry⁻¹ • sorry : ?m.6lam⁻¹ • Unknown identifier `y`y equals 1 : ℕ1 iff Unknown identifier `y`sorry = sorry : Propy 0 = Unknown identifier `lam`lam.

lemma first_coord_inv_smul_eq_one {n : Nat} {lam : Real} (hlam : 0 < lam)
    (y : Fin (n + 1) → Real) : (lam⁻¹ • y) 0 = (1 : Real) ↔ y 0 = lam := by
  have hne : lam ≠ 0 := ne_of_gt hlam
  constructor
  · intro h
    have h0 : lam⁻¹ * y 0 = 1 := by
      simpa [Pi.smul_apply, smul_eq_mul] using h
    field_simp [hne] at h0
    exact h0
  · intro h
    simp [Pi.smul_apply, smul_eq_mul, h, hne]

Positive right scalar multiples of the perspective kernel simplify.

lemma rightScalarMultiple_perspective_h_pos {n : Nat} {f : (Fin n → Real) → EReal}
    (hf : ConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) f)
    {lam : Real} (hlam : 0 < lam) (y : Fin (n + 1) → Real) :
    rightScalarMultiple
        (fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))
        lam y =
      if y 0 = lam then ((lam : EReal) *
      f (lam⁻¹ • (fun i : Fin n => y i.succ))) else (⊤ : EReal) := by
  have hconv_h :
      ConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real)))
        (fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal)) :=
    convexFunctionOn_perspective_h (f := f) hf
  have hmul :=
    rightScalarMultiple_pos
      (f := fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))
      (lam := lam) hconv_h hlam y
  have hcond : (lam⁻¹ • y) 0 = (1 : Real) ↔ y 0 = lam :=
    first_coord_inv_smul_eq_one (n := n) (lam := lam) hlam y
  have hsmul :
      (fun i : Fin n => (lam⁻¹ • y) i.succ) = lam⁻¹ • (fun i : Fin n => y i.succ) := by
    funext i
    simp [Pi.smul_apply, smul_eq_mul]
  have hsmul' :
      lam⁻¹ • (fun i : Fin n => y i.succ) = (fun i : Fin n => lam⁻¹ * y i.succ) := by
    funext i
    simp [Pi.smul_apply, smul_eq_mul]
  by_cases hy : y 0 = lam
  · have hy' : lam⁻¹ * y 0 = (1 : Real) := by
      have hy'' : (lam⁻¹ • y) 0 = (1 : Real) := (hcond).2 hy
      simpa [Pi.smul_apply, smul_eq_mul] using hy''
    calc
      rightScalarMultiple
          (fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))
          lam y =
          ((lam : EReal) * f (fun i => lam⁻¹ * y i.succ)) := by
            simp [hmul, hy', Pi.smul_apply, smul_eq_mul]
      _ = ((lam : EReal) * f (lam⁻¹ • (fun i : Fin n => y i.succ))) := by
            simp [hsmul']
      _ =  if y 0 = lam then ((lam : EReal) *
        f (lam⁻¹ • (fun i : Fin n => y i.succ))) else (⊤ : EReal) := by
            simp [hy]
  · have hy' : lam⁻¹ * y 0 ≠ (1 : Real) := by
      intro h0
      apply hy
      apply (hcond).1
      simpa [Pi.smul_apply, smul_eq_mul] using h0
    calc
      rightScalarMultiple
          (fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))
          lam y = (⊤ : EReal) := by
            simp [hmul, hy', Pi.smul_apply, smul_eq_mul, EReal.coe_mul_top_of_pos hlam]
      _ = if y 0 = lam then
        ((lam : EReal) * f (lam⁻¹ • (fun i : Fin n => y i.succ))) else (⊤ : EReal) := by
            simp [hy]

A positive scalar multiple of a non-⊥ EReal : TypeEReal is non-⊥.

lemma ereal_mul_ne_bot_of_pos' {t : Real} (ht : 0 < t) {x : EReal} (hx : x ≠ (⊥ : EReal)) :
    ((t : Real) : EReal) * x ≠ (⊥ : EReal) := by
  cases x using EReal.rec with
  | bot =>
      exact (hx rfl).elim
  | coe r =>
      simp [← EReal.coe_mul]
  | top =>
      simp [EReal.coe_mul_top_of_pos ht]

The perspective kernel has a nonempty epigraph when Unknown identifier `f`f is proper.

lemma nonempty_epigraph_perspective_h {n : Nat} {f : (Fin n → Real) → EReal}
    (hf : ProperConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) f) :
    Set.Nonempty
      (epigraph (Set.univ : Set (Fin (n + 1) → Real))
        (fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))) := by
  rcases hf.2.1 with ⟨⟨x0, μ⟩, hx0⟩
  have hx0' : f x0 ≤ (μ : EReal) := by
    exact (mem_epigraph_univ_iff (f := f)).1 hx0
  let y : Fin (n + 1) → Real := fun i => Fin.cases (1 : Real) x0 i
  have hy0 : y 0 = (1 : Real) := by
    simp [y]
  have hy_succ : (fun i : Fin n => y i.succ) = x0 := by
    funext i
    simp [y]
  have hy_le :
      (if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal)) ≤
        (μ : EReal) := by
    simpa [hy0, hy_succ] using hx0'
  refine ⟨(y, μ), ?_⟩
  exact
    (mem_epigraph_univ_iff
      (f := fun y => if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal))).2 hy_le

Text 5.4.9.1: Perspective as a positively homogeneous convex function. Let Unknown identifier `f`f be a proper convex function on ℝ ^ sorry : Typeℝ^Unknown identifier `n`n. Define for (with the closed perspective convention at ) and for . Then Unknown identifier `g`g is proper, convex, and positively homogeneous on ℝ ^ {sorry + 1} : Typeℝ^{Unknown identifier `n`n+1}; moreover, Unknown identifier `g`g coincides with the positively homogeneous convex function generated by when and otherwise.

theorem perspective_posHomogeneous_convex {n : Nat} {f : (Fin n → Real) → EReal}
    (hf : ProperConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) f) :
    let g : (Fin (n + 1) → Real) → EReal :=
      fun y =>
        if 0 ≤ y 0 then
          rightScalarMultiple f (y 0) (fun i => y i.succ)
        else
          (⊤ : EReal)
    let h : (Fin (n + 1) → Real) → EReal :=
      fun y =>
        if y 0 = (1 : Real) then
          f (fun i => y i.succ)
        else
          (⊤ : EReal)
    ProperConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) g ∧
      PositivelyHomogeneous g ∧
      g = positivelyHomogeneousConvexFunctionGenerated (n := n + 1) h := by
  classical
  let g : (Fin (n + 1) → Real) → EReal :=
    fun y =>
      if 0 ≤ y 0 then
        rightScalarMultiple f (y 0) (fun i => y i.succ)
      else
        (⊤ : EReal)
  let h : (Fin (n + 1) → Real) → EReal :=
    fun y =>
      if y 0 = (1 : Real) then
        f (fun i => y i.succ)
      else
        (⊤ : EReal)
  have hconv_h :
      ConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) h :=
    convexFunctionOn_perspective_h (f := f) hf.1
  have hne_epi_h :
      Set.Nonempty (epigraph (Set.univ : Set (Fin (n + 1) → Real)) h) :=
    nonempty_epigraph_perspective_h (f := f) hf
  have hfinite : ∃ y, h y ≠ (⊤ : EReal) := by
    rcases hne_epi_h with ⟨p, hp⟩
    refine ⟨p.1, ?_⟩
    have hp' : h p.1 ≤ (p.2 : EReal) := by
      exact (mem_epigraph_univ_iff (f := h)).1 hp
    intro htop
    have hp'' := hp'
    rw [htop] at hp''
    exact (not_top_le_coe p.2) hp''
  have hrep :=
    infimumRepresentation_posHomogeneousHull (n := n + 1) (h := h) hconv_h hfinite
  let ph := positivelyHomogeneousConvexFunctionGenerated (n := n + 1) h
  have hrep0 :
      ∀ y : Fin (n + 1) → Real,
        ph y =
          sInf { z : EReal | ∃ lam : Real, 0 ≤ lam ∧ z = rightScalarMultiple h lam y } := by
    simpa [ph] using hrep.1
  have hrep_pos :
      ∀ y : Fin (n + 1) → Real, y ≠ 0 →
        ph y =
          sInf { z : EReal | ∃ lam : Real, 0 < lam ∧ z = rightScalarMultiple h lam y } := by
    intro y hy
    have h' := hrep.2 y (Or.inl hy)
    simpa [ph] using h'
  have hgh : g = ph := by
    funext y
    by_cases hy : y = 0
    · subst hy
      have hne_epi_f :
          Set.Nonempty (epigraph (Set.univ : Set (Fin n → Real)) f) := hf.2.1
      have hval_f0 := rightScalarMultiple_zero_eval (f := f) hne_epi_f (0)
      have hg0 : g 0 = (0 : EReal) := by
        calc
          g 0 = rightScalarMultiple f 0 (fun i : Fin n => 0) := by
                simp [g]
          _ = rightScalarMultiple f 0 (0 : Fin n → Real) := by
                rfl
          _ = (0 : EReal) := by
                simpa using hval_f0
      have hval_h0 := rightScalarMultiple_zero_eval (f := h) hne_epi_h (0)
      set S0 : Set EReal :=
        { z : EReal | ∃ lam : Real, 0 ≤ lam ∧ z = rightScalarMultiple h lam (0) }
      have hmem0 : (0 : EReal) ∈ S0 := by
        refine ⟨0, le_rfl, ?_⟩
        simp [hval_h0]
      have hle : sInf S0 ≤ (0 : EReal) := sInf_le hmem0
      have hge : (0 : EReal) ≤ sInf S0 := by
        refine le_sInf ?_
        intro z hz
        rcases hz with ⟨lam, hlam, rfl⟩
        by_cases h0 : lam = 0
        · subst h0
          simp [hval_h0]
        · have hlam' : 0 < lam := lt_of_le_of_ne hlam (Ne.symm h0)
          have hform :=
            rightScalarMultiple_perspective_h_pos (f := f) hf.1 hlam' (0)
          have hne : (0 : Real) ≠ lam := by linarith
          have htop' : rightScalarMultiple h lam 0 = (⊤ : EReal) := by
            simpa [hne] using hform
          simp [htop']
      have hSinf : sInf S0 = (0 : EReal) := le_antisymm hle hge
      have hph0 : ph 0 = (0 : EReal) := by
        have hrep0' := hrep0 (0)
        simp [S0, hSinf] at hrep0'
        exact hrep0'
      simp [hg0, hph0]
    · have hph := hrep_pos y hy
      set Spos : Set EReal :=
        { z : EReal | ∃ lam : Real, 0 < lam ∧ z = rightScalarMultiple h lam y }
      have hph' : ph y = sInf Spos := by
        simpa [Spos] using hph
      have hy0 := lt_trichotomy (y 0) 0
      rcases hy0 with hyneg | hyzero | hypos
      · have htop : sInf Spos = (⊤ : EReal) := by
          refine le_antisymm le_top ?_
          refine le_sInf ?_
          intro z hz
          rcases hz with ⟨lam, hlam, rfl⟩
          have hform :=
            rightScalarMultiple_perspective_h_pos (f := f) hf.1 hlam y
          have hne : y 0 ≠ lam := by linarith
          have htop' : rightScalarMultiple h lam y = (⊤ : EReal) := by
            simpa [hne] using hform
          simp [htop']
        have hg : g y = (⊤ : EReal) := by
          have : ¬ 0 ≤ y 0 := by exact not_le.mpr hyneg
          simp [g, this]
        simp [hph', Spos, htop, hg]
      · have htop : sInf Spos = (⊤ : EReal) := by
          refine le_antisymm le_top ?_
          refine le_sInf ?_
          intro z hz
          rcases hz with ⟨lam, hlam, rfl⟩
          have hform :=
            rightScalarMultiple_perspective_h_pos (f := f) hf.1 hlam y
          have hne : y 0 ≠ lam := by linarith
          have htop' : rightScalarMultiple h lam y = (⊤ : EReal) := by
            simpa [hne] using hform
          simp [htop']
        have hne_epi_f :
            Set.Nonempty (epigraph (Set.univ : Set (Fin n → Real)) f) := hf.2.1
        have hval_f0 :=
          rightScalarMultiple_zero_eval (f := f) hne_epi_f (fun i : Fin n => y i.succ)
        have hg : g y = (⊤ : EReal) := by
          have : (fun i : Fin n => y i.succ) ≠ 0 := by
            intro hzero
            apply hy
            funext i
            cases i using Fin.cases with
            | zero =>
                simp [hyzero]
            | succ j =>
                have hj := congrArg (fun f => f j) hzero
                simp at hj
                exact hj
          simp [g, hyzero, hval_f0, this]
        simp [hph', Spos, htop, hg]
      · have hle : sInf Spos ≤ rightScalarMultiple h (y 0) y := by
          exact sInf_le ⟨y 0, hypos, rfl⟩
        have hge : rightScalarMultiple h (y 0) y ≤ sInf Spos := by
          refine le_sInf ?_
          intro z hz
          rcases hz with ⟨lam, hlam, rfl⟩
          by_cases hylam : y 0 = lam
          · subst hylam
            exact le_rfl
          · have hform :=
              rightScalarMultiple_perspective_h_pos (f := f) hf.1 hlam y
            have htop' : rightScalarMultiple h lam y = (⊤ : EReal) := by
              simpa [hylam] using hform
            simp [htop']
        have hSinf : sInf Spos = rightScalarMultiple h (y 0) y := by
          exact le_antisymm hle hge
        have hform1 :
            rightScalarMultiple h (y 0) y =
              ((y 0 : Real) : EReal) * f ((y 0)⁻¹ • fun i => y i.succ) := by
          have hform1' := rightScalarMultiple_perspective_h_pos (f := f) hf.1 hypos y
          simp at hform1'
          exact hform1'
        have hright :
            rightScalarMultiple f (y 0) (fun i => y i.succ) =
              ((y 0 : Real) : EReal) * f ((y 0)⁻¹ • fun i => y i.succ) :=
          rightScalarMultiple_pos (f := f) (lam := y 0) hf.1 hypos (fun i => y i.succ)
        have hg : g y = rightScalarMultiple h (y 0) y := by
          have : 0 ≤ y 0 := le_of_lt hypos
          calc
            g y = rightScalarMultiple f (y 0) (fun i => y i.succ) := by
              simp [g, this]
            _ = ((y 0 : Real) : EReal) * f ((y 0)⁻¹ • fun i => y i.succ) := hright
            _ = rightScalarMultiple h (y 0) y := by
              simp [hform1]
        calc
          g y = rightScalarMultiple h (y 0) y := hg
          _ = sInf Spos := by simp [hSinf]
          _ = ph y := by simp [hph']
  have hmax := maximality_posHomogeneousHull (n := n + 1) (h := h) hconv_h
  have hconv_ph :
      ConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) ph :=
    (hmax.2.1).1
  have hpos_ph : PositivelyHomogeneous ph := (hmax.2.1).2.1
  have hconv_g :
      ConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) g := by
    simpa [hgh] using hconv_ph
  have hpos_g : PositivelyHomogeneous g := by
    simpa [hgh] using hpos_ph
  have hne_epi_f :
      Set.Nonempty (epigraph (Set.univ : Set (Fin n → Real)) f) := hf.2.1
  have hval_f0 := rightScalarMultiple_zero_eval (f := f) hne_epi_f (0)
  have hg0 : g 0 = (0 : EReal) := by
    calc
      g 0 = rightScalarMultiple f 0 (fun i : Fin n => 0) := by
            simp [g]
      _ = rightScalarMultiple f 0 (0 : Fin n → Real) := by
            rfl
      _ = (0 : EReal) := by
            simpa using hval_f0
  have hne_epi_g :
      Set.Nonempty (epigraph (Set.univ : Set (Fin (n + 1) → Real)) g) := by
    refine ⟨(0, 0), ?_⟩
    exact (mem_epigraph_univ_iff (f := g)).2 (by simp [hg0])
  have hnotbot :
      ∀ y ∈ (Set.univ : Set (Fin (n + 1) → Real)), g y ≠ (⊥ : EReal) := by
    intro y hyS
    by_cases hy0 : 0 ≤ y 0
    · have hg : g y = rightScalarMultiple f (y 0) (fun i => y i.succ) := by
        simp [g, hy0]
      by_cases hpos : 0 < y 0
      · have hright :=
          rightScalarMultiple_pos (f := f) (lam := y 0) hf.1 hpos (fun i => y i.succ)
        have hne :
            f ((y 0)⁻¹ • fun i => y i.succ) ≠ (⊥ : EReal) := by
          exact hf.2.2 _ (by simp)
        have hmul_ne :
            ((y 0 : Real) : EReal) *
              f ((y 0)⁻¹ • fun i => y i.succ) ≠ (⊥ : EReal) :=
          ereal_mul_ne_bot_of_pos' (t := y 0) hpos hne
        have hgy :
            g y =
              ((y 0 : Real) : EReal) * f ((y 0)⁻¹ • fun i => y i.succ) := by
          simpa [hg] using hright
        simpa [hgy] using hmul_ne
      · have hy0' : y 0 = 0 := by linarith
        have hval :=
          rightScalarMultiple_zero_eval (f := f) hne_epi_f (fun i : Fin n => y i.succ)
        have hgy :
            g y = if (fun i : Fin n => y i.succ) = 0 then (0 : EReal) else (⊤ : EReal) := by
          simp [g, hy0', hval]
        by_cases hsucc : (fun i : Fin n => y i.succ) = 0
        · simp [hgy, hsucc]
        · simp [hgy, hsucc]
    · have hgy : g y = (⊤ : EReal) := by
        simp [g, hy0]
      simp [hgy]
  have hproper_g :
      ProperConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) g :=
    ⟨hconv_g, hne_epi_g, hnotbot⟩
  simpa [g, h] using (And.intro hproper_g (And.intro hpos_g hgh))

Text 5.4.9.1: For each fixed Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `dom`dom f, the map is a proper convex function of on .

theorem properConvexFunctionOn_perspective_param {n : Nat} {f : (Fin n → Real) → EReal}
    (hf : ProperConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) f) :
    ∀ x : Fin n → Real, x ∈ effectiveDomain Set.univ f →
      ProperConvexFunctionOn (S := {t : Fin 1 → Real | 0 ≤ t 0})
        (fun t => rightScalarMultiple f (t 0) x) := by
  classical
  intro x hx
  let g : (Fin (n + 1) → Real) → EReal :=
    fun y =>
      if 0 ≤ y 0 then
        rightScalarMultiple f (y 0) (fun i => y i.succ)
      else
        (⊤ : EReal)
  let lift : (Fin 1 → Real) → (Fin (n + 1) → Real) :=
    fun t => Fin.cases (t 0) x
  have hpers := perspective_posHomogeneous_convex (n := n) (f := f) hf
  have hpers' :
      ProperConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) g ∧
        PositivelyHomogeneous g ∧
        g =
          positivelyHomogeneousConvexFunctionGenerated (n := n + 1)
            (fun y =>
              if y 0 = (1 : Real) then f (fun i => y i.succ) else (⊤ : EReal)) := by
    simpa [g] using hpers
  have hproper_g :
      ProperConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) g :=
    hpers'.1
  have hconv_g :
      ConvexFunctionOn (S := (Set.univ : Set (Fin (n + 1) → Real))) g :=
    hproper_g.1
  have hnotbot_g :
      ∀ y ∈ (Set.univ : Set (Fin (n + 1) → Real)), g y ≠ (⊥ : EReal) :=
    hproper_g.2.2
  have hseg_g :=
    (convexFunctionOn_iff_segment_inequality (C := (Set.univ : Set (Fin (n + 1) → Real)))
        (f := g) (hC := convex_univ) (hnotbot := hnotbot_g)).1 hconv_g
  have hC :
      Convex ℝ ({t : Fin 1 → Real | 0 ≤ t 0} : Set (Fin 1 → Real)) := by
    intro t1 ht1 t2 ht2 a b ha hb hab
    have ha' : 0 ≤ a := ha
    have hb' : 0 ≤ b := hb
    have ht1' : 0 ≤ t1 0 := by
      simpa using ht1
    have ht2' : 0 ≤ t2 0 := by
      simpa using ht2
    have hcomb0 :
        0 ≤ ((a • t1 + b • t2) 0) := by
      have hcomb0' : 0 ≤ a * t1 0 + b * t2 0 := by
        nlinarith [ht1', ht2', ha', hb']
      simpa [Pi.smul_apply, smul_eq_mul] using hcomb0'
    simpa using hcomb0
  have hnotbot_phi :
      ∀ t ∈ ({t : Fin 1 → Real | 0 ≤ t 0} : Set (Fin 1 → Real)),
        rightScalarMultiple f (t 0) x ≠ (⊥ : EReal) := by
    intro t ht
    by_cases hpos : 0 < t 0
    · have hright :=
        rightScalarMultiple_pos (f := f) (lam := t 0) hf.1 hpos x
      have hne : f ((t 0)⁻¹ • x) ≠ (⊥ : EReal) := by
        exact hf.2.2 _ (by simp)
      have hmul_ne :
          ((t 0 : Real) : EReal) * f ((t 0)⁻¹ • x) ≠ (⊥ : EReal) :=
        ereal_mul_ne_bot_of_pos' (t := t 0) hpos hne
      have hgy : rightScalarMultiple f (t 0) x =
          ((t 0 : Real) : EReal) * f ((t 0)⁻¹ • x) := by
        simpa using hright
      simpa [hgy] using hmul_ne
    · have ht0' : 0 ≤ t 0 := by
        simpa using ht
      have ht0 : t 0 = 0 := by linarith
      have hne_epi_f :
          Set.Nonempty (epigraph (Set.univ : Set (Fin n → Real)) f) := hf.2.1
      have hval := rightScalarMultiple_zero_eval (f := f) hne_epi_f x
      have hgy :
          rightScalarMultiple f (t 0) x =
            if x = 0 then (0 : EReal) else (⊤ : EReal) := by
          simp [ht0, hval]
      by_cases hx0 : x = 0
      · subst hx0
        have hgy0 := hgy
        simp at hgy0
        simp [hgy0]
      · have hgy0 := hgy
        simp [hx0] at hgy0
        simp [hgy0]
  have hphi_conv :
      ConvexFunctionOn (S := {t : Fin 1 → Real | 0 ≤ t 0})
        (fun t => rightScalarMultiple f (t 0) x) := by
    refine
      (convexFunctionOn_iff_segment_inequality (C := {t : Fin 1 → Real | 0 ≤ t 0})
          (f := fun t => rightScalarMultiple f (t 0) x)
          (hC := hC) (hnotbot := hnotbot_phi)).2 ?_
    intro t1 ht1 t2 ht2 θ hθ0 hθ1
    have ht1' : 0 ≤ t1 0 := by
      simpa using ht1
    have ht2' : 0 ≤ t2 0 := by
      simpa using ht2
    have hcomb0' : 0 ≤ ((1 - θ) • t1 + θ • t2) 0 := by
      have hθ0' : 0 ≤ θ := le_of_lt hθ0
      have hθ1' : 0 ≤ 1 - θ := by linarith
      have hcomb0'' : 0 ≤ (1 - θ) * t1 0 + θ * t2 0 := by
        nlinarith [ht1', ht2', hθ0', hθ1']
      simpa [Pi.smul_apply, smul_eq_mul] using hcomb0''
    have hlift :
        (1 - θ) • lift t1 + θ • lift t2 =
          lift ((1 - θ) • t1 + θ • t2) := by
      funext i
      cases i using Fin.cases with
      | zero =>
          simp [lift, Pi.smul_apply, smul_eq_mul]
      | succ j =>
          simp [lift, Pi.smul_apply, smul_eq_mul]
          ring
    have hg1 : g (lift t1) = rightScalarMultiple f (t1 0) x := by
      simp [g, lift, ht1']
    have hg2 : g (lift t2) = rightScalarMultiple f (t2 0) x := by
      simp [g, lift, ht2']
    have hg3 :
        g (lift ((1 - θ) • t1 + θ • t2)) =
          rightScalarMultiple f (((1 - θ) • t1 + θ • t2) 0) x := by
      have hcomb0'' : 0 ≤ (1 - θ) * t1 0 + θ * t2 0 := by
        simpa [Pi.smul_apply, smul_eq_mul] using hcomb0'
      simp [g, lift, hcomb0'', Pi.smul_apply, smul_eq_mul]
    have hineq :=
      hseg_g (lift t1) (by simp) (lift t2) (by simp) θ hθ0 hθ1
    have hineq' :
        g (lift ((1 - θ) • t1 + θ • t2)) ≤
          ((1 - θ : Real) : EReal) * g (lift t1) +
            ((θ : Real) : EReal) * g (lift t2) := by
      simpa [hlift] using hineq
    simpa [hg1, hg2, hg3] using hineq'
  have hne_epi :
      Set.Nonempty (epigraph (S := {t : Fin 1 → Real | 0 ≤ t 0})
        (fun t => rightScalarMultiple f (t 0) x)) := by
    rcases hx with ⟨μ, hμ⟩
    have hμ' : f x ≤ (μ : EReal) := by
      exact (mem_epigraph_univ_iff (f := f)).1 hμ
    have hpos : 0 < (1 : Real) := by norm_num
    have hright :=
      rightScalarMultiple_pos (f := f) (lam := 1) hf.1 hpos x
    have hval : rightScalarMultiple f 1 x = f x := by
      simpa using hright
    refine ⟨(fun _ => (1 : Real), μ), ?_⟩
    have : rightScalarMultiple f (1 : Real) x ≤ (μ : EReal) := by
      simpa [hval] using hμ'
    have hmem : (fun _ => (1 : Real)) ∈ ({t : Fin 1 → Real | 0 ≤ t 0} : Set (Fin 1 → Real)) := by
      simp
    have hpair :
        (fun _ => (1 : Real)) ∈ ({t : Fin 1 → Real | 0 ≤ t 0} : Set (Fin 1 → Real)) ∧
          rightScalarMultiple f (1 : Real) x ≤ (μ : EReal) := by
      exact ⟨hmem, this⟩
    exact hpair
  have hnotbot :
      ∀ t ∈ ({t : Fin 1 → Real | 0 ≤ t 0} : Set (Fin 1 → Real)),
        rightScalarMultiple f (t 0) x ≠ (⊥ : EReal) :=
    hnotbot_phi
  exact ⟨hphi_conv, hne_epi, hnotbot⟩

Text 5.4.10 (Gauge of a convex set): Let failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `C`C ⊆ ℝ^Unknown identifier `n`n be a nonempty convex set. The gauge of Unknown identifier `C`C is the function defined by .

noncomputable def gaugeOfConvexSet {n : Nat} (C : Set (Fin n → Real)) :
    (Fin n → Real) → ℝ :=
  fun x => sInf { r : ℝ | 0 ≤ r ∧ x ∈ (fun y => r • y) '' C }

Text 5.4.10: The gauge of a convex set agrees with mathlib's gauge.{u_2} {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : Set E) (x : E) : ℝgauge.

theorem gaugeOfConvexSet_eq_gauge {n : Nat} (C : Set (Fin n → Real)) :
    gaugeOfConvexSet C = gauge C := by
  funext x
  classical
  by_cases hx : x = 0
  · subst hx
    by_cases hCne : C.Nonempty
    · set A : Set ℝ := { r : ℝ | 0 ≤ r ∧ (0 : Fin n → Real) ∈ r • C }
      have h0mem : (0 : ℝ) ∈ A := by
        refine ⟨le_rfl, ?_⟩
        rcases hCne with ⟨y, hy⟩
        exact ⟨y, hy, by simp⟩
      have hAne : A.Nonempty := ⟨0, h0mem⟩
      have hAbdd : BddBelow A := by
        refine ⟨0, ?_⟩
        intro r hr
        exact hr.1
      have hle : sInf A ≤ (0 : ℝ) := csInf_le hAbdd h0mem
      have hge : (0 : ℝ) ≤ sInf A := le_csInf hAne (by intro r hr; exact hr.1)
      have h0 : sInf A = (0 : ℝ) := le_antisymm hle hge
      have h0' : gaugeOfConvexSet C 0 = (0 : ℝ) := by
        simp [gaugeOfConvexSet, A, h0]
      simp [h0']
    · have hempty :
          { r : ℝ | 0 ≤ r ∧ (0 : Fin n → Real) ∈ r • C } = (∅ : Set ℝ) := by
        ext r
        constructor
        · intro hr
          rcases (Set.mem_smul_set.mp hr.2) with ⟨y, hy, _⟩
          exact (hCne ⟨y, hy⟩).elim
        · intro hr
          exact (Set.notMem_empty _ hr).elim
      have h0' : gaugeOfConvexSet C 0 = (0 : ℝ) := by
        simp [gaugeOfConvexSet, hempty]
      simp [h0']
  · have hset :
        { r : ℝ | 0 ≤ r ∧ x ∈ r • C } = { r : ℝ | 0 < r ∧ x ∈ r • C } := by
      ext r
      constructor
      · intro hr
        have hr0 : r ≠ 0 := by
          intro hr0
          subst hr0
          rcases (Set.mem_smul_set.mp hr.2) with ⟨y, hy, hxy⟩
          have : x = 0 := by simpa using hxy.symm
          exact (hx this).elim
        exact ⟨lt_of_le_of_ne hr.1 hr0.symm, hr.2⟩
      · intro hr
        exact ⟨le_of_lt hr.1, hr.2⟩
    simp [gaugeOfConvexSet, gauge, hset]

A finite constant function is proper convex on Set.univ.{u} {α : Type u} : Set αSet.univ.

lemma properConvexFunctionOn_const {n : Nat} (c : Real) :
    ProperConvexFunctionOn (Set.univ : Set (Fin n → Real)) (fun _ => (c : EReal)) := by
  have hconv_real :
      ConvexOn ℝ (Set.univ : Set (Fin n → Real)) (fun _ => c) :=
    convexOn_const (c := c) (hs := convex_univ)
  have hconv :
      ConvexFunctionOn (Set.univ : Set (Fin n → Real)) (fun _ => (c : EReal)) :=
    convexFunctionOn_of_convexOn_real (S := Set.univ) hconv_real
  have hne_epi :
      Set.Nonempty (epigraph (Set.univ : Set (Fin n → Real)) (fun _ => (c : EReal))) := by
    refine ⟨(0, c), ?_⟩
    refine ⟨?_, ?_⟩
    · change (0 : Fin n → Real) ∈ (Set.univ : Set (Fin n → Real))
      simp
    · simp
  have hnotbot :
      ∀ x ∈ (Set.univ : Set (Fin n → Real)), (c : EReal) ≠ (⊥ : EReal) := by
    intro x hx
    exact EReal.coe_ne_bot c
  exact ⟨hconv, hne_epi, hnotbot⟩

The indicator function plus a real constant is convex on Set.univ.{u} {α : Type u} : Set αSet.univ.

lemma convexFunctionOn_indicator_add_const {n : Nat} {C : Set (Fin n → Real)}
    (hCne : C.Nonempty) (hCconv : Convex ℝ C) (c : Real) :
    ConvexFunctionOn (Set.univ : Set (Fin n → Real))
      (fun x => indicatorFunction C x + (c : EReal)) := by
  have hproper_indicator :
      ProperConvexFunctionOn (Set.univ : Set (Fin n → Real)) (indicatorFunction C) :=
    properConvexFunctionOn_indicator_of_convex_of_nonempty (C := C) hCconv hCne
  have hproper_const :
      ProperConvexFunctionOn (Set.univ : Set (Fin n → Real)) (fun _ => (c : EReal)) :=
    properConvexFunctionOn_const (n := n) c
  simpa using
    (convexFunctionOn_add_of_proper
      (f1 := indicatorFunction C) (f2 := fun _ => (c : EReal))
      hproper_indicator hproper_const)

The indicator of a scaled image is rewritten by inverse scaling when Unknown identifier `lam`sorry ≠ 0 : Proplam ≠ 0.

lemma indicatorFunction_image_smul_eq {n : Nat} {C : Set (Fin n → Real)}
    {lam : Real} (hlam : lam ≠ 0) (x : Fin n → Real) :
    indicatorFunction ((fun y => lam • y) '' C) x =
      indicatorFunction C (lam⁻¹ • x) := by
  classical
  by_cases hxC : lam⁻¹ • x ∈ C
  · have hx : x ∈ (fun y => lam • y) '' C := by
      refine ⟨lam⁻¹ • x, hxC, ?_⟩
      simp [smul_smul, hlam]
    have hx' : x ∈ lam • C := by
      simpa using hx
    simp [indicatorFunction, hxC, hx']
  · have hx : x ∉ (fun y => lam • y) '' C := by
      intro hx
      rcases hx with ⟨y, hyC, rfl⟩
      exact hxC (by
        simpa [smul_inv_smul_simplify (lam := lam) (x := y) hlam] using hyC)
    have hx' : x ∉ lam • C := by
      simpa using hx
    simp [indicatorFunction, hxC, hx']

For positive Unknown identifier `lam`lam, the right scalar multiple of indicatorFunction sorry + 1 : (Fin ?m.1 → ℝ) → ERealindicatorFunction Unknown identifier `C`C + 1 is explicit.

lemma rightScalarMultiple_indicator_add_one_pos {n : Nat} {C : Set (Fin n → Real)}
    (hCne : C.Nonempty) (hCconv : Convex ℝ C) {lam : Real} (hlam : 0 < lam)
    (x : Fin n → Real) :
    rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) lam x =
      indicatorFunction ((fun y => lam • y) '' C) x + ((lam : Real) : EReal) := by
  classical
  have hconv :
      ConvexFunctionOn (Set.univ : Set (Fin n → Real))
        (fun y => indicatorFunction C y + (1 : EReal)) :=
    convexFunctionOn_indicator_add_const (C := C) hCne hCconv 1
  have hmul :=
    rightScalarMultiple_pos (f := fun y => indicatorFunction C y + (1 : EReal))
      (lam := lam) hconv hlam x
  have hrewrite :
      indicatorFunction (lam • C) x = indicatorFunction C (lam⁻¹ • x) := by
    simpa using
      (indicatorFunction_image_smul_eq (C := C) (lam := lam) (x := x) (ne_of_gt hlam))
  by_cases hx : lam⁻¹ • x ∈ C
  · have hval : indicatorFunction C (lam⁻¹ • x) = (0 : EReal) := by
      simp [indicatorFunction, hx]
    calc
      rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) lam x =
          ((lam : Real) : EReal) * (indicatorFunction C (lam⁻¹ • x) + (1 : EReal)) := by
            simpa using hmul
      _ = (lam : EReal) := by simp [hval]
      _ = indicatorFunction C (lam⁻¹ • x) + (lam : EReal) := by simp [hval]
      _ = indicatorFunction (lam • C) x + (lam : EReal) := by
            simp [hrewrite]
      _ = indicatorFunction ((fun y => lam • y) '' C) x + (lam : EReal) := by
            rfl
  · have hval : indicatorFunction C (lam⁻¹ • x) = (⊤ : EReal) := by
      simp [indicatorFunction, hx]
    calc
      rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) lam x =
          ((lam : Real) : EReal) * (indicatorFunction C (lam⁻¹ • x) + (1 : EReal)) := by
            simpa using hmul
      _ = (⊤ : EReal) := by
            calc
              ((lam : Real) : EReal) * (indicatorFunction C (lam⁻¹ • x) + (1 : EReal)) =
              ((lam : Real) : EReal) * ((⊤ : EReal) + (1 : EReal)) := by
                    simp [hval]
              _ = ((lam : Real) : EReal) * (⊤ : EReal) := by
                    have htop : (⊤ : EReal) + (1 : EReal) = (⊤ : EReal) := by
                      simpa using (EReal.top_add_coe (1 : ℝ))
                    simp [htop]
              _ = (⊤ : EReal) := by
                    simpa using (EReal.coe_mul_top_of_pos hlam)
      _ = indicatorFunction C (lam⁻¹ • x) + (lam : EReal) := by
            simp [hval]
      _ = indicatorFunction (lam • C) x + (lam : EReal) := by
            simp [hrewrite]
      _ = indicatorFunction ((fun y => lam • y) '' C) x + (lam : EReal) := by
            rfl

For Unknown identifier `lam`sorry = 0 : Proplam = 0, the right scalar multiple of indicatorFunction sorry + 1 : (Fin ?m.1 → ℝ) → ERealindicatorFunction Unknown identifier `C`C + 1 is an indicator.

lemma rightScalarMultiple_indicator_add_one_zero {n : Nat} {C : Set (Fin n → Real)}
    (hCne : C.Nonempty) (hCconv : Convex ℝ C) (x : Fin n → Real) :
    rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) 0 x =
      indicatorFunction ((fun y => (0 : Real) • y) '' C) x + (0 : EReal) := by
  classical
  have hconv :
      ConvexFunctionOn (Set.univ : Set (Fin n → Real))
        (fun y => indicatorFunction C y + (1 : EReal)) :=
    convexFunctionOn_indicator_add_const (C := C) hCne hCconv 1
  have hfinite :
      ∃ y, (fun y => indicatorFunction C y + (1 : EReal)) y ≠ (⊤ : EReal) := by
    rcases hCne with ⟨y, hyC⟩
    refine ⟨y, ?_⟩
    simpa [indicatorFunction, hyC] using (EReal.coe_ne_top (1 : Real))
  have hzero_fun :
      rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) 0 =
        indicatorFunction ({0} : Set (Fin n → Real)) :=
    rightScalarMultiple_zero_eq_indicator
      (f := fun y => indicatorFunction C y + (1 : EReal)) hconv hfinite
  have hzero :
      rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) 0 x =
        indicatorFunction ({0} : Set (Fin n → Real)) x := by
    simpa using congrArg (fun f => f x) hzero_fun
  have himage :
      (fun y => (0 : Real) • y) '' C = ({0} : Set (Fin n → Real)) := by
    have hconst :
        (fun y => (0 : Real) • y) =
          (fun _ : Fin n → Real => (0 : Fin n → Real)) := by
      funext y
      simp
    simpa [hconst] using
      (Set.Nonempty.image_const (s := C) hCne (a := (0 : Fin n → Real)))
  calc
    rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) 0 x =
        indicatorFunction ({0} : Set (Fin n → Real)) x := hzero
    _ = indicatorFunction ((fun y => (0 : Real) • y) '' C) x := by
        rw [himage]
    _ = indicatorFunction ((fun y => (0 : Real) • y) '' C) x + (0 : EReal) := by
        simp

Nonnegative scalars give the explicit indicator formula.

lemma rightScalarMultiple_indicator_add_one_nonneg {n : Nat} {C : Set (Fin n → Real)}
    (hCne : C.Nonempty) (hCconv : Convex ℝ C) {lam : Real} (hlam : 0 ≤ lam)
    (x : Fin n → Real) :
    rightScalarMultiple (fun y => indicatorFunction C y + (1 : EReal)) lam x =
      indicatorFunction ((fun y => lam • y) '' C) x + ((lam : Real) : EReal) := by
  by_cases h0 : lam = 0
  · subst h0
    simpa using rightScalarMultiple_indicator_add_one_zero (C := C) hCne hCconv x
  · have hpos : 0 < lam := lt_of_le_of_ne hlam (Ne.symm h0)
    simpa using
      (rightScalarMultiple_indicator_add_one_pos (C := C) hCne hCconv
        (lam := lam) hpos x)

end Section05end Chap01