1D convex hull is an interval

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this?

import Mathlib
open ENNReal

theorem ENNReal.convexHull_eq_Icc (s : Set ℝ≥0∞) :
    convexHull ℝ≥0∞ s = Set.Icc (sInf s) (sSup s) := by

I can't work out the general statement, as I don't think we have a typeclass that allows mixing complete lattice operators with ordered rings; but presumably this also applies to Rat, Nat, Int, etc.

[Aaron Liu]

Maybe something like docs#convex_iff_ordConnected, but this assumes a LinearOrderedField

[Ben Eltschig]

Open intervals are also convex by the way, so what you get won't always be closed. You can also take the closure of the convex hull, but then you still have the problem that the interval could be infinite on one or both ends - so really, docs#Set.OrdConnected and docs#IsPreconnected are probably the best characterisations you can find. Unless of course you require s to be compact - in that case, the convex hull should indeed be a compact interval

[Ben Eltschig]

I just realised, if you're talking about ℝ≥0∞ of course infinite intervals aren't really a thing, and the closure of the convex hull will always be compact. So in that case you could actually prove that it is equal to Set.Icc (sInf s) (sSup s) - it'll be indeed hard to generalise though.

[Kevin Buzzard]

Are there any ordered rings which are complete lattices other than the zero ring?

[Yaël Dillies]

No indeed. Proof: Inf empty + 1 >= Inf empty = top so top + 1 = Inf empty + 1 = top and 1 = 0

[Yaël Dillies]

ENNReal-convex hull sounds a bit cursed in general. I would advise sticking to NNReal-convexity

[Eric Wieser]

I'm not bound to ENNReal here, it just saves me needing to assume that s is bounded. Real or NNReal would be fine too

[Yury G. Kudryashov]

Is it true that ENNReal-convex hull is always equal to the NNReal-convex hull?

[Aaron Liu]

Do you mean something like this?

import Mathlib

theorem ENNReal.coe_image_convexHull (s : Set NNReal) :
    ((↑) '' convexHull NNReal s : Set ENNReal) = convexHull ENNReal ((↑) '' s) := by
  ext x
  constructor
  · rintro ⟨x, hx, rfl⟩
    apply mem_convexHull_iff.mpr
    intro t hst ht
    apply mem_convexHull_iff.mp at hx
    apply hx ((↑) ⁻¹' t)
    · exact Set.image_subset_iff.mp hst
    · apply convex_iff_segment_subset.mpr
      apply convex_iff_segment_subset.mp at ht
      rintro a ha b hb m ⟨p, q, _, _, hpq, rfl⟩
      apply ht ha hb
      rw [← ENNReal.coe_inj, ENNReal.coe_add, ENNReal.coe_one] at hpq
      exact ⟨p, q, zero_le _, zero_le _, hpq, by simp⟩
  · intro h
    apply mem_convexHull_iff.mp at h
    apply h
    · apply (Set.image_subset_image_iff ENNReal.coe_injective).mpr
      exact subset_convexHull NNReal s
    · apply convex_iff_segment_subset.mpr
      rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ m ⟨p, q, _, _, hpq, rfl⟩
      lift p to NNReal using by rintro rfl; simp at hpq
      lift q to NNReal using by rintro rfl; simp at hpq
      rw [smul_eq_mul, smul_eq_mul, ← ENNReal.coe_mul, ← ENNReal.coe_mul, ← ENNReal.coe_add]
      apply Set.mem_image_of_mem
      rw [← ENNReal.coe_add, ← ENNReal.coe_one, ENNReal.coe_inj] at hpq
      rw [← (convexHull NNReal).idempotent]
      apply segment_subset_convexHull ha hb
      exact ⟨p, q, zero_le p, zero_le q, hpq, by simp⟩

[Kevin Buzzard]

rw [h] (or [← h]) (at h2) is more idiomatic than apply h.mp/mpr (at h2)

[Eric Wieser]

I think Yury might have been asking about swapping the scalar ring,

theorem ENNReal.convexHull_ennreal_eq (s : Set ℝ≥0∞) :
    convexHull ℝ≥0∞ s = convexHull ℝ≥0 s

[Eric Wieser]

Answer:

theorem ENNReal.starConvex_iff (x : ℝ≥0∞) (s : Set ℝ≥0∞) :
    StarConvex ℝ≥0∞ x s ↔ StarConvex ℝ≥0 x s := by
  simp_rw [StarConvex]
  congr! with x y
  constructor <;> intro h a b ha hb hab
  · apply h <;> [simp; simp; (dsimp; norm_cast)]
  · lift a to ℝ≥0
    · rintro rfl
      cases hab
    lift b to ℝ≥0
    · rintro rfl
      cases hab
    exact h (mod_cast ha) (mod_cast hb) (mod_cast hab)

theorem ENNReal.convex_iff (s : Set ℝ≥0∞) :
    Convex ℝ≥0∞ s ↔ Convex ℝ≥0 s := by
  simp_rw [Convex, ENNReal.starConvex_iff]

theorem ENNReal.convexHull_ennreal_eq (s : Set ℝ≥0∞) :
    convexHull ℝ≥0∞ s = convexHull ℝ≥0 s := by
  simp_rw [convexHull_eq_iInter, ENNReal.convex_iff]

[Yury G. Kudryashov]

This should be true in a module too (e.g., measures).

[Yaël Dillies]

:golf:

import Mathlib

open ENNReal NNReal

lemma ENNReal.forall {p : ℝ≥0∞ → Prop} : (∀ x, p x) ↔ p ⊤ ∧ ∀ x : ℝ≥0, p x := WithTop.forall

theorem ENNReal.starConvex_iff (x : ℝ≥0∞) (s : Set ℝ≥0∞) :
    StarConvex ℝ≥0∞ x s ↔ StarConvex ℝ≥0 x s := by
  simp [StarConvex, ENNReal.forall, ← ENNReal.coe_add, ENNReal.smul_def]