-
-
Save PatrickMassot/328b58599618f8642da7fd45a5457f17 to your computer and use it in GitHub Desktop.
Hahn-Banach following Kerjean and Mahboubi
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment