Hahn-Banach following Kerjean and Mahboubi

hahn_banach.lean

import analysis.convex
import linear_algebra.dual

noncomputable theory
local attribute [instance, priority 0] classical.prop_decidable

-- Why can't I find this in mathlib?!
lemma div_le_div_iff {α : Type*} [linear_ordered_field α] {b d : α} (hd : 0 < d) (hb : 0 < b) (a c : α) :
  a/b ≤ c/d ↔ d*a ≤ b*c :=
by rw [div_le_iff' hb, ← mul_div_assoc, le_div_iff' hd]

-- Why can't I find this in mathlib?! I hate those lemmas
lemma sub_le_sub_iff {α : Type*} [ordered_comm_group α] (a b c d : α) :
a - b ≤ c - d ↔ a + d ≤ b + c :=
by rw [sub_le, show a - (c - d) = a + d - c, by abel, sub_le_iff_le_add]

open set function lattice module

namespace rel -- TODO: check whether these defs are not already somewhere in mathlib
variables {α : Type*} {β : Type*}

def functional (f : rel α β) :=
  ∀ v r₁ r₂, f v r₁ → f v r₂ → r₁ = r₂

def partial_order : partial_order (rel α β) :=
{ le :=  λ f g, ∀ {a b}, f a b → g a b,
  le_refl := λ _ _ _, id,
  le_trans := λ _ _ _ H H' _ _ hab, H' (H hab),
  le_antisymm := λ _ _ H H', by { ext, exact ⟨H, H'⟩ } }
end rel

variables {V : Type*} [add_comm_group V] [vector_space ℝ V] (f : rel V ℝ)

def rel.linear := ∀ v₁ v₂ (l r₁ r₂ : ℝ), f v₁ r₁ → f v₂ r₂ → f (v₁ + l • v₂) (r₁ + l • r₂)

def rel.prol (φ : V → ℝ) (F : set V)  := ∀ v ∈ F, f v (φ v)

def rel.maj_by (p : V → ℝ) := ∀ v r, f v r → r ≤ p v

section
variables {f} (hf : f.linear)
include hf

lemma linrel_00 {x r} (h : f x r) : f 0 0 :=
begin
  rw show f 0 0 = f (x + (-1 : ℝ) • x) (r + (-1 : ℝ) • r), by simp,
  exact hf x x (-1) r r h h,
end

lemma linrel_scale (x r l) : f x r → f (l • x) (l * r) :=
begin
  intro fxr,
  rw show f (l • x) (l * r) = f (0 + l • x) (0 + l * r), by simp,
  apply hf,
  exact linrel_00 hf fxr,
  exact fxr
end

lemma linrel_add (x₁ x₂ r₁ r₂) : f x₁ r₁ → f x₂ r₂ → f (x₁ - x₂) (r₁ - r₂) :=
begin
  rw show x₁ - x₂ = x₁ + (-1 : ℝ) • x₂, by simp,
  rw show r₁ - r₂ = r₁ + (-1 : ℝ) * r₂, by simp,
  apply hf
end

lemma linrel_lc {x₁ x₂ r₁ r₂} (t s) : f x₁ r₁ → f x₂ r₂ → f (t • x₁ + s • x₂) (t*r₁ + s*r₂) :=
λ  h₁ h₂, hf _ _ _ _  _ (linrel_scale hf x₁ r₁ t h₁) h₂
end

def add_line (w a) := λ v r, ∃ (v' : V) (r' l : ℝ), f v' r' ∧ v = v' + l • w ∧ r = r' + l * a

variables (φ : V → ℝ) (F : submodule ℝ V) (p : V → ℝ)

structure zorn_type :=
(carrier : rel V ℝ)
(func    : carrier.functional)
(lin     : carrier.linear)
(maj_by  : carrier.maj_by p)
(prol    : carrier.prol φ F.carrier)

def spec := f.functional ∧ f.linear ∧ f.maj_by p ∧ f.prol φ F.carrier

variables {f φ F p}

def zorn_type.mk' (s : spec f φ F p) : zorn_type φ F p := zorn_type.mk _ s.1 s.2.1 s.2.2.1 s.2.2.2

instance : has_coe_to_fun (zorn_type φ F p) := ⟨_, zorn_type.carrier⟩

def graph_over (F : set V) (φ : V → ℝ): rel V ℝ := λ v r, v ∈ F ∧ r = φ v

-- There is probably a way to avoid repeating `φ F p` all over the place. I should ask.

@[extensionality]
lemma zorn_type.ext (z₁ z₂ : zorn_type φ F p) : z₁.carrier = z₂.carrier → z₁ = z₂ :=
λ h, by { cases z₁, cases z₂, congr, exact h}

instance : partial_order (zorn_type φ F p) :=
  partial_order.lift _ zorn_type.ext rel.partial_order

