theorem polarGauge_le_supportFunction_unitSublevel_of_isGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (xStar : Fin n → ℝ) : polarGauge k xStar ≤ supportFunctionEReal {x : Fin n → ℝ | k x ≤ 1} xStar

The polar gauge is bounded above by the support function of the unit sublevel.

theorem supportFunction_unitSublevel_eq_polarGauge_of_isGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (xStar : Fin n → ℝ) : supportFunctionEReal {x : Fin n → ℝ | k x ≤ 1} xStar = polarGauge k xStar

The support function of a gauge's unit sublevel equals the polar gauge.

noncomputable def monotoneConjugateERealNonneg (g : EReal → EReal) (s : EReal) : EReal

The monotone conjugate g⁺ of a function g : [0, +∞] → (-∞, +∞], defined by g⁺(s) = sup_{t ≥ 0} (t * s - g t).

Equations

• monotoneConjugateERealNonneg g s = sSup ((fun (t : EReal) => t * s - g t) '' {t : EReal | 0 ≤ t})

theorem monotoneConjugateERealNonneg_mono {g : EReal → EReal} : Monotone (monotoneConjugateERealNonneg g)

The monotone conjugate is monotone in its argument.

theorem term_le_monotoneConjugateERealNonneg {g : EReal → EReal} {s t : EReal} (ht : 0 ≤ t) : t * s - g t ≤ monotoneConjugateERealNonneg g s

Each affine term lies below the monotone conjugate.

theorem monotoneConjugateERealNonneg_top_of_exists_finite {g : EReal → EReal} (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) : monotoneConjugateERealNonneg g ⊤ = ⊤

The monotone conjugate takes value ⊤ at ⊤ once g is finite at some positive point.

theorem bddAbove_cutoff_real_of_monotoneConjugateERealNonneg_of_exists_finite {g : EReal → EReal} (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) {αr : ℝ} : BddAbove {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr}

Real cutoffs for the monotone conjugate are bounded above once g is finite at some positive point.

theorem csSup_cutoff_mem_sublevel_monotoneConjugateERealNonneg {g : EReal → EReal} (hg_top : g ⊤ = ⊤) {αr : ℝ} (hA_bdd : BddAbove {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr}) (hA_nonempty : {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr}.Nonempty) : 0 ≤ sSup {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr} ∧ monotoneConjugateERealNonneg g ↑(sSup {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr}) ≤ ↑αr

The cutoff for a monotone conjugate lies in its real sublevel.

theorem sublevel_monotoneConjugate_comp_polarGauge_eq_sublevel_polarGauge_csSup {n : ℕ} {k : (Fin n → ℝ) → EReal} {g : EReal → EReal} (hg_top : g ⊤ = ⊤) (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) {αr : ℝ} (hA_bdd : BddAbove {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr}) (hA_nonempty : {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr}.Nonempty) : {xStar : Fin n → ℝ | monotoneConjugateERealNonneg g (polarGauge k xStar) ≤ ↑αr} = {xStar : Fin n → ℝ | polarGauge k xStar ≤ ↑(sSup {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr})}

Sublevels of g⁺ ∘ kᵒ are kᵒ-sublevels at the real cutoff.

theorem monotoneConjugateERealNonneg_le_affine {g : EReal → EReal} (hg_top : g ⊤ = ⊤) (h0_ne_top : monotoneConjugateERealNonneg g 0 ≠ ⊤) {s0 lam : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam ≤ 1) : monotoneConjugateERealNonneg g ↑(lam * s0) ≤ ↑(1 - lam) * monotoneConjugateERealNonneg g 0 + ↑lam * monotoneConjugateERealNonneg g ↑s0

A convex interpolation bound for the monotone conjugate on the nonnegative ray.

