Starting convexity in mathlib

convex.lean

import analysis.normed_space.basic

namespace set
variables {α : Type*} [preorder α] {a₁ b₁ a₂ b₂ b x : α}
def Iic (b : α) := {x | x ≤ b}
@[simp] lemma mem_Iic : x ∈ Iic b ↔ x ≤ b := iff.rfl


lemma Icc_subset_Ico_iff (h₁ : a₁ ≤ b₁) :
  Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂ :=
⟨λ h, ⟨(h ⟨le_refl _, h₁⟩).1, (h ⟨h₁, le_refl _⟩).2⟩,
 λ ⟨h, h'⟩ x ⟨hx, hx'⟩, ⟨le_trans h hx, lt_of_le_of_lt hx' h'⟩⟩
end set

open set
local notation `I` := (Icc 0 1 : set ℝ)

section algebra
variables {E : Type*} [add_comm_group E] [vector_space ℝ E]
variables (x y : E)

def segment (x y : E) := {z : E | ∃ l : ℝ, l ∈ I ∧ z - x = l•(y-x)}
local notation `[`x `, ` y `]` := segment x y

lemma left_mem_segment (x y : E) : x ∈ [x, y] := ⟨0, ⟨⟨le_refl _, zero_le_one⟩, by simp⟩⟩
lemma right_mem_segment (x y : E) : y ∈ [x, y] := ⟨1, ⟨⟨zero_le_one, le_refl _⟩, by simp⟩⟩

lemma mem_segment_iff {x y z : E} : z ∈ [x, y] ↔ ∃ l ∈ I, z = x + l•(y - x) :=
by split ; rintro ⟨l, l_in, H⟩ ; use [l, l_in] ; try { rw sub_eq_iff_eq_add at H } ; rw H ; abel

lemma mem_segment_iff' {x y z : E} : z ∈ [x, y] ↔ ∃ l ∈ I, z = ((1:ℝ)-l)•x + l•y :=
begin
  split ; rintro ⟨l, l_in, H⟩ ; use [l, l_in] ; try { rw sub_eq_iff_eq_add at H } ; rw H ;
  simp only [smul_sub, sub_smul, one_smul] ; abel,
end

def is_convex (s : set E) := ∀ x y ∈ s, [x, y] ⊆ s

lemma segment_symm (x y : E) : [x, y] = [y, x] :=
begin
  ext z,
  rw [mem_segment_iff', mem_segment_iff'],
  split,
  all_goals {
    rintro ⟨l, ⟨hl₀, hl₁⟩, h⟩,
    use (1-l),
    split,
    split ; linarith,
    rw [h] ; simp },
end

lemma segment_eq_Icc {a b : ℝ} (h : a ≤ b) : [a, b] = Icc a b :=
begin
  ext z,
  rw mem_segment_iff,
  split,
  { rintro ⟨l, ⟨hl₀, hl₁⟩, H⟩,
    rw smul_eq_mul at H,
    have hba : 0 ≤ b - a, by linarith,
    split ; rw H,
    { have := mul_le_mul (le_refl l) hba (le_refl _) hl₀,
      simpa using this, },
    { have := mul_le_mul hl₁ (le_refl (b-a)) hba zero_le_one,
      rw one_mul at this,
      apply le_trans (add_le_add (le_refl a) this),
      convert le_refl _,
      show b = a + (b-a), by ring } },
  { rintro ⟨hza, hzb⟩,
    by_cases hba : b-a = 0,
    { use [(0:ℝ), ⟨le_refl 0, zero_le_one⟩],
      rw zero_smul, linarith },
    { have : (z-a)/(b-a) ∈ I,
      { change b -a ≠ 0 at hba,
        have : 0 < b - a, from lt_of_le_of_ne (by linarith) hba.symm,
        split,
        apply div_nonneg ; linarith,
        apply (div_le_iff this).2,
        simp, convert hzb, ring},
      use [(z-a)/(b-a), this],
      rw [smul_eq_mul, div_mul_cancel],
      ring,
      exact hba}}
end

lemma Ico_is_convex (a b : ℝ) : is_convex (Ico a b) :=
λ x y ⟨xa, xb⟩ ⟨ya, yb⟩, begin
  clear _fun_match _fun_match _x _x,
  wlog h : x ≤ y using x y,
  { rw segment_eq_Icc,
    rw Icc_subset_Ico_iff ; try {split}, all_goals { finish },
  },
  { revert a_2,
    rw segment_symm,
    apply this ; assumption }
end

lemma Iio_is_convex (b : ℝ) : is_convex (Iio b) :=
sorry

lemma Iic_is_convex (b : ℝ) : is_convex (Iic b) :=
sorry
end algebra

section normed
open metric real
variables {E : Type*} [normed_space ℝ E]

lemma balls_are_convex (a : E) (r : ℝ) : is_convex (ball a r) ∧ is_convex (closed_ball a r) :=
begin
  split ; try
  {intros x y x_in y_in z z_in,
  rcases mem_segment_iff'.1 z_in with ⟨l, l_in, H⟩,
  rcases mem_Icc.1 l_in with ⟨hl0, hl1⟩,
  have eq₁ : (1 - l) • x + l • y - a = (1 - l) • (x-a) + l • (y - a),
  { repeat {rw [smul_sub, sub_smul, one_smul]},
    set X := l•x,
    set Y := l•y,
    set A := l•a,
    change x - X + Y - a = x - X - (a - A) + (Y - A),
    abel },
  set d₁ := ∥x - a∥,
  set d₂ := ∥y - a∥,
  have ineq := calc
    ∥(1 - l) • x + l • y - a∥ = ∥(1 - l) • (x-a) + l • (y - a)∥ : by rw eq₁
    ... ≤ ∥(1 - l) • (x-a)∥ + ∥l • (y - a)∥ : norm_triangle _ _
    ... = abs(1 - l)*d₁ + abs l*d₂ : by repeat {rw [norm_smul, norm_eq_abs]}
    ... = (1 - l)*d₁ + l*d₂ : by { repeat { rw [abs_of_nonneg] } ; linarith } },

  { rw [mem_ball, dist_eq_norm] at *,
    rw H,
    have : (1 - l) * d₁ + l * d₂ < r,
    { suffices : (1 - l) * d₁ + l * d₂ ∈ Iio r,
      from mem_Iio.1 this,
      rw ←mem_Iio at x_in y_in,
      apply Iio_is_convex r d₁ d₂ x_in y_in (mem_segment_iff'.2 ⟨l, l_in, rfl⟩) },
    exact lt_of_le_of_lt ineq this },
  { rw [mem_closed_ball, dist_eq_norm] at *,
    rw H,
    have : (1 - l) * d₁ + l * d₂ ≤ r,
    { suffices : (1 - l) * d₁ + l * d₂ ∈ Iic r,
      from mem_Iic.1 this,
      rw ←mem_Iic at x_in y_in,
      apply Iic_is_convex r d₁ d₂ x_in y_in (mem_segment_iff'.2 ⟨l, l_in, rfl⟩) },
    exact le_trans ineq this },
end

lemma ball_is_convex (a : E) (r : ℝ) : is_convex (ball a r) :=
(balls_are_convex a r).1

lemma closed_ball_is_convex (a : E) (r : ℝ) : is_convex (closed_ball a r) :=
(balls_are_convex a r).2
end normed