lemma zorn_type.le_iff (z₁ z₂ : zorn_type φ F p) : z₁ ≤ z₂ ↔ ∀ v r, z₁ v r → z₂ v r :=
⟨λ h _ _ h₁, h h₁, id⟩

-- My coercion idea is probably not so smart...
lemma zut (z : zorn_type φ F p) (v r): z v r ↔ z.carrier v r := iff.rfl

section preparation
variables (φ F p)

def is_linear_on (F : submodule ℝ V) (φ : V → ℝ) := ∀ (v₁ v₂ ∈ F) (l : ℝ), φ (v₁ + l • v₂) = φ v₁ + l • (φ v₂).

variables (lin_φ_F : is_linear_on F φ)

include lin_φ_F

lemma phi0 : φ 0 = 0 :=
by { rw [show (0 : V) = 0 + (-1 : ℝ) • 0, by simp, lin_φ_F _ _ F.zero_mem F.zero_mem], simp }

lemma zorn_rel_ex (s : spec (graph_over F.carrier φ) φ F p) : ∃ g : zorn_type φ F p, ∀ z, g ≤ z → z = g :=
begin
  apply zorn.zorn_partial_order,
  intros A Achain,
  by_cases h : ∃ z, z ∈ A,
  { cases h with f f_in,
    let g : rel V ℝ := λ v r, ∃  a ∈ A, (a v r : Prop), -- don't know why the elaborator needs help
    have g_fun : g.functional,
    { rintros v r₁ r₂ ⟨a₁, in₁, h₁⟩ ⟨a₂, in₂, h₂⟩,
      rcases Achain.directed in₁ in₂ with ⟨z, z_in, hz₁, hz₂⟩, -- A variant of KM, for fun
      rw zorn_type.le_iff at *,
      exact z.func v _ _ (hz₁ v r₁ h₁) (hz₂ v r₂ h₂) },
    have g_lin : g.linear,
    { rintros v₁ v₂ l r₁ r₂ ⟨a₁, in₁, c₁⟩ ⟨a₂, in₂, c₂⟩,
      rcases Achain.total_of_refl in₁ in₂ with h ; rw zorn_type.le_iff at h, -- back to KM
      { use [a₂, in₂, by apply a₂.lin ; solve_by_elim] },
      { use [a₁, in₁, by apply a₁.lin ; solve_by_elim] } },
    have g_maj : g.maj_by p, from λ v r ⟨z, _, h⟩, z.maj_by _ _ h,
    have g_prol : g.prol φ F.carrier, from λ v v_in, ⟨f, f_in, f.prol v v_in⟩,
    exact ⟨zorn_type.mk _ g_fun g_lin g_maj g_prol, λ z z_in _ _ h, ⟨z, z_in, h⟩⟩ },
  { use zorn_type.mk' s,
    intros a H,
    exact false.elim (h ⟨a, H⟩) }
end

variables {φ F p} (hp : convex_on univ p)

include hp

