Module mathcomp.analysis.functional_analysis.hahn_banach_theorem
From HB Require Import structures.From mathcomp Require Import boot order algebra interval_inference.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp contra classical_sets filter.
From mathcomp Require Import reals convex topology normedtype.
# The Hahn-Banach theorem
This file proves the Hahn-Banach theorem thanks to Zorn's lemma. Theorem
`hahn_banach_extension` states that, considering `V` an lmodType on a
realtype, a linear function on a subLmodType of V, that is bounded by a
convex function, can be extended to a linear map on V bounded by the same
convex function.
Theorem `hahn_banach_extension_normed` specifies this to the extension of
a linear continuous function defined on a subnormedmodule to the whole
normed module.
Theorem `hahn_banach_extension_subctvs` allows to extend a linear function
defined on a subconvextvs to a convextvs.
Theorem `hahn_banach_extension_initialsubctvs` allows to extend a linear
function defined on a sublmodule to a convextvs.
| Extension theorem | subcodomain | codomain |
|--------------------------------------|------------------|---------------|
| hahn_banach_extension | subLmodType | lmodType |
| hahn_banach_extension_normed | subNormedmodType | normedModType |
| hahn_banach_extension_subcvts | subconvextvsType | convexTvsType |
| hahn_banach_extension_initialsubctvs | subLmodType | convexTvsType |
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Local Open Scope convex_scope.
Local Open Scope real_scope.
module with definitions on linear relations, thought of as graph of
functions
Module LinearGraphInternalSource code.Section linear_graph.
Context (RSource code : numDomainType) (VSource code : lmodType R).
Definition graph
Source code := V -> R -> Prop.
Definition linear_graph
Source code (fSource code : graph) :=
forall v1Source code v2Source code lSource code r1Source code r2Source code, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2).
Variable fSource code : graph.
Hypothesis lfSource code : linear_graph f.
Lemma lingraph_00Source code xSource code rSource code : f x r -> f 0 0.
Lemma lingraphZSource code xSource code rSource code lSource code : f x r -> f (l *: x) (l * r).
Proof.
Lemma lingraphDSource code x1Source code x2Source code r1Source code r2Source code : f x1 r1 -> f x2 r2 -> f (x1 - x2) (r1 - r2).
End linear_graph.
End LinearGraphInternal.
module with definition of the type `zorn_type` of linear functional
graphs, bounded by a convex function and extending to the whole space a
given linear graph
Module HahnBanachZornInternalSource code.Section hahnbanachzorn.
Import LinearGraphInternal.
Context (RSource code : realType) (VSource code : lmodType R) (FSource code : pred V)
(F'Source code : subLmodType F) (phiSource code : {linear F' -> R}) (pSource code : V -> R).
Implicit Types f g : graph V.
Hypothesis phi_le_pSource code : forall vSource code, phi v <= p (val v).
Hypothesis p_cvxSource code : @convex_function R V [set: V] p.
Definition extend_graph
LinearGraphInternal.graph : forall [R : numDomainType], lmodType R -> Type LinearGraphInternal.graph is not universe polymorphic Arguments LinearGraphInternal.graph [R] V LinearGraphInternal.graph is transparent Expands to: Constant mathcomp.analysis.functional_analysis.hahn_banach_theorem.LinearGraphInternal.graph Declared in library mathcomp.analysis.functional_analysis.hahn_banach_theorem, line 51, characters 11-16
Source code fSource code := forall vSource code : F', f (\val v) (phi v).
Definition le_graph
LinearGraphInternal.linear_graph : forall [R : numDomainType] [V : lmodType R], LinearGraphInternal.graph (R:=R) V -> Prop LinearGraphInternal.linear_graph is not universe polymorphic Arguments LinearGraphInternal.linear_graph [R V] f LinearGraphInternal.linear_graph is transparent Expands to: Constant mathcomp.analysis.functional_analysis.hahn_banach_theorem.LinearGraphInternal.linear_graph Declared in library mathcomp.analysis.functional_analysis.hahn_banach_theorem, line 53, characters 11-23
Source code pSource code fSource code := forall vSource code rSource code, f v r -> r <= p v.
Definition functional_graph
HahnBanachZornInternal.extend_graph : forall [R : realType] [V : lmodType R] [F : pred V] [F' : subLmodType (V:=V) F], {linear F' -> R} -> graph (R:=R) V -> Prop HahnBanachZornInternal.extend_graph is not universe polymorphic Arguments HahnBanachZornInternal.extend_graph [R V F F'] phi f HahnBanachZornInternal.extend_graph is transparent Expands to: Constant mathcomp.analysis.functional_analysis.hahn_banach_theorem.HahnBanachZornInternal.extend_graph Declared in library mathcomp.analysis.functional_analysis.hahn_banach_theorem, line 88, characters 11-23
Source code fSource code := forall vSource code r1Source code r2Source code, f v r1 -> f v r2 -> r1 = r2.
Definition le_extend_graph
HahnBanachZornInternal.le_graph : forall [R : realType] [V : lmodType R], (V -> R) -> graph (R:=R) V -> Prop HahnBanachZornInternal.le_graph is not universe polymorphic Arguments HahnBanachZornInternal.le_graph [R V] p%_function_scope f HahnBanachZornInternal.le_graph is transparent Expands to: Constant mathcomp.analysis.functional_analysis.hahn_banach_theorem.HahnBanachZornInternal.le_graph Declared in library mathcomp.analysis.functional_analysis.hahn_banach_theorem, line 90, characters 11-19
Source code fSource code :=
[/\ functional_graph f, linear_graph f, le_graph p f & extend_graph f].
Record zorn_typeSource code : Type := ZornType
{carrierSource code : graph V; specPSource code : le_extend_graph carrier}.
Implicit Types z : zorn_type.
Let spec_phiSource code :
le_extend_graph (fun vSource code rSource code => exists2 ySource code : F', v = val y & r = phi y).
Proof.
Definition zphi
HahnBanachZornInternal.functional_graph : forall [R : realType] [V : lmodType R], graph (R:=R) V -> Prop HahnBanachZornInternal.functional_graph is not universe polymorphic Arguments HahnBanachZornInternal.functional_graph [R V] f HahnBanachZornInternal.functional_graph is transparent Expands to: Constant mathcomp.analysis.functional_analysis.hahn_banach_theorem.HahnBanachZornInternal.functional_graph Declared in library mathcomp.analysis.functional_analysis.hahn_banach_theorem, line 92, characters 11-27
Source code := ZornType spec_phi.
Lemma zorn_type_eqSource code z1Source code z2Source code : carrier z1 = carrier z2 -> z1 = z2.
Proof.
case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; rewrite e in pm1 pm2 *.
by congr ZornType; exact: Prop_irrelevance.
Qed.
by congr ZornType; exact: Prop_irrelevance.
Qed.
Definition zornS
HahnBanachZornInternal.le_extend_graph : forall [R : realType] [V : lmodType R] [F : pred V] [F' : subLmodType (V:=V) F], {linear F' -> R} -> (V -> R) -> graph (R:=R) V -> Prop HahnBanachZornInternal.le_extend_graph is not universe polymorphic Arguments HahnBanachZornInternal.le_extend_graph [R V F F'] phi p%_function_scope f HahnBanachZornInternal.le_extend_graph is transparent Expands to: Constant mathcomp.analysis.functional_analysis.hahn_banach_theorem.HahnBanachZornInternal.le_extend_graph Declared in library mathcomp.analysis.functional_analysis.hahn_banach_theorem, line 94, characters 11-26
Source code z1Source code z2Source code := forall xSource code ySource code, carrier z1 x y -> carrier z2 x y.
Lemma zornS_exSource code : exists gSource code : zorn_type, forall zSource code, zornS g z -> z = g.
Proof.
pose Rbool xSource code ySource code := `[< zornS x y >].
have RboolP z t : Rbool z t <-> zornS z t by split => /asboolP.
suff [t st] : exists tSource code : zorn_type, forall sSource code : zorn_type, Rbool t s -> s = t.
by exists t; move => z /RboolP tz; exact: st.
apply: (@Zorn zorn_type Rbool); first by move=> t; exact/RboolP.
- by move=> r s t /RboolP a /RboolP b; apply/RboolP => x y /a /b.
- move=> r s /RboolP a /RboolP b; apply: zorn_type_eq.
by apply: funext => z; apply: funext => h; apply: propext; split => [/a | /b].
move=> A Amax.
have [[w Aw]|eA] := lem (exists aSource code, A a); last first.
by exists zphi => a Aa; absurd: eA; exists a.
(* g is the union of the graphs indexed by elements in a *)
pose g vSource code rSource code := exists2 aSource code, A a & carrier a v r.
have g_fun : functional_graph g.
move=> v r1 r2 [a Aa avr1] [b Ab bvr2].
have [|] : Rbool a b \/ Rbool b a by exact: Amax.
- rewrite /Rbool /RboolP /zornS.
case: b Ab bvr2 {Aa} => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2.
by move/ecas2 : avr1 => /fs2 /(_ s2vr2).
- rewrite /Rbool /RboolP /zornS.
case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1.
by move/ecbs1: bvr2; exact: fs1.
have g_lin : linear_graph g.
move=> v1 v2 l r1 r2 [a1 Aa1 c1] [a2 Aa2 c2].
have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2.
- have {sc12 Aa1 a1} {}c1 : carrier a2 v1 r1 by exact: sc12.
by exists a2 => //; case: a2 {Aa2} c2 c1 => c /= [_ + _ _] *; exact.
- have {sc21 Aa2 a2} {}c2 : carrier a1 v2 r2 by exact: sc21.
by exists a1 => //; case: a1 {Aa1} c2 c1 => c /= [_ + _ _] *; exact.
have g_majp : le_graph p g by move=> v r [[c/= [fs1 ls1 ms1 ps1]]]/= _ => /ms1.
have g_prol : extend_graph g.
by move=> *; exists w => //; case: w Aw => [c [_ _ _ +]] _ //=; exact.
have spec_g : le_extend_graph g by split.
pose zg := ZornType spec_g.
by exists zg => [a Aa]; apply/RboolP; rewrite /zornS => v r cvr; exists a.
Qed.
have RboolP z t : Rbool z t <-> zornS z t by split => /asboolP.
suff [t st] : exists tSource code : zorn_type, forall sSource code : zorn_type, Rbool t s -> s = t.
by exists t; move => z /RboolP tz; exact: st.
apply: (@Zorn zorn_type Rbool); first by move=> t; exact/RboolP.
- by move=> r s t /RboolP a /RboolP b; apply/RboolP => x y /a /b.
- move=> r s /RboolP a /RboolP b; apply: zorn_type_eq.
by apply: funext => z; apply: funext => h; apply: propext; split => [/a | /b].
move=> A Amax.
have [[w Aw]|eA] := lem (exists aSource code, A a); last first.
by exists zphi => a Aa; absurd: eA; exists a.
(* g is the union of the graphs indexed by elements in a *)
pose g vSource code rSource code := exists2 aSource code, A a & carrier a v r.
have g_fun : functional_graph g.
move=> v r1 r2 [a Aa avr1] [b Ab bvr2].
have [|] : Rbool a b \/ Rbool b a by exact: Amax.
- rewrite /Rbool /RboolP /zornS.
case: b Ab bvr2 {Aa} => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2.
by move/ecas2 : avr1 => /fs2 /(_ s2vr2).
- rewrite /Rbool /RboolP /zornS.
case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1.
by move/ecbs1: bvr2; exact: fs1.
have g_lin : linear_graph g.
move=> v1 v2 l r1 r2 [a1 Aa1 c1] [a2 Aa2 c2].
have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2.
- have {sc12 Aa1 a1} {}c1 : carrier a2 v1 r1 by exact: sc12.
by exists a2 => //; case: a2 {Aa2} c2 c1 => c /= [_ + _ _] *; exact.
- have {sc21 Aa2 a2} {}c2 : carrier a1 v2 r2 by exact: sc21.
by exists a1 => //; case: a1 {Aa1} c2 c1 => c /= [_ + _ _] *; exact.
have g_majp : le_graph p g by move=> v r [[c/= [fs1 ls1 ms1 ps1]]]/= _ => /ms1.
have g_prol : extend_graph g.
by move=> *; exists w => //; case: w Aw => [c [_ _ _ +]] _ //=; exact.
have spec_g : le_extend_graph g by split.
pose zg := ZornType spec_g.
by exists zg => [a Aa]; apply/RboolP; rewrite /zornS => v r cvr; exists a.
Qed.
Variable gSource code : zorn_type.
Lemma domain_extendSource code zSource code vSource code : exists2 zeSource code, zornS z ze & exists rSource code, (carrier ze) v r.
Proof.
have [[r rP]|] := lem (exists rSource code, carrier z v r).
by exists z => //; exists r.
case: z => [c [fs1 ls1 ms1 ps1]] /= nzv.
have c00 : c 0 0.
have <- : phi 0 = 0 by rewrite linear0.
by have := ps1 0; rewrite GRing.val0.
have [a aP] : exists aSource code, forall (xSource code : V) (rSource code lambdaSource code : R), c x r ->
r + lambda * a <= p (x + lambda *: v).
suff [a aP] : exists aSource code, forall (xSource code : V) (rSource code lambdaSource code : R), c x r -> 0 < lambda ->
r + lambda * a <= p (x + lambda *: v) /\
r - lambda * a <= p (x - lambda *: v).
exists a => x r lambda /[dup] cxr /aP {}aP.
have [/aP[]// | ltl0 | ->] := ltrgt0P lambda.
rewrite -[lambda]opprK scaleNr mulNr.
by have /aP[] : 0 < - lambda by rewrite oppr_gt0.
by rewrite mul0r scale0r !addr0 ms1.
pose b (xSource code : V) rSource code lambdaSource code : R := (p (x + lambda *: v) - r) / lambda.
pose a (xSource code : V) rSource code lambdaSource code : R := (r - p (x - lambda *: v)) / lambda.
have le_a_b x1 x2 r1 r2 (sSource code tSource code : R) : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t ->
a x1 r1 s <= b x2 r2 t.
move=> cxr1 cxr2 lt0s lt0t; rewrite /a /b.
rewrite ler_pdivlMr// mulrAC ler_pdivrMr// [leLHS]mulrC [leRHS]mulrC.
rewrite !mulrDr !mulrN lerBlDr addrAC lerBrDr.
have /ler_pM2r <- : 0 < (s + t)^-1 by rewrite invr_gt0 addr_gt0.
set y1 : V := _ + _ *: _; set y2 : V := _ - _ *: _.
rewrite (@le_trans _ _ (p (s / (s + t) *: y1 + t / (s + t) *: y2)))//.
set u : V := (X in p X).
have {u y1 y2} -> : u = t / (s + t) *: x1 + s / (s + t) *: x2.
rewrite /u ![_ / _]mulrC -!scalerA -!scalerDr /y1 /y2; congr (_ *: _).
by rewrite !scalerDr addrCA scalerN scalerA (mulrC s) -scalerA addrK.
set l := t / _; set m := s / _.
rewrite [leLHS](_ : _ = l * r1 + m * r2).
by rewrite mulrDl ![_ * _ / _]mulrAC.
apply: ms1; apply: (ls1) => //.
by rewrite -[_ *: _]add0r -[_ * _]add0r; exact: ls1.
rewrite !mulrDl ![_ * _ / _]mulrAC -divD_onem//.
pose st := Itv01 (divDl_ge0 (ltW lt0s) (ltW lt0t))
(divDl_le1 (ltW lt0s) (ltW lt0t)).
exact: (p_cvx st (in_setT y1) (in_setT y2)).
pose Pa :=
[set rSource code | exists x1Source code r1Source code (s1Source code : R), [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]].
pose Pb :=
[set rSource code | exists x1Source code r1Source code (s1Source code : R), [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]].
pose sa := sup Pa. (* We need p with values in a *realType* *)
have Pax : Pa !=set0 by exists (a 0 0 1), 0, 0, 1.
have ubdP : ubound Pa sa.
apply: sup_upper_bound; split => //=.
by exists (b 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; exact: le_a_b.
have saP (uSource code : R) : ubound Pa u -> sa <= u by exact: ge_sup.
pose ib := inf Pb. (* We need P with values in a *realType* *)
have Pbx : Pb !=set0 by exists (b 0 0 1), 0, 0, 1.
have ibdP : lbound Pb ib.
apply: ge_inf; exists (a 0 0 1) => /= x [y [r [s [cry lt0s ->]]]].
exact: le_a_b.
have ibP (uSource code : R) : lbound Pb u -> u <= ib by exact: lb_le_inf Pbx.
have le_sa_ib : sa <= ib.
apply: saP => _ [y [r [l [cry lt0l ->]]]].
by apply: ibP => _ [z [s [m [crz lt0m ->]]]]; exact: le_a_b.
pose alpha := (sa + ib) / 2.
exists alpha => x r l cxr lt0l; split.
- suff : alpha <= b x r l by rewrite (ler_pdivlMr _ _ lt0l) lerBrDl mulrC.
by apply: (le_trans (midf_le le_sa_ib).2); apply: ibdP; exists x, r, l.
- suff : a x r l <= alpha.
by rewrite (ler_pdivrMr _ _ lt0l) lerBlDl -lerBlDr mulrC.
by apply: (le_trans _ (midf_le le_sa_ib).1); apply: ubdP; exists x, r, l.
pose z' := fun kSource code rSource code => exists (v'Source code : V) (r'Source code lambdaSource code : R),
[/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a].
have z'_extends x r : c x r -> z' x r.
by move=> cxr; exists x, r, 0; split; rewrite // ?scale0r ?mul0r ?addr0.
have z'_prol : extend_graph z'.
move=> x.
by exists (val x), (phi x), 0; split; rewrite // ?scale0r ?mul0r ?addr0.
have z'_maj_by_p : le_graph p z'
by move=> x r [w [s [l [cws -> ->]]]]; apply: aP.
have z'_lin : linear_graph z'.
move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]].
rewrite [X in z' X _](_ : _ = w1 + l *: w2 + (m1 + l * m2) *: v).
by rewrite !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA.
rewrite [X in z' _ X](_ : _ = s1 + l * s2 + (m1 + l * m2) * a).
by rewrite !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA.
exists (w1 + l *: w2), (s1 + l * s2), (m1 + l * m2); split => //.
exact: ls1.
have z'_functional : functional_graph z'.
move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]].
have [rw12 erw12] : exists rSource code, c (w1 - w2) r.
by exists (s1 + -1 * s2); rewrite -(scaleN1r w2); exact: ls1.
have h1 (xSource code : V) (rSource code lSource code : R) : x = l *: v -> c x r -> x = 0 /\ l = 0.
move=> -> cxr; have [->|ln0] := eqVneq l 0; first by rewrite scale0r.
suff cvs : c v (l^-1 * r) by absurd: nzv; exists (l^-1 * r).
suff -> : v = l ^-1 *: (l *: v).
by rewrite -(add0r (_ *: _)) -(add0r (_ * _)); exact: ls1.
by rewrite scalerA mulVf ?scale1r.
have [ew12] : w1 - w2 = 0 /\ m2 - m1 = 0.
apply: h1 erw12; rewrite scalerBl.
by apply: subr0_eq; rewrite opprB addrACA e1 -opprD subrr.
suff -> : s1 = s2 by move/subr0_eq => ->.
by apply: fs1 cws2; rewrite -(subr0_eq ew12).
have z'_spec : le_extend_graph z' by [].
exists (ZornType z'_spec) => //=; exists a, 0, 0, 1.
by rewrite !add0r mul1r scale1r.
Qed.
by exists z => //; exists r.
case: z => [c [fs1 ls1 ms1 ps1]] /= nzv.
have c00 : c 0 0.
have <- : phi 0 = 0 by rewrite linear0.
by have := ps1 0; rewrite GRing.val0.
have [a aP] : exists aSource code, forall (xSource code : V) (rSource code lambdaSource code : R), c x r ->
r + lambda * a <= p (x + lambda *: v).
suff [a aP] : exists aSource code, forall (xSource code : V) (rSource code lambdaSource code : R), c x r -> 0 < lambda ->
r + lambda * a <= p (x + lambda *: v) /\
r - lambda * a <= p (x - lambda *: v).
exists a => x r lambda /[dup] cxr /aP {}aP.
have [/aP[]// | ltl0 | ->] := ltrgt0P lambda.
rewrite -[lambda]opprK scaleNr mulNr.
by have /aP[] : 0 < - lambda by rewrite oppr_gt0.
by rewrite mul0r scale0r !addr0 ms1.
pose b (xSource code : V) rSource code lambdaSource code : R := (p (x + lambda *: v) - r) / lambda.
pose a (xSource code : V) rSource code lambdaSource code : R := (r - p (x - lambda *: v)) / lambda.
have le_a_b x1 x2 r1 r2 (sSource code tSource code : R) : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t ->
a x1 r1 s <= b x2 r2 t.
move=> cxr1 cxr2 lt0s lt0t; rewrite /a /b.
rewrite ler_pdivlMr// mulrAC ler_pdivrMr// [leLHS]mulrC [leRHS]mulrC.
rewrite !mulrDr !mulrN lerBlDr addrAC lerBrDr.
have /ler_pM2r <- : 0 < (s + t)^-1 by rewrite invr_gt0 addr_gt0.
set y1 : V := _ + _ *: _; set y2 : V := _ - _ *: _.
rewrite (@le_trans _ _ (p (s / (s + t) *: y1 + t / (s + t) *: y2)))//.
set u : V := (X in p X).
have {u y1 y2} -> : u = t / (s + t) *: x1 + s / (s + t) *: x2.
rewrite /u ![_ / _]mulrC -!scalerA -!scalerDr /y1 /y2; congr (_ *: _).
by rewrite !scalerDr addrCA scalerN scalerA (mulrC s) -scalerA addrK.
set l := t / _; set m := s / _.
rewrite [leLHS](_ : _ = l * r1 + m * r2).
by rewrite mulrDl ![_ * _ / _]mulrAC.
apply: ms1; apply: (ls1) => //.
by rewrite -[_ *: _]add0r -[_ * _]add0r; exact: ls1.
rewrite !mulrDl ![_ * _ / _]mulrAC -divD_onem//.
pose st := Itv01 (divDl_ge0 (ltW lt0s) (ltW lt0t))
(divDl_le1 (ltW lt0s) (ltW lt0t)).
exact: (p_cvx st (in_setT y1) (in_setT y2)).
pose Pa :=
[set rSource code | exists x1Source code r1Source code (s1Source code : R), [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]].
pose Pb :=
[set rSource code | exists x1Source code r1Source code (s1Source code : R), [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]].
pose sa := sup Pa. (* We need p with values in a *realType* *)
have Pax : Pa !=set0 by exists (a 0 0 1), 0, 0, 1.
have ubdP : ubound Pa sa.
apply: sup_upper_bound; split => //=.
by exists (b 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; exact: le_a_b.
have saP (uSource code : R) : ubound Pa u -> sa <= u by exact: ge_sup.
pose ib := inf Pb. (* We need P with values in a *realType* *)
have Pbx : Pb !=set0 by exists (b 0 0 1), 0, 0, 1.
have ibdP : lbound Pb ib.
apply: ge_inf; exists (a 0 0 1) => /= x [y [r [s [cry lt0s ->]]]].
exact: le_a_b.
have ibP (uSource code : R) : lbound Pb u -> u <= ib by exact: lb_le_inf Pbx.
have le_sa_ib : sa <= ib.
apply: saP => _ [y [r [l [cry lt0l ->]]]].
by apply: ibP => _ [z [s [m [crz lt0m ->]]]]; exact: le_a_b.
pose alpha := (sa + ib) / 2.
exists alpha => x r l cxr lt0l; split.
- suff : alpha <= b x r l by rewrite (ler_pdivlMr _ _ lt0l) lerBrDl mulrC.
by apply: (le_trans (midf_le le_sa_ib).2); apply: ibdP; exists x, r, l.
- suff : a x r l <= alpha.
by rewrite (ler_pdivrMr _ _ lt0l) lerBlDl -lerBlDr mulrC.
by apply: (le_trans _ (midf_le le_sa_ib).1); apply: ubdP; exists x, r, l.
pose z' := fun kSource code rSource code => exists (v'Source code : V) (r'Source code lambdaSource code : R),
[/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a].
have z'_extends x r : c x r -> z' x r.
by move=> cxr; exists x, r, 0; split; rewrite // ?scale0r ?mul0r ?addr0.
have z'_prol : extend_graph z'.
move=> x.
by exists (val x), (phi x), 0; split; rewrite // ?scale0r ?mul0r ?addr0.
have z'_maj_by_p : le_graph p z'
by move=> x r [w [s [l [cws -> ->]]]]; apply: aP.
have z'_lin : linear_graph z'.
move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]].
rewrite [X in z' X _](_ : _ = w1 + l *: w2 + (m1 + l * m2) *: v).
by rewrite !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA.
rewrite [X in z' _ X](_ : _ = s1 + l * s2 + (m1 + l * m2) * a).
by rewrite !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA.
exists (w1 + l *: w2), (s1 + l * s2), (m1 + l * m2); split => //.
exact: ls1.
have z'_functional : functional_graph z'.
move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]].
have [rw12 erw12] : exists rSource code, c (w1 - w2) r.
by exists (s1 + -1 * s2); rewrite -(scaleN1r w2); exact: ls1.
have h1 (xSource code : V) (rSource code lSource code : R) : x = l *: v -> c x r -> x = 0 /\ l = 0.
move=> -> cxr; have [->|ln0] := eqVneq l 0; first by rewrite scale0r.
suff cvs : c v (l^-1 * r) by absurd: nzv; exists (l^-1 * r).
suff -> : v = l ^-1 *: (l *: v).
by rewrite -(add0r (_ *: _)) -(add0r (_ * _)); exact: ls1.
by rewrite scalerA mulVf ?scale1r.
have [ew12] : w1 - w2 = 0 /\ m2 - m1 = 0.
apply: h1 erw12; rewrite scalerBl.
by apply: subr0_eq; rewrite opprB addrACA e1 -opprD subrr.
suff -> : s1 = s2 by move/subr0_eq => ->.
by apply: fs1 cws2; rewrite -(subr0_eq ew12).
have z'_spec : le_extend_graph z' by [].
exists (ZornType z'_spec) => //=; exists a, 0, 0, 1.
by rewrite !add0r mul1r scale1r.
Qed.
Hypothesis gPSource code : forall zSource code, zornS g z -> z = g.
Let total_gSource code vSource code : exists rSource code, carrier g v r.
Proof.
Lemma hahn_banach_witnessSource code :
exists hSource code : V -> R, forall vSource code rSource code, carrier g v r <-> h v = r.
Proof.
End hahnbanachzorn.
End HahnBanachZornInternal.
Section hahn_banach.
Import LinearGraphInternal.
Import HahnBanachZornInternal.
Context {RSource code : realType} (VSource code : lmodType R) (FSource code : pred V).
Variables (F'Source code : subLmodType F) (fSource code : {linear F' -> R}) (pSource code : V -> R).
Hypothesis p_cvxSource code : @convex_function R V [set: V] p.
Hypothesis f_bounded_by_pSource code : forall zSource code : F', f z <= p (\val z).
Theorem hahn_banach_extensionSource code : exists2 gSource code : {scalar V},
(forall xSource code, g x <= p x) & forall zSource code : F', g (\val z) = f z.
Proof.
pose graphF (vSource code : V) rSource code := exists2 zSource code : F', v = \val z & r = f z.
have [z /(hahn_banach_witness p_cvx)[g gP]] := zornS_ex f_bounded_by_p.
have scalg : linear_for *%R g.
case: z gP => [c [_ ls1 _ _]] /= gP.
have addg : zmod_morphism g.
by move=> w1 w2; apply/gP; apply: lingraphD => //; apply/gP.
suff scalg : scalable_for *%R g.
by move=> a u v; rewrite -gP -(addrC v) -(addrC (g v)); apply/ls1; exact/gP.
by move=> w l; apply/gP; apply: lingraphZ => //; exact/gP.
pose lg := GRing.isLinear.Build _ _ _ _ g scalg.
pose g' : {linear V -> R | *%R} := HB.pack g lg.
exists g'.
by case: z gP => [c [_ _ bp _]] /= gP => x; apply: bp; exact/gP.
by move=> z'; apply/gP; case: z {gP} => [c [_ _ _ pf]] /=; exact: pf.
Qed.
have [z /(hahn_banach_witness p_cvx)[g gP]] := zornS_ex f_bounded_by_p.
have scalg : linear_for *%R g.
case: z gP => [c [_ ls1 _ _]] /= gP.
have addg : zmod_morphism g.
by move=> w1 w2; apply/gP; apply: lingraphD => //; apply/gP.
suff scalg : scalable_for *%R g.
by move=> a u v; rewrite -gP -(addrC v) -(addrC (g v)); apply/ls1; exact/gP.
by move=> w l; apply/gP; apply: lingraphZ => //; exact/gP.
pose lg := GRing.isLinear.Build _ _ _ _ g scalg.
pose g' : {linear V -> R | *%R} := HB.pack g lg.
exists g'.
by case: z gP => [c [_ _ bp _]] /= gP => x; apply: bp; exact/gP.
by move=> z'; apply/gP; case: z {gP} => [c [_ _ _ pf]] /=; exact: pf.
Qed.
End hahn_banach.
Section hahn_banach_normed.
Variable (RSource code : realType) (VSource code : normedModType R) (FSource code : pred V)
(F'Source code : subNormedModType F) (fSource code : {linear_continuous F' -> R}).
Theorem hahn_banach_extension_normedSource code :
exists gSource code : {linear_continuous V -> R}, forall xSource code : F', g (val x) = f x.
Proof.
have [r ltr0 fxrx] : exists2 rSource code, r > 0 & forall zSource code : F', `|f z| <= `|val z| * r.
suff: \forall rSource code \near +oo, forall xSource code : F', `|f x| <= r * `|x|.
move=> [t [_ tf]].
exists (`|t| + 1); first by rewrite ltr_wpDl.
move=> z; rewrite mulrC Num.norm_valE tf//.
by rewrite (le_lt_trans (ler_norm _)) ?ltrDl.
exact/linear_boundedP/continuous_linear_bounded/continuous_fun.
pose p := fun xSource code : V => `|x| * r.
have convp : @convex_function _ _ [set: V] p.
rewrite /convex_function /conv => l v1 v2 _ _ /=.
rewrite [in leRHS]/conv /= /p.
apply: le_trans.
have /ler_pM := ler_normD (l%:num *: v1) (l%:num.~ *: v2).
by apply => //; exact: ltW.
rewrite mulrDl !normrZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//.
by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0.
have : forall zSource code : F', f z <= p (\val z).
by move=> z; rewrite /p (le_trans (ler_norm _)).
move=> /(hahn_banach_extension convp)[g majgp F_eqgf].
have ling : linear (g : V -> R) by exact: linearP.
have contg : continuous (g : V -> R).
move=> x; apply/continuousfor0_continuous/bounded_linear_continuous.
exists r; split; first exact: gtr0_real.
move=> M rM; rewrite nbhs_ballP; exists 1 => //=.
move=> y; rewrite -ball_normE//= sub0r => y1.
rewrite ler_norml; apply/andP; split.
- rewrite lerNl -linearN (le_trans (majgp (- y)))//.
by rewrite /p -(mul1r M) ltW// ltr_pM// ltW.
- by rewrite (le_trans (majgp y))// /p -(mul1r M) -normrN ltW// ltr_pM// ltW.
pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg.
pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg.
by exists g'.
Qed.
suff: \forall rSource code \near +oo, forall xSource code : F', `|f x| <= r * `|x|.
move=> [t [_ tf]].
exists (`|t| + 1); first by rewrite ltr_wpDl.
move=> z; rewrite mulrC Num.norm_valE tf//.
by rewrite (le_lt_trans (ler_norm _)) ?ltrDl.
exact/linear_boundedP/continuous_linear_bounded/continuous_fun.
pose p := fun xSource code : V => `|x| * r.
have convp : @convex_function _ _ [set: V] p.
rewrite /convex_function /conv => l v1 v2 _ _ /=.
rewrite [in leRHS]/conv /= /p.
apply: le_trans.
have /ler_pM := ler_normD (l%:num *: v1) (l%:num.~ *: v2).
by apply => //; exact: ltW.
rewrite mulrDl !normrZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//.
by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0.
have : forall zSource code : F', f z <= p (\val z).
by move=> z; rewrite /p (le_trans (ler_norm _)).
move=> /(hahn_banach_extension convp)[g majgp F_eqgf].
have ling : linear (g : V -> R) by exact: linearP.
have contg : continuous (g : V -> R).
move=> x; apply/continuousfor0_continuous/bounded_linear_continuous.
exists r; split; first exact: gtr0_real.
move=> M rM; rewrite nbhs_ballP; exists 1 => //=.
move=> y; rewrite -ball_normE//= sub0r => y1.
rewrite ler_norml; apply/andP; split.
- rewrite lerNl -linearN (le_trans (majgp (- y)))//.
by rewrite /p -(mul1r M) ltW// ltr_pM// ltW.
- by rewrite (le_trans (majgp y))// /p -(mul1r M) -normrN ltW// ltr_pM// ltW.
pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg.
pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg.
by exists g'.
Qed.
End hahn_banach_normed.
Section hahn_banach_extension_ctvs.
Context {RSource code : realType} {VSource code : convexTvsType R} (FSource code : pred V).
Contrary to the normed case, the extension theorem is not true for any
subtopology on `F`, but only for the finest one.
Import Norm.
A first version specifying the seminorm bounding the function
[Jarchow 7.1.2]
Let $V$ be a real vector space, $F$ a subspace of $V$, and $p \in V^{\#}$
(the set of all sublinear functionals on $V$) and $p$ is a seminorm,
if $f \in F^*$ satisfies $|f| \leq p|_F$, then a $g\in V^*$ exists
such that $g|_F = f$.
Theorem hahn_banach_extension_subctvsSource code (F'Source code : subConvexTvsType F)(fSource code : {linear F' -> R}) :
(exists2 pSource code : SemiNorm.type V,
seminorm_of p & forall zSource code : F', f z <= p (val z)) ->
exists gSource code : {linear_continuous V -> R}, forall xSource code : F', g (val x) = f x.
Proof.
move=> [p ps fp].
have convp : @convex_function _ _ [set: V] p.
rewrite /convex_function /conv => l v1 v2 _ _ /=.
rewrite [in leRHS]/conv /= (le_trans (ler_normD _ _))//.
rewrite !normZ (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~)//.
exact: onem_ge0.
have [g majgp F_eqgf] := @hahn_banach_extension R V _ F' f p convp fp.
have ling : linear (g : V -> R) by exact: linearP.
have contg : continuous (g : V -> R).
by apply/lcfun_seminorm; exists p => //; exact: continuous_seminorm_of.
pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg.
pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg.
by exists g'.
Qed.
have convp : @convex_function _ _ [set: V] p.
rewrite /convex_function /conv => l v1 v2 _ _ /=.
rewrite [in leRHS]/conv /= (le_trans (ler_normD _ _))//.
rewrite !normZ (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~)//.
exact: onem_ge0.
have [g majgp F_eqgf] := @hahn_banach_extension R V _ F' f p convp fp.
have ling : linear (g : V -> R) by exact: linearP.
have contg : continuous (g : V -> R).
by apply/lcfun_seminorm; exists p => //; exact: continuous_seminorm_of.
pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg.
pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg.
by exists g'.
Qed.
A second version where `F` is a subspace of `V`, meaning endowed with
the initial topology w.r.t. to `val`.
[Jarchow, 7.2.1] Let $F$ be a subspace of the lcs $V$. Then every
continuous linear form $f:F\to \mathbb{K}$ extends to a continuous
linear form $g:V\to \mathbb{K}$.
Theorem hahn_banach_extension_initialsubctvsSource code (F'Source code : subLmodType F)(fSource code : {linear_continuous (init_subconvextvs F') -> R^o}) :
exists gSource code : {linear_continuous V -> R}, forall xSource code : F', g (val x) = f x.
Proof.
have [[openBasisV BasisV] _] := has_open_nbhs_basis V.
have [p' ps' fp'] : exists2 pSource code : SemiNorm.type V,
seminorm_of p & forall zSource code : F', f z <= p (val z).
have : continuous (f : init_subconvextvs F' -> R^o) by exact: continuous_fun.
move=> /linear_continuous_seminorm[p [cp ps] /= fp].
have [/= nF [onF pF]] := cp.
have [/(_ nF onF) + _] := basis_opennbhsbasis (init_subconvextvs F').
move=> [oF [[/= oV] ooV oVF] oF0 oFn].
have /BasisV [/= bV obV boV] : nbhs 0 oV.
rewrite nbhsE; exists oV => //; split => //.
apply: (@image_preimage_subset _ _ (val : F'-> V)).
by rewrite oVF; exists 0; rewrite ?linear0.
exists (gauge_fun_basis obV); first by exists bV, obV.
move=> z.
set pVz := (leRHS).
apply: le_trans; first exact: fp.
rewrite pF; apply: inf_le.
- move=> x /= [r [r0]] /set_mem[v bVv rvalz] <-.
exists (- r); split => //; exists r; split => //.
rewrite inE; exists (r^-1 *: z).
apply: oFn; rewrite -oVF /=; apply: boV.
by rewrite linearZ/= -rvalz scalerA mulVf ?scale1r ?gt_eqF.
by rewrite scalerA divff ?scale1r ?gt_eqF.
- have [/= s s0 szbV]:= absorbing_opennbhsbasis obV (val z).
exists s^-1; split; rewrite ?invr_gt0// inE /=.
exists (s *: val z); first exact/set_mem.
by rewrite scalerA mulVf ?scale1r// gt_eqF.
- split; last by exists 0 => r [? _]; rewrite ltW.
have [/= s s0 sznF]:= absorbing_opennbhsbasis onF z.
exists s^-1; split; rewrite ?invr_gt0// inE /=.
exists (s *: z); first exact/set_mem.
by rewrite scalerA mulVf ?scale1r// gt_eqF.
(* apply the previous thm but typing or... *)
have convp : @convex_function _ _ [set: V] p'.
rewrite /convex_function /conv => l v1 v2 _ _ /=.
rewrite [in leRHS]/conv /= (le_trans (ler_normD _ _))//.
by rewrite !normZ (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~)// onem_ge0.
have [g majgp F_eqgf] := @hahn_banach_extension R V _ F' f p' convp fp'.
have ling : linear (g : V -> R) by exact: linearP.
have contg : continuous (g : V -> R).
by apply/lcfun_seminorm; exists p' => //; exact: continuous_seminorm_of.
pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg.
pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg.
by exists g'.
Qed.
have [p' ps' fp'] : exists2 pSource code : SemiNorm.type V,
seminorm_of p & forall zSource code : F', f z <= p (val z).
have : continuous (f : init_subconvextvs F' -> R^o) by exact: continuous_fun.
move=> /linear_continuous_seminorm[p [cp ps] /= fp].
have [/= nF [onF pF]] := cp.
have [/(_ nF onF) + _] := basis_opennbhsbasis (init_subconvextvs F').
move=> [oF [[/= oV] ooV oVF] oF0 oFn].
have /BasisV [/= bV obV boV] : nbhs 0 oV.
rewrite nbhsE; exists oV => //; split => //.
apply: (@image_preimage_subset _ _ (val : F'-> V)).
by rewrite oVF; exists 0; rewrite ?linear0.
exists (gauge_fun_basis obV); first by exists bV, obV.
move=> z.
set pVz := (leRHS).
apply: le_trans; first exact: fp.
rewrite pF; apply: inf_le.
- move=> x /= [r [r0]] /set_mem[v bVv rvalz] <-.
exists (- r); split => //; exists r; split => //.
rewrite inE; exists (r^-1 *: z).
apply: oFn; rewrite -oVF /=; apply: boV.
by rewrite linearZ/= -rvalz scalerA mulVf ?scale1r ?gt_eqF.
by rewrite scalerA divff ?scale1r ?gt_eqF.
- have [/= s s0 szbV]:= absorbing_opennbhsbasis obV (val z).
exists s^-1; split; rewrite ?invr_gt0// inE /=.
exists (s *: val z); first exact/set_mem.
by rewrite scalerA mulVf ?scale1r// gt_eqF.
- split; last by exists 0 => r [? _]; rewrite ltW.
have [/= s s0 sznF]:= absorbing_opennbhsbasis onF z.
exists s^-1; split; rewrite ?invr_gt0// inE /=.
exists (s *: z); first exact/set_mem.
by rewrite scalerA mulVf ?scale1r// gt_eqF.
(* apply the previous thm but typing or... *)
have convp : @convex_function _ _ [set: V] p'.
rewrite /convex_function /conv => l v1 v2 _ _ /=.
rewrite [in leRHS]/conv /= (le_trans (ler_normD _ _))//.
by rewrite !normZ (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~)// onem_ge0.
have [g majgp F_eqgf] := @hahn_banach_extension R V _ F' f p' convp fp'.
have ling : linear (g : V -> R) by exact: linearP.
have contg : continuous (g : V -> R).
by apply/lcfun_seminorm; exists p' => //; exact: continuous_seminorm_of.
pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg.
pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg.
by exists g'.
Qed.
End hahn_banach_extension_ctvs.