theorem cutoff_pos_or_all_zero_of_monotoneConjugateERealNonneg {g : EReal → EReal} (hg_top : g ⊤ = ⊤) (h0_ne_bot : monotoneConjugateERealNonneg g 0 ≠ ⊥) {αr βr : ℝ} (hα0 : monotoneConjugateERealNonneg g 0 < ↑αr) (hβ0 : monotoneConjugateERealNonneg g 0 < ↑βr) (hAα_bdd : BddAbove {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr}) (hAβ_bdd : BddAbove {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑βr}) : sSup {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr} = 0 ∧ sSup {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑βr} = 0 ∨ 0 < sSup {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑αr} ∧ 0 < sSup {s : ℝ | 0 ≤ s ∧ monotoneConjugateERealNonneg g ↑s ≤ ↑βr}

Cutoffs for the monotone conjugate are either both zero or both positive.

def profileSet {n : ℕ} (f k : (Fin n → ℝ) → EReal) (z : EReal) : Set EReal

Admissible levels covering a k-sublevel by a sublevel of f.

Equations

• profileSet f k z = {α : EReal | f 0 < α ∧ α < ⊤ ∧ {x : Fin n → ℝ | k x ≤ z} ⊆ {x : Fin n → ℝ | f x ≤ α}}

theorem profileSet_mono {n : ℕ} {f k : (Fin n → ℝ) → EReal} {z₁ z₂ : EReal} (hz : z₁ ≤ z₂) : profileSet f k z₂ ⊆ profileSet f k z₁

The admissible sets are antitone in the threshold.

theorem profileFun_mono {n : ℕ} {f k : (Fin n → ℝ) → EReal} : Monotone fun (z : EReal) => sInf (profileSet f k z)

The profile infimum is monotone in the threshold.

theorem profileFun_with_top_mono {n : ℕ} {f k : (Fin n → ℝ) → EReal} : Monotone fun (z : EReal) => if z = ⊤ then ⊤ else sInf (profileSet f k z)

The profile infimum with a ⊤ guard is monotone.

theorem profileFun_with_top_top {n : ℕ} {f k : (Fin n → ℝ) → EReal} : (fun (z : EReal) => if z = ⊤ then ⊤ else sInf (profileSet f k z)) ⊤ = ⊤

The profile infimum with a ⊤ guard sends ⊤ to ⊤.

theorem g0_ne_bot_of_convex_closed_and_exists_finite_nonneg {g : EReal → EReal} (hg_conv : ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) (hg_closed : IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0))) (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) : g 0 ≠ ⊥

A convex function on t ≥ 0 with closed epigraph cannot take value ⊥ at 0 if it is finite somewhere on the positive ray.

theorem monotone_ne_bot_of_nonneg {g : EReal → EReal} (hg_mono : Monotone g) (h0 : g 0 ≠ ⊥) (t : EReal) : 0 ≤ t → g t ≠ ⊥

A monotone function is never ⊥ on nonnegative inputs once g 0 ≠ ⊥.

theorem sublevel_comp_subset_sublevel_gauge_sSup {n : ℕ} {k : (Fin n → ℝ) → EReal} {g : EReal → EReal} (hk : IsGauge k) {α : EReal} : {x : Fin n → ℝ | g (k x) ≤ α} ⊆ {x : Fin n → ℝ | k x ≤ sSup {t : EReal | 0 ≤ t ∧ g t ≤ α}}

Sublevels of g ∘ k are contained in the k-sublevel at the sSup cutoff.

theorem lscOn_g_nonneg_of_isClosed_epigraph {g : EReal → EReal} (hg_closed : IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0))) : LowerSemicontinuousOn (fun (t : Fin 1 → ℝ) => g ↑(t 0)) {t : Fin 1 → ℝ | 0 ≤ t 0}

Closed epigraph on the nonnegative ray gives lower semicontinuity on that ray.

theorem g_le_csSup_of_lscOn_nonneg {g : EReal → EReal} (hlsc : LowerSemicontinuousOn (fun (t : Fin 1 → ℝ) => g ↑(t 0)) {t : Fin 1 → ℝ | 0 ≤ t 0}) {α : ℝ} (h0α : g 0 ≤ ↑α) (hA_bdd : BddAbove {s : ℝ | 0 ≤ s ∧ g ↑s ≤ ↑α}) : g ↑(sSup {s : ℝ | 0 ≤ s ∧ g ↑s ≤ ↑α}) ≤ ↑α

Lower semicontinuity on t ≥ 0 makes the sSup cutoff attainable.