lemma domain_extend (z : zorn_type φ F p) (v : V) : ∃ ze : zorn_type φ F p, z ≤ ze ∧ ∃ r, ze v r :=
begin
  by_cases H : ∃ r, z v r,
  { cases H with r rh,
    exact ⟨z, le_refl _, r, rh⟩ },
  { have z0 : z 0 0, from (phi0 φ F lin_φ_F) ▸ z.prol 0 F.zero_mem,
    have key : ∃ a : ℝ, ∀ x r l, z x r → r + l * a ≤ p (x + l • v),
    { suffices : ∃ a, ∀ x r l, z x r → 0 < l → r + l*a ≤ p (x + l • v) ∧ r - l*a ≤ p (x - l • v),
      { cases this with a aP,
        use a,
        introv zxr,
        rcases lt_trichotomy 0 l with h | ⟨h | h⟩,
        { exact (aP x r l zxr h).1 },
        { rw [← h, zero_mul, zero_smul, add_zero, add_zero],
          exact z.maj_by _ _ zxr, },
        { convert (aP x r (-l) zxr (by linarith)).2 ; simp } },
      let B := λ x r l, (p (x + l • v) - r)/l,
      let A := λ x r l, (r - p (x - l • v))/l,
      have le_AB : ∀ x₁ x₂ r₁ r₂ s t, z x₁ r₁ → z x₂ r₂ → 0 < s → 0 < t → A x₁ r₁ s ≤ B x₂ r₂ t,
      { introv zx₁ zx₂ lt0s lt0t,
        dsimp only [A, B],
        have lt0ts : 0 < t + s, by linarith,
        let X := x₁ - s • v,
        let Y := x₂ + t • v,
        replace hp := ((convex_on_iff_div _ _).1 hp).2 (mem_univ X) (mem_univ Y)
                        (le_of_lt lt0t) (le_of_lt lt0s) lt0ts,
        rw div_le_div_iff lt0t lt0s,
        change t • (r₁ - p X) ≤ s • (p Y - r₂),
        have := z.maj_by _ _ zx₁,
        rw [smul_sub, smul_sub, sub_le_sub_iff, ← div_le_div_right lt0ts],
        repeat { rw add_div }, repeat { rw [smul_eq_mul, mul_div_right_comm] },
        set T := t/(t+s), set S := s/(t+s),
        change T • r₁ + S • r₂ ≤ T * p X + S * p Y,
        rw ← show T • x₁ + S • x₂ = T • X + S • Y,
        { dsimp only [T, S, X, Y],
          rw [smul_sub,  smul_add, smul_smul, smul_smul, div_mul_comm],
          simp } at hp,
        exact le_trans (z.maj_by _ _ (linrel_lc z.lin T S zx₁ zx₂)) hp },
        let Pa := {r | ∃ x₁ r₁ s₁, z x₁ r₁ ∧ 0 < s₁ ∧ r = A x₁ r₁ s₁ },
        let Pb := {r | ∃ x₁ r₁ s₁, z x₁ r₁ ∧ 0 < s₁ ∧ r = B x₁ r₁ s₁ },
        have zlo : (0 : ℝ) < 1 := zero_lt_one,
        have exPa : A 0 0 1 ∈ Pa, from ⟨0, 0, 1, by simp [z0, zlo]⟩,
        have exPb : B 0 0 1 ∈ Pb, from ⟨0, 0, 1, by simp [z0, zlo]⟩,
        have majPa : ∀ x ∈ Pa, x ≤ B 0 0 1,
        { rintros x ⟨y, r, s, zry, lts, rfl⟩,
          apply le_AB ; assumption },
        have minPb : ∀ x ∈ Pb, A 0 0 1 ≤ x,
        { rintros x ⟨y, r, s, zry, lts, rfl⟩,
          apply le_AB ; try { assumption } },
        cases is_lub_cSup (ne_empty_of_mem exPa) ⟨_, majPa⟩ with ubdP saP,
        cases is_glb_cInf (ne_empty_of_mem exPb) ⟨_, minPb⟩ with ibdP ibP,
        set sa := Sup Pa,
        set ib := Inf Pb,
        have le_sa_ib : sa ≤ ib,
        { apply saP,
          rintros r' ⟨y, r, l, zry, lt0l, rfl⟩,
          apply ibP,
          rintros s' ⟨w, s, m, zrw, lt0m, rfl⟩,
          apply le_AB ; assumption },
        clear le_AB,
        let α := (sa + ib)/2,
        have le_α_ib : α ≤ ib, by dsimp [α] ; linarith,
        have le_sa_α : sa ≤ α, by dsimp [α] ; linarith,
        use α,
        introv zxr lt0l,
        split,
        { suffices : α ≤ B x r l,
          { dsimp only [B] at this,
            rw le_div_iff' lt0l at this,
            linarith },
          apply le_trans le_α_ib _,
          apply ibdP,
          use [x, r, l],
          simp [*] },
        { suffices : A x r l ≤ α,
          { dsimp only [A] at this,
            rw div_le_iff' lt0l at this,
            linarith },
          apply le_trans _ le_sa_α,
          apply ubdP,
          use [x, r, l],
          simp [*] } },
    cases key with a ha,
    refine ⟨⟨add_line z v a, _, _, _, _⟩, _⟩,
    { rintros w r₁ r₂ ⟨w₁, s₁, m₁, h₁, rfl, rfl⟩ ⟨w₂, s₂, m₂, h₂, h₂', rfl⟩,
      have H₁ : ∀ (x : V) (r l : ℝ), x = l • v →  z x r → x = 0 ∧ l = 0,
      { rintros x r l rfl hz,
        by_cases hl : l = 0,
        { simp [hl] },
        { suffices zvs : z v (l⁻¹*r), from false.elim (H ⟨_, zvs⟩),
          rw show v = l⁻¹ • (l • v), by rw [smul_smul, inv_mul_cancel hl, one_smul],
          apply linrel_scale z.lin,
          exact hz } },
      have : ∃ r, z (w₁ - w₂) r,
      { use s₁ + (-1)*s₂,
        rw show w₁ - w₂ = w₁ + (-1 : ℝ) • w₂, by simp,
        apply z.lin ; assumption },
      cases this with rw₁₂ erw₁₂,
      have : w₁ - w₂ = 0 ∧ (m₂ - m₁ = 0),
      { apply H₁,
        { rw ← sub_eq_zero at h₂' ⊢,
          rw [← h₂', sub_smul],
          abel },
        { exact erw₁₂ } },
      cases this with erw₁₂ eqP,
      suffices : s₁ = s₂, by rw [this, eq_of_sub_eq_zero eqP],
      apply z.func w₁ _ _ h₁,
      rwa eq_of_sub_eq_zero erw₁₂ },
    { rintros x₁ x₂ l r₁ r₂ ⟨w₁, s₁, m₁, h₁, rfl, rfl⟩ ⟨w₂, s₂, m₂, h₂, rfl, rfl⟩,
      let w := _, let s := _,
      change add_line z v a w s,
      rw show w = w₁ + l • w₂ + (m₁ + l*m₂) • v,
      { dsimp [w],
        rw [smul_add, add_smul, smul_smul],
        abel },
      rw show s = s₁ + l * s₂ + (m₁ + l*m₂) * a,
      { dsimp[s],
        ring },
      use [w₁ + l • w₂, s₁ + l *s₂, m₁ + l*m₂],
      refine ⟨z.lin _ _ _ _ _ h₁ h₂, _⟩,
      simp },
    { rintros x r ⟨v', r', l, h, rfl, rfl⟩,
      exact ha _ _ _ h },
    { intros x x_in,
      use [x, φ x, 0],
      simpa using z.prol x x_in },
    split,
    { rw zorn_type.le_iff,
      intros v' r h,
      change ∃ (v' : V) (r' l : ℝ), _,
      use [v', r, 0],
      simp [h] },
    { use [a, 0, 0, 1],
      simp [z0] } }
end

lemma tot_g {g : zorn_type φ F p} (hg : ∀ z, g ≤ z → z = g) : ∀ v, ∃ r, g v r :=
begin
  intro v,
  rcases domain_extend lin_φ_F hp g v with ⟨z, hgz, H⟩,
  rw zorn_type.le_iff at hgz,
  rwa hg z hgz at H
end

lemma hb_witness {g : zorn_type φ F p} (hg : ∀ z, g ≤ z → z = g) :
 ∃ h : V → ℝ, ∀ v r, g v r ↔ (h v = r) :=
begin
  choose h H using tot_g lin_φ_F hp hg,
  use h,
  intros v r,
  split ; intro hyp,
  { rw g.func v r (h v) hyp (H v) },
  { rw ← hyp,
    apply H },
end
end preparation

variables {F} {p}


theorem hahn_banach (hp : convex_on univ p)
  {f : V → ℝ} (lin_f : is_linear_on F f) (H : ∀ x ∈ F, f x ≤ p x) :
  ∃ g : dual ℝ V, (∀ x, g x ≤ p x) ∧ (∀ x ∈ F, g x = f x) :=
begin
  let graphF : rel V ℝ := graph_over F.carrier f,
  have func_graphF : graphF.functional, from λ _ _ _ ⟨_, h₁⟩ ⟨_, h₂⟩, by rw [h₁, h₂],
  have lin_graphF : graphF.linear, from λ v₁ v₂ l r₁ r₂ ⟨in₁, h₁⟩ ⟨in₂, h₂⟩,
    h₁.symm ▸ h₂.symm ▸ ⟨F.add_mem in₁ (F.smul_mem l in₂), (lin_f _ _ in₁ in₂ l).symm⟩,
  have maj_graphF : graphF.maj_by p, from λ v _ ⟨v_in, h⟩, h.symm ▸ H v v_in,
  have prol_graphF : graphF.prol f F.carrier, from λ v v_in,  ⟨v_in, rfl⟩,
  have graphFP : spec graphF f F p, from ⟨func_graphF, lin_graphF, maj_graphF, prol_graphF⟩,

  cases zorn_rel_ex f F p lin_f graphFP with z zmax,
  cases hb_witness lin_f hp zmax with g gP,
  have gadd : ∀ (v₁ v₂ : V), g (v₁ + v₂) = g v₁ + g v₂,
  { intros,
    rw ← gP,
    have := z.lin v₁ v₂ 1 (g v₁) (g v₂),
    repeat { rw ← zut at this },
    rw [gP, gP, one_smul, one_smul] at this,
    exact this rfl rfl },
  have gsmul : ∀ (c : ℝ) (v : V), g (c • v) = c • g v,
  { intros,
    rw ← gP,
    have := z.lin 0 v c 0 (g v),
    repeat { rw ← zut at this },
    have z00 : z 0 0, by simpa [phi0 f F lin_f] using z.prol 0 F.zero_mem,
    specialize this z00,
    rw [gP, zero_add, zero_add ] at this,
    exact this rfl },
  have gbound : ∀ v, g v ≤ p v,
  { intros,
    have := z.maj_by v (g v),
    rw [← zut, gP] at this,
    exact this rfl },
  have gextend : ∀ v ∈ F, g v = f v,
  { introv v_in,
    rw ← gP,
    exact z.prol v v_in },
  exact ⟨⟨g, gadd, gsmul⟩, gbound, gextend⟩,
end