From 65e2002f618c2b7968f72bf6ebd4b94c5c251b3f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 11 Mar 2026 13:50:27 +0900 Subject: [PATCH 01/11] generalization Co-authored-by: Marie Kerjean --- theories/normedtype_theory/pseudometric_normed_Zmodule.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 687d6f3f6..8cfbf80bf 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -11,7 +11,7 @@ From mathcomp Require Import prodnormedzmodule num_normedtype. (* *) (* This directory (`normed_theory`) file extends the topological hierarchy *) (* with norm-related notions. Note that balls in `topology_theory` are not *) -(* necessarily open, here they are. *) +(* necessarily ope, here they are. *) (* *) (* ## Helper functions *) (* To be used in `normed_module.v`. *) From 3932450d2cdd7dd6a257c6da56685fb8c3e7b3ce Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 11 Mar 2026 13:54:28 +0900 Subject: [PATCH 02/11] fix --- theories/normedtype_theory/pseudometric_normed_Zmodule.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 8cfbf80bf..687d6f3f6 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -11,7 +11,7 @@ From mathcomp Require Import prodnormedzmodule num_normedtype. (* *) (* This directory (`normed_theory`) file extends the topological hierarchy *) (* with norm-related notions. Note that balls in `topology_theory` are not *) -(* necessarily ope, here they are. *) +(* necessarily open, here they are. *) (* *) (* ## Helper functions *) (* To be used in `normed_module.v`. *) From c7d9ec4fe80b0b3a6ca49eb29583bbdb980f8e23 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Mar 2026 12:24:49 +0900 Subject: [PATCH 03/11] convex_function generalized Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 4 ++++ theories/convex.v | 5 +++-- theories/hoelder.v | 7 ++++--- 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0366d7f63..ba6a10d84 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -229,6 +229,7 @@ + lemma `cvg_comp_shift` + lemma `ball_open_nbhs` + ### Renamed - in `topology_structure.v` @@ -273,6 +274,9 @@ + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`, `integral_itv_bndoo` +- in `convex.v`: + + definition `convex_function` (from a realType as domain to a convex_lmodType as domain) + ### Deprecated - in `lebesgue_integral_nonneg.v`: diff --git a/theories/convex.v b/theories/convex.v index 66a143d7e..c050e7834 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -220,7 +220,8 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed. End conv_numDomainType. -Definition convex_function (R : realType) (D : set R) (f : R -> R^o) := + +Definition convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) := forall (t : {i01 R}), - {in D &, forall (x y : R^o), (f (x <| t |> y) <= f x <| t |> f y)%R}. + {in D &, forall (x y : E'), (f (x <| t |> y) <= f x <| t |> f y)%R}. (* TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) *) diff --git a/theories/hoelder.v b/theories/hoelder.v index 096f55960..16cfdc741 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -532,13 +532,14 @@ End hoelder2. Section convex_powR. Context {R : realType}. Local Open Scope ring_scope. +Local Open Scope convex_scope. Lemma convex_powR p : 1 <= p -> - convex_function `[0, +oo[%classic (@powR R ^~ p). + convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p). Proof. move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0. -have p0 : 0 < p by rewrite (lt_le_trans _ p1). -rewrite !convRE; set w1 := t%:num; set w2 := t%:inum.~. +have p0 : 0 < p by rewrite (lt_le_trans _ p1). +rewrite convRE [X in X `^ _ <= _]convRE; set w1 := t%:num; set w2 := t%:inum.~. have [->|w20] := eqVneq w2 0. rewrite !mul0r !addr0; have [->|w10] := eqVneq w1 0. by rewrite !mul0r powR0// gt_eqF. From 640b0ca0016c369e01883a9271ba5913c668d890 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 6 Mar 2026 14:10:06 +0900 Subject: [PATCH 04/11] mv convex --- CHANGELOG_UNRELEASED.md | 5 +++ theories/convex.v | 16 ++++++++ theories/normedtype_theory/normed_module.v | 30 +++++++++------ theories/normedtype_theory/tvs.v | 44 +++++++++++++--------- 4 files changed, 66 insertions(+), 29 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ba6a10d84..ccddc1f28 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -72,6 +72,9 @@ - in `derive.v`: + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV` +- in `convex.v`: + + lemma `convexW` + ### Changed - in `constructive_ereal.v`: fixed the infamous `%E` scope bug. @@ -229,6 +232,8 @@ + lemma `cvg_comp_shift` + lemma `ball_open_nbhs` +- moved from `tvs.v` to `convex.v` + + definition `convex` ### Renamed diff --git a/theories/convex.v b/theories/convex.v index c050e7834..d44cadc1c 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -220,6 +220,22 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed. End conv_numDomainType. +Definition convex (R : numDomainType) (M : lmodType R) + (A : set (convex_lmodType M)) := + forall x y lambda, x \in A -> y \in A -> x <| lambda |> y \in A. + +Lemma convexW (R : numDomainType) (M : lmodType R) (A : set (convex_lmodType M)) : + convex A <-> + {in A &, forall x y (k : {i01 R}), 0 < k%:num -> k%:num < 1 -> x <| k |> y \in A}. +Proof. +split => [cA x y xA yA k k0 k1|cA x y l xA yA]. + by have /(_ k) := cA _ _ _ xA yA. +have [->|l0] := eqVneq l 0%:i01; first by rewrite conv0. +have [->|l1] := eqVneq l 1%:i01; first by rewrite conv1. +apply: cA => //. +- by rewrite lt_neqAle eq_sym l0 ge0. +- by rewrite lt_neqAle l1 le1. +Qed. Definition convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) := forall (t : {i01 R}), diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 9ccf4583a..e6bb58265 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -7,7 +7,7 @@ From mathcomp Require Import interval_inference fieldext falgebra. From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets filter functions cardinality. From mathcomp Require Import set_interval ereal reals topology real_interval. -From mathcomp Require Import prodnormedzmodule tvs num_normedtype. +From mathcomp Require Import convex prodnormedzmodule tvs num_normedtype. From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. (**md**************************************************************************) @@ -111,21 +111,27 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//. by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0. Unshelve. all: by end_near. Qed. +Local Open Scope convex_scope. + (** NB: we have almost the same proof in `tvs.v` *) Let locally_convex : - exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B. -Proof. -exists [set B | exists x r, B = ball x r]. - move=> b; rewrite inE /= => [[x]] [r] -> z y l. - rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1. - have -> : x = l *: x + (1 - l) *: x by rewrite addrC scalerBl subrK scale1r. - rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first. + exists2 B : set (set (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B. +Proof. +exists [set B | exists (x : convex_lmodType V) r, B = ball x r]. + move=> b; rewrite inE => [[x]] [r] ->. + apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. + have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *) + rewrite /ball_/= inE/=. + rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType V) <| l |> + (x - y : convex_lmodType V)); last first. by rewrite opprD addrACA -scalerBr -scalerBr. - rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//. + rewrite (@le_lt_trans _ _ ((l%:num) * `|x - z| + l%:num.~ * `|x - y|))//. + rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//. + rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//. by rewrite -!normrZ ler_normD. - rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//. - by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF// ltW. - by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r. + rewrite (@lt_le_trans _ _ (l%:num * r + l%:num.~ * r ))//. + by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF ?ltW// subr_gt0. + by rewrite -mulrDl addrC subrK mul1r. split; first by move=> B [x] [r] ->; exact: ball_open. move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index c67224749..c96daf9db 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -2,8 +2,10 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector. From mathcomp Require Import interval_inference. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import set_interval reals topology num_normedtype. +From mathcomp Require Import convex set_interval reals topology num_normedtype. From mathcomp Require Import pseudometric_normed_Zmodule. (**md**************************************************************************) @@ -306,10 +308,6 @@ HB.instance Definition _ := HB.end. -Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := - forall x y (lambda : R), x \in A -> y \in A -> - 0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A. - HB.mixin Record Uniform_isTvs (R : numDomainType) E & Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set (set E), @@ -511,20 +509,30 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//. by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0. Unshelve. all: by end_near. Qed. +Local Open Scope convex_scope. + Let standard_locally_convex : exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B. Proof. exists [set B | exists x r, B = ball x r]. - move=> b; rewrite inE /= => [[x]] [r] -> z y l. - rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1. - have -> : x = l *: x + (1 - l) *: x by rewrite addrC scalerBl subrK scale1r. - rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first. - by rewrite opprD addrACA -scalerBr -scalerBr. - rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//. - by rewrite -!normrM ler_normD. - rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//. - by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF// ltW. - by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r. + move=> b/= /[!inE]/= [[x]] [r] ->. + apply/convexW => z y; rewrite /ball/= !inE/= => zx yx l /[!inE]/= l0 l1. + (* conv lemma? *) + have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *) + rewrite [X in `|X|](_ : _ = (x - z) <| l |> (x - y)); last first. + by rewrite opprD addrACA -mulrBr -mulrBr. + rewrite (@le_lt_trans _ _ ((`|x - z| : R^o) <| l |> `|x - y|))//. + rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//. + rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//. + rewrite [X in `|X| <= _](_ : _ = l%:num * (x - z) + l%:num.~ * (x - y))//. + rewrite -[X in _ <= X + _]normrM. + rewrite -[X in _ <= _ + X]normrM. + by rewrite ler_normD. + rewrite (@lt_le_trans _ _ ((r : R^o) <| l |> r))//. + rewrite ltr_leD//. + by rewrite ltr_pM2l// normr_gt0// gt_eqF. + by rewrite ler_wpM2l// ?subr_ge0// ltW. + by rewrite convmm. split; first by move=> B [x] [r] ->; exact: ball_open. move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. @@ -582,8 +590,10 @@ have : basis B. rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo. by exists b => //; split => // []; exact: Bfo. exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-. -move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1. -by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE]. +move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2]. +split. + by apply/set_mem/Bcb; [exact/mem_set|exact/mem_set|exact/mem_set]. +by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set]. Qed. HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build From 3e26e7b12fa86557e20522b27d5050971fe9c1a0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 11 Mar 2026 13:16:20 +0900 Subject: [PATCH 05/11] simplification --- theories/normedtype_theory/normed_module.v | 27 +++++++++--------- theories/normedtype_theory/tvs.v | 33 +++++++++------------- 2 files changed, 27 insertions(+), 33 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index e6bb58265..9e69097fa 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -113,25 +113,24 @@ Unshelve. all: by end_near. Qed. Local Open Scope convex_scope. +Let ball_convex (x : convex_lmodType V) (r : K) : convex (ball x r). +Proof. +apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. +rewrite inE/=. +rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |> + (x - y : convex_lmodType _)); last first. + by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr. +rewrite (le_lt_trans (ler_normD _ _))// !normrZ. +rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//. +by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0. +Qed. + (** NB: we have almost the same proof in `tvs.v` *) Let locally_convex : exists2 B : set (set (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B. Proof. exists [set B | exists (x : convex_lmodType V) r, B = ball x r]. - move=> b; rewrite inE => [[x]] [r] ->. - apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. - have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *) - rewrite /ball_/= inE/=. - rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType V) <| l |> - (x - y : convex_lmodType V)); last first. - by rewrite opprD addrACA -scalerBr -scalerBr. - rewrite (@le_lt_trans _ _ ((l%:num) * `|x - z| + l%:num.~ * `|x - y|))//. - rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//. - rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//. - by rewrite -!normrZ ler_normD. - rewrite (@lt_le_trans _ _ (l%:num * r + l%:num.~ * r ))//. - by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF ?ltW// subr_gt0. - by rewrite -mulrDl addrC subrK mul1r. + by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex. split; first by move=> B [x] [r] ->; exact: ball_open. move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index c96daf9db..2a1800050 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -511,31 +511,26 @@ Unshelve. all: by end_near. Qed. Local Open Scope convex_scope. +Let standard_ball_convex (x : R^o) (r : R) : convex (ball x r). +Proof. +apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. +rewrite inE/=. +rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |> + (x - y : convex_lmodType _)); last first. + by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr. +rewrite (le_lt_trans (ler_normD _ _))// !normrM. +rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//. +by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0. +Qed. + Let standard_locally_convex : exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B. Proof. exists [set B | exists x r, B = ball x r]. - move=> b/= /[!inE]/= [[x]] [r] ->. - apply/convexW => z y; rewrite /ball/= !inE/= => zx yx l /[!inE]/= l0 l1. - (* conv lemma? *) - have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *) - rewrite [X in `|X|](_ : _ = (x - z) <| l |> (x - y)); last first. - by rewrite opprD addrACA -mulrBr -mulrBr. - rewrite (@le_lt_trans _ _ ((`|x - z| : R^o) <| l |> `|x - y|))//. - rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//. - rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//. - rewrite [X in `|X| <= _](_ : _ = l%:num * (x - z) + l%:num.~ * (x - y))//. - rewrite -[X in _ <= X + _]normrM. - rewrite -[X in _ <= _ + X]normrM. - by rewrite ler_normD. - rewrite (@lt_le_trans _ _ ((r : R^o) <| l |> r))//. - rewrite ltr_leD//. - by rewrite ltr_pM2l// normr_gt0// gt_eqF. - by rewrite ler_wpM2l// ?subr_ge0// ltW. - by rewrite convmm. + by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex. split; first by move=> B [x] [r] ->; exact: ball_open. move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. -by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. +by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. Qed. HB.instance Definition _ := From f790135a5de3bcb7be8b677aa678c6988abdac50 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 11 Mar 2026 16:34:44 +0900 Subject: [PATCH 06/11] fix CI --- theories/normedtype_theory/normed_module.v | 3 ++- theories/normedtype_theory/tvs.v | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 9e69097fa..3e1e925e9 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -122,7 +122,8 @@ rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |> by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr. rewrite (le_lt_trans (ler_normD _ _))// !normrZ. rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//. -by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0. +rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl. +by rewrite ltrD// ltr_pM2l// onem_gt0. Qed. (** NB: we have almost the same proof in `tvs.v` *) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 2a1800050..8fbd1dd55 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -520,7 +520,8 @@ rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |> by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr. rewrite (le_lt_trans (ler_normD _ _))// !normrM. rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//. -by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0. +rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl. +by rewrite ltrD// ltr_pM2l// onem_gt0. Qed. Let standard_locally_convex : From 58897ba589a884ddef351a01f331198fe28e5ca5 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Mar 2026 15:11:02 +0900 Subject: [PATCH 07/11] hahn_banach thm file --- _CoqProject | 2 + theories/Make | 2 + theories/hahn_banach_theorem.v | 716 +++++++++++++++++++++++++++++++++ 3 files changed, 720 insertions(+) create mode 100644 theories/hahn_banach_theorem.v diff --git a/_CoqProject b/_CoqProject index 8b90d4861..182e2ecd8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -87,6 +87,8 @@ theories/normedtype_theory/urysohn.v theories/normedtype_theory/vitali_lemma.v theories/normedtype_theory/normedtype.v +theories/hahn_banach_theorem.v + theories/sequences.v theories/realfun.v theories/exp.v diff --git a/theories/Make b/theories/Make index 75ab71c74..cc3ad18fd 100644 --- a/theories/Make +++ b/theories/Make @@ -53,6 +53,8 @@ normedtype_theory/urysohn.v normedtype_theory/vitali_lemma.v normedtype_theory/normedtype.v +hahn_banach_theorem.v + realfun.v sequences.v exp.v diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v new file mode 100644 index 000000000..8258fecb7 --- /dev/null +++ b/theories/hahn_banach_theorem.v @@ -0,0 +1,716 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import interval_inference. +From mathcomp Require Import unstable wochoice boolp classical_sets topology reals. +From mathcomp Require Import filter reals normedtype convex. +Import numFieldNormedType.Exports. +Local Open Scope classical_set_scope. + +(* Marie's proposal: encode the "partial" properties by reasoning on + the graph of functions. The other option would be to study a partial + order defined on subsets of the ambiant space V, on which it is possible + to obtain a bounded lineEar form extending f. But this options seems much + less convenient, in particular when establishing that one can extend f + on a space with one more dimension. Indeed, exhibiting a term of type + V -> R requires a case ternary analysis on F, the new line, and an + explicit direct sum to ensure the definition is exhaustive. Working with + graphs allows to leave this argument completely implicit. *) + + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + + + + +Local Open Scope ring_scope. +Local Open Scope convex_scope. + Import GRing.Theory. + Import Num.Theory. + +Section SetPredRels. + + Variables T U : Type. + Implicit Types f g : T -> U -> Prop. + (* Functional (possibly empty or partial) graphs *) + Definition functional f := + forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. + +End SetPredRels. + + +Section OrderRels. + + Variable (R : numDomainType). + + (* Upper bound *) + Definition ubd (s : set R) (a : R) := forall x, s x -> x <= a. + + (* Lower bound *) + Definition ibd (s : set R) (a : R) := forall x, s x -> a <= x. + + (* the intension is that f is the graph of a function bounded by p *) + Definition maj_by T p (f : T -> R -> Prop) := + forall v r, f v r -> r <= p v. + + End OrderRels. + + + Section LinAndCvx. + + Variables (R : numDomainType) (V : lmodType R). + (* + Check convex_function. + Definition convex_function (p : V -> R) := forall v1 v2 l m, + ( 0 <= l /\ 0 <= m) -> l + m = 1 -> p (l *: v1 + m *: v2) <= l * (p v1) + m * (p v2). + *) + + Definition linear_rel (f : V -> R -> Prop) := + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + + Variable f : V -> R -> Prop. + Hypothesis lrf : linear_rel f. + + Lemma linrel_00 x r : f x r -> f 0 0. + Proof. + suff -> : f 0 0 = f (x + (-1) *: x) (r + (-1) * r) by move=> h; apply: lrf. + by rewrite scaleNr mulNr mul1r scale1r !subrr. + Qed. + + Lemma linrel_scale x r l : f x r -> f (l *: x) (l * r). + Proof. + move=> fxr. + have -> : f (l *: x) (l * r) = f (0 + l *: x) (0 + l * r) by rewrite !add0r. + by apply: lrf=> //; apply: linrel_00 fxr. + Qed. + + Lemma linrel_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2)(r1 - r2). + Proof. + have -> : x1 - x2 = x1 + (-1) *: x2 by rewrite scaleNr scale1r. + have -> : r1 - r2 = r1 + (-1) * r2 by rewrite mulNr mul1r. + by apply: lrf. + Qed. + + + Definition add_line f w a := fun v r => + exists v' : V, exists r' : R, exists lambda : R, + [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. + + End LinAndCvx. + + + Section HBPreparation. + + Variables (R : realFieldType) (V : lmodType R). + + Variables (F : set V) (phi : V -> R) (p : V -> R). + +Hypothesis linphiF : forall v1 v2 l, F v1 -> F v2 -> + phi (v1 + l *: v2) = phi v1 + l * (phi v2). + Implicit Types (f g : V -> R -> Prop). + +Hypothesis F0 : F 0. + +Fact phi0 : phi 0 = 0. +Proof. +have -> : 0 = 0 + (-1) *: 0 :> V by rewrite scaler0 addr0. +by rewrite linphiF // mulN1r addrN. +Qed. + +About convex_function. +Hypothesis p_cvx : (@convex_function R V [set: V] p). + + Hypothesis sup : forall (A : set R) (a m : R), + A a -> ubd A m -> + {s : R | ubd A s /\ forall u, ubd A u -> s <= u}. + + Hypothesis inf : forall (A : set R) (a m : R), + A a -> ibd A m -> + {s : R | ibd A s /\ forall u, ibd A u -> u <= s}. + + (* f is a subset of (V x R), if v is in pi_1 f, then (v, phi v) is in f. + Otherwise said, the graph of phi restructed to pi_1 f is included in f*) + + Definition prol f := forall v, F v -> f v (phi v). + + Definition spec (f : V -> R -> Prop) := + [/\ functional f, linear_rel f, maj_by p f & prol f]. + + Record zorn_type : Type := ZornType + {carrier : V -> R -> Prop; specP : spec carrier}. + + Hypothesis spec_phi : spec (fun v r => F v /\ r = phi v). + + Definition zphi := ZornType spec_phi. + + Lemma zorn_type_eq z1 z2 : carrier z1 = carrier z2 -> z1 = z2. + Proof. + case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; move: pm1 pm2; rewrite e => pm1 pm2. + by congr ZornType; apply: Prop_irrelevance. + Qed. + + Definition zorn_rel (z1 z2 : zorn_type):= forall x y, (carrier z1 x y) -> (carrier z2 x y ). + + (* Zorn applied to the relation of extending the graph of the first function *) + Lemma zorn_rel_ex : exists g : zorn_type, forall z, zorn_rel g z -> z = g. + Proof. + pose Rbool := (fun x y => `[< zorn_rel x y >]). + have RboolP : forall z t, Rbool z t <-> zorn_rel z t by split; move => /asboolP //=. + suff [t st]: exists t : zorn_type, forall s : zorn_type, Rbool t s -> s = t. + by exists t; move => z /RboolP tz; apply: st. + apply: (@Zorn zorn_type Rbool). + - by move => t; apply/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. + case: (lem (exists a, A a)) => [[w Aw] | eA]; last first. + by exists zphi => a Aa; elim: eA; exists a. + (* g is the union of the graphs indexed by elements in a *) + pose g v r := exists a, A a /\ (carrier a v r). + have g_fun : functional g. + move=> v r1 r2 [a [Aa avr1]] [b [Ab bvr2]]. + have [] : Rbool a b \/ Rbool b a by exact: Amax. + - rewrite /Rbool /RboolP /zorn_rel; case: b Ab bvr2 {Aa}. + move => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2. + by move/ecas2: avr1 => /fs2 /(_ s2vr2). + - rewrite /Rbool /RboolP /zorn_rel; case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1. + by move/ecbs1: bvr2; apply: fs1. + have g_lin : linear_rel g. + move=> v1 v2 l r1 r2 [a1 [Aa1 c1]] [a2 [Aa2 c2]]. + have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2. + - have {c1 sc12 Aa1 a1} c1 : carrier a2 v1 r1 by apply: sc12. + exists a2; split=> //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl. + - have {c2 sc21 Aa2 a2} c2 : carrier a1 v2 r2 by apply: sc21. + exists a1; split=> //; case: a1 {Aa1} c2 c1 => c /= [_ hl _ _] *; exact: hl. + have g_majp : maj_by p g by move=> v r [[c [fs1 ls1 ms1 ps1]]] /= [_ /ms1]. + have g_prol : prol g. + move=> *; exists w; split=> //; case: w Aw => [c [_ _ _ hp]] _ //=; exact: hp. + have spec_g : spec g by split. + pose zg := ZornType spec_g. + by exists zg => [a Aa]; apply/RboolP; rewrite /zorn_rel => v r cvr; exists a. + Qed. + + + Variable g : zorn_type. + + Hypothesis gP : forall z, zorn_rel g z -> z = g. + + (*The next lemma proves that when z is of zorn_type, it can be extended on any + real line directed by an arbitrary vector v *) + + Lemma divDl_ge0 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : 0 <= s / (s +t). + Admitted. + + Lemma divDl_le1 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : s / (s +t) <= 1. + Admitted. + + Lemma divD_onem (s t : R) : (s / (s + t)).~ = t / (s + t). + Admitted. + + Lemma domain_extend (z : zorn_type) v : + exists2 ze : zorn_type, (zorn_rel z ze) & (exists r, (carrier ze) v r). + Proof. + case: (lem (exists r, (carrier z v r))). + by case=> r rP; exists z => //; exists r. + case: z => [c [fs1 ls1 ms1 ps1]] /= nzv. + have c00 : c 0 0. + rewrite -phi0; exact: ps1. + have [a aP] : exists a, forall (x : V) (r lambda : R), + c x r -> r + lambda * a <= p (x + lambda *: v). + suff [a aP] : exists a, forall (x : V) (r lambda : 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 cxr. + have {aP} aP := aP _ _ _ cxr. + case: (ltrgt0P lambda) ; [by case/aP | move=> ltl0 | move->]; last first. + by rewrite mul0r scale0r !addr0; apply: ms1. + rewrite -[lambda]opprK scaleNr mulNr. + have /aP [] : 0 < - lambda by rewrite oppr_gt0. + done. + pose b (x : V) r lambda : R := (p (x + lambda *: v) - r) / lambda. + pose a (x : V) r lambda : R := (r - p (x - lambda *: v)) / lambda. + have le_a_b x1 x2 r1 r2 s t : 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 // mulrC [_ * s]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 := _ - _ *: _. + set rhs := (X in _ <= X). + have step1 : p (s / (s + t) *: y1 + t / (s + t) *: y2) <= rhs. + rewrite /rhs !mulrDl ![_ * _ / _]mulrAC. + pose st := Itv01 (divDl_ge0 (ltW lt0s) (ltW lt0t)) ((divDl_le1 (ltW lt0s) (ltW lt0t))). + move: (p_cvx st (in_setT y1) (in_setT y2)). + by rewrite /conv /= [X in ((_ <= X)-> _)]/conv /= divD_onem /=. + apply: le_trans step1 => {rhs}. + 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 [s * t]mulrC -scalerA addrK. + set l := t / _; set m := s / _; set lhs := (X in X <= _). + have {lhs} -> : lhs = l * r1 + m * r2. + by rewrite /lhs mulrDl ![_ * _ / _]mulrAC. + apply: ms1; apply: (ls1) => //. + rewrite -[_ *: _]add0r -[_ * _] add0r; apply: ls1 => //. + pose Pa : set R := fun r => exists x1, exists r1, exists s1, + [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]. + pose Pb : set R := fun r => exists x1, exists r1, exists s1, + [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]. + have exPa : Pa (a 0 0 1) by exists 0; exists 0; exists 1; split. + have exPb : Pb (b 0 0 1) by exists 0; exists 0; exists 1; split. + have majPa x : Pa x -> x <= b 0 0 1. + move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have minPb x : Pb x -> a 0 0 1 <= x. + move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have [sa [ubdP saP]]:= sup exPa majPa; have [ib [ibdP ibP]]:= inf exPb minPb. + have le_sa_ib : sa <= ib. + apply: saP=> r' [y [r [l [cry lt0l -> {r'}]]]]. + apply: ibP=> s' [z [s [m [crz lt0m -> {s'}]]]]; exact: le_a_b. + pose alpha := ((sa + ib) / 2%:R). + have le_alpha_ib : alpha <= ib by rewrite /alpha midf_le. + have le_sa_alpha : sa <= alpha by rewrite /alpha midf_le. + exists alpha => x r l cxr lt0l; split. + - suff : alpha <= b x r l. + by rewrite /b; move/ler_pdivlMr: lt0l->; rewrite lerBrDl mulrC. + by apply: le_trans le_alpha_ib _; apply: ibdP; exists x; exists r; exists l. + - suff : a x r l <= alpha. + rewrite /a. move/ler_pdivrMr: lt0l->. + by rewrite lerBlDl -lerBlDr mulrC. + by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l. + pose z' := add_line c v a. + have z'_extends : forall v r, c v r -> z' v r. + move=> x r cxr; exists x; exists r; exists 0; split=> //. + - by rewrite scale0r addr0. + - by rewrite mul0r addr0. + have z'_prol : prol z'. + move=> x /ps1 cxphix; exists x; exists (phi x); exists 0; split=> //. + - by rewrite scale0r addr0. + - by rewrite mul0r addr0. + - have z'_maj_by_p : maj_by p z'. + by move=> x r [w [s [l [cws -> ->]]]]; apply: aP. + - have z'_lin : linear_rel z'. + move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]]. + set w := (X in z' X _); set s := (X in z' _ X). + have {w} -> : w = w1 + l *: w2 + (m1 + l * m2) *: v. + by rewrite /w !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA. + have {s} -> : s = s1 + l * s2 + (m1 + l * m2) * a. + by rewrite /s !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA. + exists (w1 + l *: w2); exists (s1 + l * s2); exists (m1 + l * m2); split=> //. + exact: ls1. + - have z'_functional : functional z'. + move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]]. + have h1 (x : V) (r l : R) : x = l *: v -> c x r -> x = 0 /\ l = 0. + move=> -> cxr; case: (l =P 0) => [-> | /eqP ln0]; first by rewrite scale0r. + suff cvs: c v (l^-1 * r) by elim:nzv; exists (l^-1 * r). + suff -> : v = l ^-1 *: (l *: v) by exact: linrel_scale. + by rewrite scalerA mulVf ?scale1r. + have [rw12 erw12] : exists r, c (w1 - w2) r. + exists (s1 + (-1) * s2). + have -> : w1 - w2 = w1 + (-1) *: w2 by rewrite scaleNr scale1r. + by apply: ls1. + have [ew12 /eqP]: w1 - w2 = 0 /\ (m2 - m1 = 0). + apply: h1 erw12; rewrite scalerBl; apply/eqP; rewrite subr_eq addrC addrA. + by rewrite -subr_eq opprK e1. + suff -> : s1 = s2 by rewrite subr_eq0=> /eqP->. + by apply: fs1 cws2; move/eqP: ew12; rewrite subr_eq0=> /eqP<-. + have z'_spec : spec z' by split. + pose zz' := ZornType z'_spec. + exists zz'; rewrite /zorn_rel => //=; exists a; exists 0; exists 0; exists 1. + by rewrite add0r mul1r scale1r add0r; split. + Qed. + + Lemma tot_g v : exists r, carrier g v r. + Proof. + have [z /gP sgz [r zr]]:= domain_extend g v. + by exists r; rewrite -sgz. + Qed. + + +Lemma hb_witness : exists h : V -> R, forall v r, carrier g v r <-> (h v = r). +Proof. +move: (choice tot_g) => [h hP]; exists h => v r; split; last by move<-. +case: g gP tot_g hP => c /= [fg lg mg pg] => gP' tot_g' hP cvr. +by have -> // := fg v r (h v). +Qed. + + + End HBPreparation. + + + Section HahnBanachold. +(* Now we prove HahnBanach on functions*) +(* We consider R a real (=ordered) field with supremum, and V a (left) module + on R. We do not make use of the 'vector' interface as the latter enforces + finite dimension. *) + +Variables (R : realFieldType) (V : lmodType R). + +Hypothesis sup : forall (A : set R) (a m : R), + A a -> ubd A m -> + {s : R | ubd A s /\ forall u, ubd A u -> s <= u}. + +(* This could be obtained from sup but we are lazy here *) +Hypothesis inf : forall (A : set R) (a m : R), + A a -> ibd A m -> + {s : R | ibd A s /\ forall u, ibd A u -> u <= s}. + +Variables (F : pred V) (f : V -> R) (p : V -> R). + +(* MathComp seems to lack of an interface for submodules of V, so for now + we state "by hand" that F is closed under linear combinations. *) +Hypothesis F0 : F 0. +Hypothesis linF : forall v1 v2 l, F v1 -> F v2 -> F (v1 + l *: v2). + +Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> + f (v1 + l *: v2) = f v1 + l * (f v2). + +Hypothesis p_cvx : (@convex_function R V [set: V] p). + +Hypothesis f_bounded_by_p : forall x, F x -> f x <= p x. + +Theorem HahnBanachold : exists g : {scalar V}, + (forall x, g x <= p x) /\ (forall x, F x -> g x = f x). +pose graphF v r := F v /\ r = f v. +have func_graphF : functional graphF by move=> v r1 r2 [Fv ->] [_ ->]. +have lin_graphF : linear_rel graphF. + move=> v1 v2 l r1 r2 [Fv1 ->] [Fv2 ->]; split; first exact: linF. + by rewrite linfF. +have maj_graphF : maj_by p graphF by move=> v r [Fv ->]; exact: f_bounded_by_p. + +have prol_graphF : prol F f graphF by move=> v Fv; split. +have graphFP : spec F f p graphF by split. +have [z zmax]:= zorn_rel_ex graphFP. +pose FP v : Prop := F v. +have FP0 : FP 0 by []. +have [g gP]:= (hb_witness linfF FP0 p_cvx sup inf graphFP zmax). +have scalg : linear_for *%R g. + case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. + have addg : additive g. + move=> w1 w2; apply/gP. + apply: linrel_add. + exact ls1. + by apply /gP. + by apply /gP. + suff scalg : scalable_for *%R g. + move=> a u v. + rewrite -gP. + rewrite (addrC _ v). + rewrite (addrC _ (g v)). + apply: ls1. + by apply /gP. + by apply /gP. + by move=> w l; apply/gP; apply: linrel_scale=> //; apply/gP. +pose H := GRing.isLinear.Build _ _ _ _ g scalg. +pose g' : {linear V -> R | *%R} := HB.pack g H. +exists g'. +have grxtf v : F v -> g v = f v. + move=> Fv; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf. + suff pmajg v : g v <= p v by split. + by case: z {zmax} gP => [c [_ _ bp _]] /= gP; apply/bp/gP. +Qed. + +End HahnBanachold. + + + +Section HahnBanachnew. +(* Now we prove HahnBanach on functions*) +(* We consider R a real (=ordered) field with supremum, and V a (left) module + on R. We do not make use of the 'vector' interface as the latter enforces + finite dimension. *) + +Variables (R : realFieldType) (V : lmodType R). + +Hypothesis sup : forall (A : set R) (a m : R), + A a -> ubd A m -> + {s : R | ubd A s /\ forall u, ubd A u -> s <= u}. + +(* This could be obtained from sup but we are lazy here *) +Hypothesis inf : forall (A : set R) (a m : R), + A a -> ibd A m -> + {s : R | ibd A s /\ forall u, ibd A u -> u <= s}. + +Variables (F : subLmodType V) (f : {linear F -> R}) (p : V -> R). + +Hypothesis p_cvx : (@convex_function R V [set: V] p). + +Hypothesis f_bounded_by_p : forall x : F, (f x) <= (p (val x)). + +Theorem newHahnBanach : exists g : {scalar V}, + (forall x, g x <= p x) /\ (forall x, F x -> g (val x) = f x). +pose graphF v r := r = f v. +have graphFP: spec [set: F] f (fun z => p (val z)) graphF. split => //=. + - by move=> v r1 r2 [->] [ ->]. + - by move=> v1 v2 l r1 r2; rewrite /graphF => -> -> ;rewrite !linearE. + by move=> v r [->]. +(* +have [z zmax]:= zorn_rel_ex graphFP. +(* z : zorn_type (fun x : V => F x) f p + zmax : forall z0 : zorn_type (fun x : V => F x) f p, zorn_rel z z0 -> z0 = z +*) +pose FP v : Prop := F v. +have FP0 : FP 0 by []. +have [g gP]:= hb_witness linfF FP0 p_cvx sup inf zmax. +have scalg : linear_for *%R g. + case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. + have addg : additive g. + move=> w1 w2; apply/gP. + apply: linrel_add. + exact ls1. + by apply /gP. + by apply /gP. + suff scalg : scalable_for *%R g. + move=> a u v. + rewrite -gP. + rewrite (addrC _ v). + rewrite (addrC _ (g v)). + apply: ls1. + by apply /gP. + by apply /gP. + by move=> w l; apply/gP; apply: linrel_scale=> //; apply/gP. +pose H := GRing.isLinear.Build _ _ _ _ g scalg. +pose g' : {linear V -> R | *%R} := HB.pack g H. +exists g'. +have grxtf v : F v -> g v = f v. + move=> Fv; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf. + suff pmajg v : g v <= p v by split. + by case: z {zmax} gP => [c [_ _ bp _]] /= gP; apply/bp/gP. +Qed. + *) +Admitted. +End HahnBanachnew. + + +Section HBGeom. +Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 0). + +Hypothesis linF : forall (v1 v2 : V) (l : R), F v1 -> F v2 -> F (v1 + l *: v2). +Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> f (v1 + l *: v2) = f v1 + l * (f v2). + +(*Looked a long time for within *) +Definition continuousR_on (G : set V) (g : V -> R) := + {within G, continuous g}. +(* (forall x, (g @ (within G (nbhs x))) --> g x).*) + +(*Do we need to have F x ?*) +Definition continuousR_on_at (G : set V) (x : V) (g : V -> R) := + g @ (within G (nbhs x)) --> (g x). + +Lemma continuousR_scalar_on_bounded : + (continuousR_on_at F 0 f) -> + (exists r , (r > 0 ) /\ (forall x : V, F x -> (`|f x| ) <= `|x| * r)). +Proof. + rewrite /continuousR_on_at. + move => /cvg_ballP H. + have H': (0 < 1) by []. + have : \forall x \near within (fun x : V => F x) (nbhs 0), ball (f 0) 1 (f x). + apply: H. by []. + have f0 : f 0 = 0. + suff -> : f 0 = f (0 + (-1)*: 0) by rewrite linfF // mulNr mul1r addrN. + by rewrite scaleNr scaler0 addrN. + rewrite /( _ @ _ ) //= nearE /(within _ ) f0 //=. rewrite near_simpl. + rewrite -nbhs_nearE => H0 {H} ; move : (nbhs_ex H0) => [tp H] {H0}. + (*pose t := tp%:num . *) + exists (2*(tp%:num)^-1). split=> //. + move=> x. case: (lem (x=0)). + - by move=> ->; rewrite f0 normr0 normr0 //= mul0r. + - move/eqP=> xneq0 Fx. + pose a : V := (`|x|^-1 * (tp%:num)/2 ) *: x. + have Btp : ball 0 (tp%:num) a. + apply : ball_sym ; rewrite -ball_normE /ball_ /= subr0. + rewrite normrZ mulrC normrM. + rewrite !gtr0_norm //= ; last first. + rewrite pmulr_lgt0 // ?invr_gt0 ?normr_gt0 //. + rewrite mulrC -mulrA -mulrA ltr_pdivrMl; last by rewrite normr_gt0. + rewrite mulrC -mulrA gtr_pMl. + rewrite invf_lt1 //=. + by rewrite ltr1n. + by rewrite pmulr_lgt0 // !normr_gt0. + have Fa : F a by rewrite -[a]add0r; apply: linF. + have : `|f a| < 1. + by move: (H _ Btp Fa); rewrite /ball /ball_ //= sub0r normrN. + suff -> : ( f a = ( (`|x|^-1) * (tp%:num)/2 ) * ( f x)) . + rewrite normrM (gtr0_norm) //. + rewrite mulrC mulrC -mulrA -mulrA ltr_pdivrMl //= ; + last by rewrite normr_gt0. + rewrite mulrC [(_*1)]mulrC mul1r. + rewrite -[X in _ * X < _ ]invf_div ltr_pdivrMr //=; apply: ltW. + by rewrite !mulr_gt0 ?normr_gt0 // ?invr_gt0 normr_gt0. + suff -> : a = 0+ (`|x|^-1 * tp%:num /2) *: x by rewrite linfF // f0 add0r. + by rewrite add0r. +Qed. + +Lemma mymysup : forall (A : set R) (a m : R), + A a -> ubound A m -> + {s : R | ubound A s /\ forall u, ubound A u -> s <= u}. +Proof. + move => A a m Aa majAm. + have [A0 Aub]: has_sup A. split; first by exists a. + by exists m => x; apply majAm. + exists (reals.sup A). +split. + by apply: sup_upper_bound. + by move => x; apply: sup_le_ub. +Qed. + +(*TODO: should be lb_le_inf: *) +Lemma mymyinf : forall (A : set R) (a m : R), + A a -> lbound A m -> + {s : R | lbound A s /\ forall u, lbound A u -> u <= s}. + move => A a m Aa minAm. + have [A0 Alb]: has_inf A. split; first by exists a. + by exists m => x; apply minAm. + exists (reals.inf A). + split. + exact: ge_inf. + by move => x; apply: lb_le_inf. +Qed. + +Notation myHB := + (HahnBanachold mymysup mymyinf F0 linF linfF). + +Theorem HB_geom_normed : + continuousR_on_at F 0 f -> + exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall x, F x -> (g x = f x)). +Proof. + move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}. + pose p:= fun x : V => `|x|*r. + have convp: (@convex_function _ _ [set: V] p). + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [X in (_ <= X)]/conv /=. + move => v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl. + suff: `|l *: v1 + m *: v2| <= (l * `|v1| + m * `|v2|). + move => h; apply : ler_pM; last by []. + by apply : normr_ge0. + by apply : ltW. + by []. + have labs : `|l| = l by apply/normr_idP. + have mabs: `|m| = m by apply/normr_idP. + rewrite -[in(_*_)]labs -[in(m*_)]mabs. + rewrite -!normrZ. + by apply : ler_normD. + have majfp : forall x, F x -> f x <= p x. + move => x Fx; rewrite /(p _) ; apply : le_trans ; last by []. + apply : le_trans. + apply : ler_norm. + by apply : (fxrx x Fx). + move: (myHB convp majfp) => [ g [majgp F_eqgf] ] {majfp}. + exists g; split; last by []. + move=> x; rewrite /cvgP; apply: (continuousfor0_continuous). + apply: bounded_linear_continuous. + exists r. + split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *) + move => M m1; rewrite nbhs_ballP; exists 1 => /=; first by []. + move => y; rewrite -ball_normE //= sub0r => y1. + rewrite ler_norml; apply/andP. split. + - rewrite lerNl -linearN; apply: (le_trans (majgp (-y))). + by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. + - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. + apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. +Qed. + + +End HBGeom. + + +Section newHBGeom. + + (* TODO: port to ctvsType, by porting lemmas on continuous bounded linear functions there *) + +Variable (R : realType) (V: normedModType R) (F : subLmodType V) (f : {linear F -> R}). + +(* One needs to define the topological structure on F as the one induced by V, and make it a normedModtype, as was done for subLmodType *) + + +(* +Lemma mymysup : forall (A : set R) (a m : R), + A a -> ubound A m -> + {s : R | ubound A s /\ forall u, ubound A u -> s <= u}. +Proof. + move => A a m Aa majAm. + have [A0 Aub]: has_sup A. split; first by exists a. + by exists m => x; apply majAm. + exists (reals.sup A). +split. + by apply: sup_upper_bound. + by move => x; apply: sup_le_ub. +Qed. + +(*TODO: should be lb_le_inf: *) +Lemma mymyinf : forall (A : set R) (a m : R), + A a -> lbound A m -> + {s : R | lbound A s /\ forall u, lbound A u -> u <= s}. + move => A a m Aa minAm. + have [A0 Alb]: has_inf A. split; first by exists a. + by exists m => x; apply minAm. + exists (reals.inf A). + split. + exact: ge_inf. + by move => x; apply: lb_le_inf. +Qed. + + +Notation myHB := + (HahnBanach (boolp.EM) mymysup mymyinf F0 linF linfF). + *) + + Search "continuous" "subspace". +(* bounded_linear_continuous: forall [R : numFieldType] [V W : normedModType R] [f : {linear V -> W}], bounded_near f (nbhs (0 : V)) -> continuous f +linear_bounded_continuous: forall [R : numFieldType] [V W : normedModType R] (f : {linear V -> W}), bounded_near f (nbhs 0) <-> continuous f +continuous_linear_bounded: forall [R : numFieldType] [V W : normedModType R] (x : V) [f : {linear V -> W}], {for 0, continuous f} -> bounded_near f (nbhs x) *) + + (*TODO : clean the topological structure on F. Define subctvs ? *) +Theorem new_HB_geom_normed : + continuous (f : (@initial_topology (sub_type F) V val) -> R) -> + exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall (x : F), (g (val x) = f x)). +Proof. + move /(_ 0) => /= H; rewrite /from_subspace /=. + have f0 : {for 0, continuous ( (f : (@initial_topology (sub_type F) V val) -> R))}. + admit. + Check (continuous_linear_bounded). + (* TODO ; to apply this lemma, F needs to be given a normedmodtype structure *) + (* move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}. + (* want : r : + ltr0 : 0 < r + fxrx : forall x : V, F x -> `|f x| <= `|x| * r*) + pose p:= fun x : V => `|x|*r. + have convp: hahn_banach_theorem.convex p. + move=> v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl. + suff: `|l *: v1 + m *: v2| <= (l * `|v1| + m * `|v2|). + move => h; apply : ler_pM; last by []. + by apply : normr_ge0. + by apply : ltW. + by []. + have labs : `|l| = l by apply/normr_idP. + have mabs: `|m| = m by apply/normr_idP. + rewrite -[in(_*_)]labs -[in(m*_)]mabs. + rewrite -!normrZ. + by apply : ler_normD. + have majfp : forall x, F x -> f x <= p x. + move => x Fx; rewrite /(p _) ; apply : le_trans ; last by []. + apply : le_trans. + apply : ler_norm. + by apply : (fxrx x Fx). + move: (myHB convp majfp) => [ g [majgp F_eqgf] ] {majfp}. + exists g; split; last by []. + move=> x; rewrite /cvgP; apply: (continuousfor0_continuous). + apply: bounded_linear_continuous. + exists r. + split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *) + move => M m1; rewrite nbhs_ballP; exists 1 => /=; first by []. + move => y; rewrite -ball_normE //= sub0r => y1. + rewrite ler_norml; apply/andP. split. + - rewrite lerNl -linearN; apply: (le_trans (majgp (-y))). + by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. + - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. + apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. +Qed. +*) +Admitted. + + +End newHBGeom. From f44d8f2bf54aef4f4571e2420ea689a006dc6f65 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Mar 2026 22:25:41 +0900 Subject: [PATCH 08/11] convex functions wip i01 --- theories/hahn_banach_theorem.v | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 8258fecb7..6d959ecb2 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -581,18 +581,15 @@ Proof. pose p:= fun x : V => `|x|*r. have convp: (@convex_function _ _ [set: V] p). rewrite /convex_function /conv => l v1 v2 _ _ /=. - rewrite [X in (_ <= X)]/conv /=. - move => v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl. - suff: `|l *: v1 + m *: v2| <= (l * `|v1| + m * `|v2|). - move => h; apply : ler_pM; last by []. - by apply : normr_ge0. - by apply : ltW. - by []. - have labs : `|l| = l by apply/normr_idP. - have mabs: `|m| = m by apply/normr_idP. - rewrite -[in(_*_)]labs -[in(m*_)]mabs. - rewrite -!normrZ. - by apply : ler_normD. + rewrite [X in (_ <= X)]/conv /= /p. + apply: le_trans. + have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. + by apply: ler_normD. + by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. + rewrite mulrDl !normrZ -mulr_algl -[X in _ <= _ + X]mulr_algl. + have -> : `|l%:num| = l%:num by apply/normr_idP. + have -> : `|(l%:num).~| = (l%:num).~. apply/normr_idP. admit. + rewrite !mulrA. admit. have majfp : forall x, F x -> f x <= p x. move => x Fx; rewrite /(p _) ; apply : le_trans ; last by []. apply : le_trans. @@ -611,8 +608,7 @@ Proof. by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. -Qed. - +Admitted. End HBGeom. From e6a6d119e7ed73fa0980f67d3a149c5131b1b94f Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 9 Mar 2026 22:29:14 +0900 Subject: [PATCH 09/11] lemmas i01 and fix --- theories/hahn_banach_theorem.v | 38 +++++++++++++++++++++------------- 1 file changed, 24 insertions(+), 14 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 6d959ecb2..953d3821a 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -202,14 +202,23 @@ Hypothesis p_cvx : (@convex_function R V [set: V] p). real line directed by an arbitrary vector v *) Lemma divDl_ge0 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : 0 <= s / (s +t). - Admitted. - + by apply: divr_ge0 => //; apply: addr_ge0. + Qed. + Lemma divDl_le1 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : s / (s +t) <= 1. - Admitted. - - Lemma divD_onem (s t : R) : (s / (s + t)).~ = t / (s + t). - Admitted. - + move: s0; rewrite le0r => /orP []; first by move => /eqP ->; rewrite mul0r //. + move: t0; rewrite le0r => /orP []. + by move => /eqP -> s0; rewrite addr0 divff //=; apply: lt0r_neq0. + by move=> t0 s0; rewrite ler_pdivrMr ?mul1r ?addr_gt0 // lerDl ltW. + Qed. + + Lemma divD_onem (s t : R) (s0 : 0 < s) (t0 : 0 < t): (s / (s + t)).~ = t / (s + t). + rewrite /(_).~. + suff -> : 1 = (s + t)/(s + t) by rewrite -mulrBl -addrAC subrr add0r. + rewrite divff // /eqP addr_eq0; apply/negbT/eqP => H. + by move: s0; rewrite H oppr_gt0 ltNge; move/negP; apply; rewrite ltW. + Qed. + Lemma domain_extend (z : zorn_type) v : exists2 ze : zorn_type, (zorn_rel z ze) & (exists r, (carrier ze) v r). Proof. @@ -386,7 +395,7 @@ have graphFP : spec F f p graphF by split. have [z zmax]:= zorn_rel_ex graphFP. pose FP v : Prop := F v. have FP0 : FP 0 by []. -have [g gP]:= (hb_witness linfF FP0 p_cvx sup inf graphFP zmax). +have [g gP]:= (hb_witness linfF FP0 p_cvx sup inf zmax). have scalg : linear_for *%R g. case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. have addg : additive g. @@ -585,12 +594,13 @@ Proof. apply: le_trans. have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. by apply: ler_normD. - by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. - rewrite mulrDl !normrZ -mulr_algl -[X in _ <= _ + X]mulr_algl. + by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. + rewrite mulrDl !normrZ -mulr_algl -[X in _ <= _ + X]mulr_algl !scaler1. + (* where is the lemma combining mulr_algl and scaler1, easier to search *) have -> : `|l%:num| = l%:num by apply/normr_idP. - have -> : `|(l%:num).~| = (l%:num).~. apply/normr_idP. admit. - rewrite !mulrA. admit. - have majfp : forall x, F x -> f x <= p x. + have -> : `|(l%:num).~| = (l%:num).~ by apply/normr_idP; apply: onem_ge0. + by rewrite !mulrA. + have majfp : forall x, F x -> f x <= p x. move => x Fx; rewrite /(p _) ; apply : le_trans ; last by []. apply : le_trans. apply : ler_norm. @@ -608,7 +618,7 @@ Proof. by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. -Admitted. +Qed. End HBGeom. From 11483f26f3d2a9151febf53626e620de949d31cd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 11 Mar 2026 14:18:23 +0900 Subject: [PATCH 10/11] sup and inf from realtype --- theories/hahn_banach_theorem.v | 130 ++++++++------------------------- 1 file changed, 31 insertions(+), 99 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 953d3821a..398d09528 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -27,37 +27,10 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. Local Open Scope convex_scope. +Local Open Scope real_scope. Import GRing.Theory. Import Num.Theory. -Section SetPredRels. - - Variables T U : Type. - Implicit Types f g : T -> U -> Prop. - (* Functional (possibly empty or partial) graphs *) - Definition functional f := - forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. - -End SetPredRels. - - -Section OrderRels. - - Variable (R : numDomainType). - - (* Upper bound *) - Definition ubd (s : set R) (a : R) := forall x, s x -> x <= a. - - (* Lower bound *) - Definition ibd (s : set R) (a : R) := forall x, s x -> a <= x. - - (* the intension is that f is the graph of a function bounded by p *) - Definition maj_by T p (f : T -> R -> Prop) := - forall v r, f v r -> r <= p v. - - End OrderRels. - - Section LinAndCvx. Variables (R : numDomainType) (V : lmodType R). @@ -103,7 +76,7 @@ Section OrderRels. Section HBPreparation. - Variables (R : realFieldType) (V : lmodType R). + Variables (R : realType) (V : lmodType R). Variables (F : set V) (phi : V -> R) (p : V -> R). @@ -122,18 +95,13 @@ Qed. About convex_function. Hypothesis p_cvx : (@convex_function R V [set: V] p). - Hypothesis sup : forall (A : set R) (a m : R), - A a -> ubd A m -> - {s : R | ubd A s /\ forall u, ubd A u -> s <= u}. - - Hypothesis inf : forall (A : set R) (a m : R), - A a -> ibd A m -> - {s : R | ibd A s /\ forall u, ibd A u -> u <= s}. + Definition prol f := forall v, F v -> f v (phi v). - (* f is a subset of (V x R), if v is in pi_1 f, then (v, phi v) is in f. - Otherwise said, the graph of phi restructed to pi_1 f is included in f*) + Definition maj_by T p (f : T -> R -> Prop) := + forall v r, f v r -> r <= p v. - Definition prol f := forall v, F v -> f v (phi v). + Definition functional f := + forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. Definition spec (f : V -> R -> Prop) := [/\ functional f, linear_rel f, maj_by p f & prol f]. @@ -269,13 +237,21 @@ Hypothesis p_cvx : (@convex_function R V [set: V] p). [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]. pose Pb : set R := fun r => exists x1, exists r1, exists s1, [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]. - have exPa : Pa (a 0 0 1) by exists 0; exists 0; exists 1; split. - have exPb : Pb (b 0 0 1) by exists 0; exists 0; exists 1; split. - have majPa x : Pa x -> x <= b 0 0 1. - move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. - have minPb x : Pb x -> a 0 0 1 <= x. - move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. - have [sa [ubdP saP]]:= sup exPa majPa; have [ib [ibdP ibP]]:= inf exPb minPb. + (* have exPb : Pb (b 0 0 1) by exists 0; exists 0; exists 1; split. *) + (* have minPb x : Pb x -> a 0 0 1 <= x. *) + (* move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. *) + (* have [ib [ibdP ibP]]:= inf exPb minPb. (*To be deleted*) *) + pose sa := reals.sup Pa. (* This is why we need realTypes, we need P with values in a realType *) + have Pax : Pa !=set0 by exists (a 0 0 1); exists 0; exists 0; exists 1; split. + have ubdP : ubound Pa sa. + apply: sup_upper_bound; split => //=. + exists (b 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have saP: forall u : R, ubound Pa u -> sa <= u by move=> u; apply: ge_sup. + pose ib := reals.inf Pb. (* This is why we need realTypes, we need P with values in a realType *) + have Pbx : Pb !=set0 by exists (b 0 0 1); exists 0; exists 0; exists 1; split. + have ibdP : lbound Pb ib. + by apply: ge_inf; exists (a 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have ibP: forall u : R, lbound Pb u -> u <= ib by move=> u; apply: lb_le_inf Pbx. have le_sa_ib : sa <= ib. apply: saP=> r' [y [r [l [cry lt0l -> {r'}]]]]. apply: ibP=> s' [z [s [m [crz lt0m -> {s'}]]]]; exact: le_a_b. @@ -356,18 +332,10 @@ Qed. on R. We do not make use of the 'vector' interface as the latter enforces finite dimension. *) -Variables (R : realFieldType) (V : lmodType R). + Variables (R : realType) (V : lmodType R) (f: V -> R). -Hypothesis sup : forall (A : set R) (a m : R), - A a -> ubd A m -> - {s : R | ubd A s /\ forall u, ubd A u -> s <= u}. - -(* This could be obtained from sup but we are lazy here *) -Hypothesis inf : forall (A : set R) (a m : R), - A a -> ibd A m -> - {s : R | ibd A s /\ forall u, ibd A u -> u <= s}. + Variables (F : set V) (phi : V -> R) (p : V -> R). -Variables (F : pred V) (f : V -> R) (p : V -> R). (* MathComp seems to lack of an interface for submodules of V, so for now we state "by hand" that F is closed under linear combinations. *) @@ -389,13 +357,12 @@ have lin_graphF : linear_rel graphF. move=> v1 v2 l r1 r2 [Fv1 ->] [Fv2 ->]; split; first exact: linF. by rewrite linfF. have maj_graphF : maj_by p graphF by move=> v r [Fv ->]; exact: f_bounded_by_p. - have prol_graphF : prol F f graphF by move=> v Fv; split. have graphFP : spec F f p graphF by split. have [z zmax]:= zorn_rel_ex graphFP. pose FP v : Prop := F v. have FP0 : FP 0 by []. -have [g gP]:= (hb_witness linfF FP0 p_cvx sup inf zmax). +have [g gP]:= (hb_witness linfF FP0 p_cvx zmax). have scalg : linear_for *%R g. case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. have addg : additive g. @@ -432,16 +399,7 @@ Section HahnBanachnew. on R. We do not make use of the 'vector' interface as the latter enforces finite dimension. *) -Variables (R : realFieldType) (V : lmodType R). - -Hypothesis sup : forall (A : set R) (a m : R), - A a -> ubd A m -> - {s : R | ubd A s /\ forall u, ubd A u -> s <= u}. - -(* This could be obtained from sup but we are lazy here *) -Hypothesis inf : forall (A : set R) (a m : R), - A a -> ibd A m -> - {s : R | ibd A s /\ forall u, ibd A u -> u <= s}. +Variables (R : realType) (V : lmodType R). Variables (F : subLmodType V) (f : {linear F -> R}) (p : V -> R). @@ -463,7 +421,7 @@ have [z zmax]:= zorn_rel_ex graphFP. *) pose FP v : Prop := F v. have FP0 : FP 0 by []. -have [g gP]:= hb_witness linfF FP0 p_cvx sup inf zmax. +have [g gP]:= hb_witness linfF FP0 p_cvx inf zmax. have scalg : linear_for *%R g. case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. have addg : additive g. @@ -495,6 +453,7 @@ End HahnBanachnew. Section HBGeom. +(* TODO : make R : realFieldtype *) Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 0). Hypothesis linF : forall (v1 v2 : V) (l : R), F v1 -> F v2 -> F (v1 + l *: v2). @@ -553,34 +512,8 @@ Proof. by rewrite add0r. Qed. -Lemma mymysup : forall (A : set R) (a m : R), - A a -> ubound A m -> - {s : R | ubound A s /\ forall u, ubound A u -> s <= u}. -Proof. - move => A a m Aa majAm. - have [A0 Aub]: has_sup A. split; first by exists a. - by exists m => x; apply majAm. - exists (reals.sup A). -split. - by apply: sup_upper_bound. - by move => x; apply: sup_le_ub. -Qed. - -(*TODO: should be lb_le_inf: *) -Lemma mymyinf : forall (A : set R) (a m : R), - A a -> lbound A m -> - {s : R | lbound A s /\ forall u, lbound A u -> u <= s}. - move => A a m Aa minAm. - have [A0 Alb]: has_inf A. split; first by exists a. - by exists m => x; apply minAm. - exists (reals.inf A). - split. - exact: ge_inf. - by move => x; apply: lb_le_inf. -Qed. - Notation myHB := - (HahnBanachold mymysup mymyinf F0 linF linfF). + (HahnBanachold F0 linF linfF). Theorem HB_geom_normed : continuousR_on_at F 0 f -> @@ -594,9 +527,8 @@ Proof. apply: le_trans. have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. by apply: ler_normD. - by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. - rewrite mulrDl !normrZ -mulr_algl -[X in _ <= _ + X]mulr_algl !scaler1. - (* where is the lemma combining mulr_algl and scaler1, easier to search *) + by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. + rewrite mulrDl !normrZ -![_ *: _]/(_ * _). have -> : `|l%:num| = l%:num by apply/normr_idP. have -> : `|(l%:num).~| = (l%:num).~ by apply/normr_idP; apply: onem_ge0. by rewrite !mulrA. From 846ab42e695256ac02e66894afc5363cfe6e1008 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 11 Mar 2026 16:37:45 +0900 Subject: [PATCH 11/11] F : subLmodType --- theories/hahn_banach_theorem.v | 362 +++++++-------------------------- 1 file changed, 74 insertions(+), 288 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 398d09528..627fc5bc6 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -28,18 +28,15 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. Local Open Scope convex_scope. Local Open Scope real_scope. - Import GRing.Theory. - Import Num.Theory. +Import GRing.Theory. +Import Num.Theory. - Section LinAndCvx. + +Module Linrel. +Section Linrelsec. Variables (R : numDomainType) (V : lmodType R). - (* - Check convex_function. - Definition convex_function (p : V -> R) := forall v1 v2 l m, - ( 0 <= l /\ 0 <= m) -> l + m = 1 -> p (l *: v1 + m *: v2) <= l * (p v1) + m * (p v2). - *) - + Definition linear_rel (f : V -> R -> Prop) := forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). @@ -71,47 +68,45 @@ Local Open Scope real_scope. exists v' : V, exists r' : R, exists lambda : R, [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. - End LinAndCvx. +End Linrelsec. +End Linrel. - Section HBPreparation. +Section HBPreparation. +Import Linrel. + (* TODO: getting rid of relations and linear relations to make Zorn act on functions only ? *) Variables (R : realType) (V : lmodType R). - Variables (F : set V) (phi : V -> R) (p : V -> R). - + Variables (F : subLmodType V) (phi : {linear F -> R}) (p : V -> R). + Hypothesis linphiF : forall v1 v2 l, F v1 -> F v2 -> phi (v1 + l *: v2) = phi v1 + l * (phi v2). - Implicit Types (f g : V -> R -> Prop). - -Hypothesis F0 : F 0. - -Fact phi0 : phi 0 = 0. -Proof. -have -> : 0 = 0 + (-1) *: 0 :> V by rewrite scaler0 addr0. -by rewrite linphiF // mulN1r addrN. -Qed. - -About convex_function. +Implicit Types (f g : V -> R -> Prop). + Hypothesis p_cvx : (@convex_function R V [set: V] p). - Definition prol f := forall v, F v -> f v (phi v). +Definition prol f := forall v, F v -> f (val v) (phi v). - Definition maj_by T p (f : T -> R -> Prop) := +Definition maj_by T p (f : T -> R -> Prop) := forall v r, f v r -> r <= p v. - Definition functional f := - forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. +Definition functional f := + forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. - Definition spec (f : V -> R -> Prop) := +Definition linear_rel (f : V -> R -> Prop) := + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + +Definition spec (f : V -> R -> Prop) := [/\ functional f, linear_rel f, maj_by p f & prol f]. - Record zorn_type : Type := ZornType +Record zorn_type : Type := ZornType {carrier : V -> R -> Prop; specP : spec carrier}. - Hypothesis spec_phi : spec (fun v r => F v /\ r = phi v). +(*Variables (v : V) (r : R). Check (v \in (val @` [set: F])).*) +Hypothesis spec_phi : spec (fun v r => exists2 y : F, v = val y & r = phi y). - Definition zphi := ZornType spec_phi. +Definition zphi := ZornType spec_phi. Lemma zorn_type_eq z1 z2 : carrier z1 = carrier z2 -> z1 = z2. Proof. @@ -194,7 +189,8 @@ Hypothesis p_cvx : (@convex_function R V [set: V] p). by case=> r rP; exists z => //; exists r. case: z => [c [fs1 ls1 ms1 ps1]] /= nzv. have c00 : c 0 0. - rewrite -phi0; exact: ps1. + have <- : phi 0 = 0 by rewrite linear0. + by move: ps1; rewrite /prol /= => /(_ 0 _) /=; rewrite GRing.val0; apply. have [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> r + lambda * a <= p (x + lambda *: v). suff [a aP] : exists a, forall (x : V) (r lambda : R), @@ -237,11 +233,7 @@ Hypothesis p_cvx : (@convex_function R V [set: V] p). [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]. pose Pb : set R := fun r => exists x1, exists r1, exists s1, [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]. - (* have exPb : Pb (b 0 0 1) by exists 0; exists 0; exists 1; split. *) - (* have minPb x : Pb x -> a 0 0 1 <= x. *) - (* move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. *) - (* have [ib [ibdP ibP]]:= inf exPb minPb. (*To be deleted*) *) - pose sa := reals.sup Pa. (* This is why we need realTypes, we need P with values in a realType *) + pose sa := reals.sup Pa. (* This is why we need realTypes, we need p with values in a realType *) have Pax : Pa !=set0 by exists (a 0 0 1); exists 0; exists 0; exists 1; split. have ubdP : ubound Pa sa. apply: sup_upper_bound; split => //=. @@ -265,14 +257,16 @@ Hypothesis p_cvx : (@convex_function R V [set: V] p). - suff : a x r l <= alpha. rewrite /a. move/ler_pdivrMr: lt0l->. by rewrite lerBlDl -lerBlDr mulrC. - by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l. - pose z' := add_line c v a. + by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l. + pose z' := fun k r => + exists v' : V, exists r' : R, exists lambda : R, + [/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a]. have z'_extends : forall v r, c v r -> z' v r. move=> x r cxr; exists x; exists r; exists 0; split=> //. - by rewrite scale0r addr0. - by rewrite mul0r addr0. have z'_prol : prol z'. - move=> x /ps1 cxphix; exists x; exists (phi x); exists 0; split=> //. + move=> x /ps1 cxphix; exists (val x); exists (phi x); exists 0; split=> //. - by rewrite scale0r addr0. - by rewrite mul0r addr0. - have z'_maj_by_p : maj_by p z'. @@ -291,7 +285,10 @@ Hypothesis p_cvx : (@convex_function R V [set: V] p). have h1 (x : V) (r l : R) : x = l *: v -> c x r -> x = 0 /\ l = 0. move=> -> cxr; case: (l =P 0) => [-> | /eqP ln0]; first by rewrite scale0r. suff cvs: c v (l^-1 * r) by elim:nzv; exists (l^-1 * r). - suff -> : v = l ^-1 *: (l *: v) by exact: linrel_scale. + suff -> : v = l ^-1 *: (l *: v). + have -> : + c ( l ^-1 *: (l *: v)) (l^-1 * r) = c (0 + l ^-1 *: (l *: v)) (0 + l^-1 * r) by rewrite !add0r. + by apply: ls1=> //; apply: linrel_00 fxr. by rewrite scalerA mulVf ?scale1r. have [rw12 erw12] : exists r, c (w1 - w2) r. exists (s1 + (-1) * s2). @@ -326,49 +323,43 @@ Qed. End HBPreparation. - Section HahnBanachold. +Section HahnBanachold. +Import Linrel. (* Now we prove HahnBanach on functions*) (* We consider R a real (=ordered) field with supremum, and V a (left) module on R. We do not make use of the 'vector' interface as the latter enforces finite dimension. *) - Variables (R : realType) (V : lmodType R) (f: V -> R). + Variables (R : realType) (V : lmodType R). - Variables (F : set V) (phi : V -> R) (p : V -> R). + Variables (F : subLmodType V) (f : {linear F -> R}) (p : V -> R). (* MathComp seems to lack of an interface for submodules of V, so for now we state "by hand" that F is closed under linear combinations. *) -Hypothesis F0 : F 0. -Hypothesis linF : forall v1 v2 l, F v1 -> F v2 -> F (v1 + l *: v2). - -Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> - f (v1 + l *: v2) = f v1 + l * (f v2). Hypothesis p_cvx : (@convex_function R V [set: V] p). -Hypothesis f_bounded_by_p : forall x, F x -> f x <= p x. +Hypothesis f_bounded_by_p : forall (z : F), (f z <= p (val z)). Theorem HahnBanachold : exists g : {scalar V}, - (forall x, g x <= p x) /\ (forall x, F x -> g x = f x). -pose graphF v r := F v /\ r = f v. -have func_graphF : functional graphF by move=> v r1 r2 [Fv ->] [_ ->]. -have lin_graphF : linear_rel graphF. - move=> v1 v2 l r1 r2 [Fv1 ->] [Fv2 ->]; split; first exact: linF. - by rewrite linfF. -have maj_graphF : maj_by p graphF by move=> v r [Fv ->]; exact: f_bounded_by_p. -have prol_graphF : prol F f graphF by move=> v Fv; split. -have graphFP : spec F f p graphF by split. + (forall x, g x <= p x) /\ (forall (z : F), g (\val z) = f z). +pose graphF (v : V) r := exists2 z : F, v = \val z & r = f z. +have func_graphF : functional graphF. + by move=> _ _ _ [z1 -> ->] [z2] /val_inj -> ->. +have lin_graphF : linear_rel graphF. + by move=> _ _ l _ _ [z1 [-> ->]] [z2 -> ->]; exists (z1 + l*: z2); by rewrite linearD linearZ. +have maj_graphF : maj_by p graphF by move=> _ _ [z -> ->]; exact: f_bounded_by_p. +have prol_graphF : prol f graphF by move=> v Fv; exists v. +have graphFP : spec f p graphF by split. have [z zmax]:= zorn_rel_ex graphFP. -pose FP v : Prop := F v. -have FP0 : FP 0 by []. -have [g gP]:= (hb_witness linfF FP0 p_cvx zmax). +have [g gP]:= (hb_witness p_cvx zmax). have scalg : linear_for *%R g. case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. have addg : additive g. move=> w1 w2; apply/gP. apply: linrel_add. - exact ls1. + exact: ls1. by apply /gP. by apply /gP. suff scalg : scalable_for *%R g. @@ -381,83 +372,20 @@ have scalg : linear_for *%R g. by apply /gP. by move=> w l; apply/gP; apply: linrel_scale=> //; apply/gP. pose H := GRing.isLinear.Build _ _ _ _ g scalg. -pose g' : {linear V -> R | *%R} := HB.pack g H. +pose g' : {linear V -> R | *%R} := HB.pack g H. simpl in *. exists g'. -have grxtf v : F v -> g v = f v. - move=> Fv; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf. - suff pmajg v : g v <= p v by split. - by case: z {zmax} gP => [c [_ _ bp _]] /= gP; apply/bp/gP. +have gextf y : F y -> g (val y) = f y. + by move=> Fy; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf. +split; last by move => z'; apply: gextf. +suff pmajg (y : F) : g (val y) <= p (val y). + by case: z {zmax} gP => [c [_ _ bp _]] /= gP => x; apply: bp; apply/gP. +by rewrite gextf //. Qed. End HahnBanachold. - - -Section HahnBanachnew. -(* Now we prove HahnBanach on functions*) -(* We consider R a real (=ordered) field with supremum, and V a (left) module - on R. We do not make use of the 'vector' interface as the latter enforces - finite dimension. *) - -Variables (R : realType) (V : lmodType R). - -Variables (F : subLmodType V) (f : {linear F -> R}) (p : V -> R). - -Hypothesis p_cvx : (@convex_function R V [set: V] p). - -Hypothesis f_bounded_by_p : forall x : F, (f x) <= (p (val x)). - -Theorem newHahnBanach : exists g : {scalar V}, - (forall x, g x <= p x) /\ (forall x, F x -> g (val x) = f x). -pose graphF v r := r = f v. -have graphFP: spec [set: F] f (fun z => p (val z)) graphF. split => //=. - - by move=> v r1 r2 [->] [ ->]. - - by move=> v1 v2 l r1 r2; rewrite /graphF => -> -> ;rewrite !linearE. - by move=> v r [->]. -(* -have [z zmax]:= zorn_rel_ex graphFP. -(* z : zorn_type (fun x : V => F x) f p - zmax : forall z0 : zorn_type (fun x : V => F x) f p, zorn_rel z z0 -> z0 = z -*) -pose FP v : Prop := F v. -have FP0 : FP 0 by []. -have [g gP]:= hb_witness linfF FP0 p_cvx inf zmax. -have scalg : linear_for *%R g. - case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. - have addg : additive g. - move=> w1 w2; apply/gP. - apply: linrel_add. - exact ls1. - by apply /gP. - by apply /gP. - suff scalg : scalable_for *%R g. - move=> a u v. - rewrite -gP. - rewrite (addrC _ v). - rewrite (addrC _ (g v)). - apply: ls1. - by apply /gP. - by apply /gP. - by move=> w l; apply/gP; apply: linrel_scale=> //; apply/gP. -pose H := GRing.isLinear.Build _ _ _ _ g scalg. -pose g' : {linear V -> R | *%R} := HB.pack g H. -exists g'. -have grxtf v : F v -> g v = f v. - move=> Fv; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf. - suff pmajg v : g v <= p v by split. - by case: z {zmax} gP => [c [_ _ bp _]] /= gP; apply/bp/gP. -Qed. - *) -Admitted. -End HahnBanachnew. - - Section HBGeom. -(* TODO : make R : realFieldtype *) -Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 0). - -Hypothesis linF : forall (v1 v2 : V) (l : R), F v1 -> F v2 -> F (v1 + l *: v2). -Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> f (v1 + l *: v2) = f v1 + l * (f v2). +Variable (R : realType) (V : normedModType R) (F : subLmodType V) (f : {linear F -> R}). (*Looked a long time for within *) Definition continuousR_on (G : set V) (g : V -> R) := @@ -468,58 +396,17 @@ Definition continuousR_on (G : set V) (g : V -> R) := Definition continuousR_on_at (G : set V) (x : V) (g : V -> R) := g @ (within G (nbhs x)) --> (g x). -Lemma continuousR_scalar_on_bounded : - (continuousR_on_at F 0 f) -> - (exists r , (r > 0 ) /\ (forall x : V, F x -> (`|f x| ) <= `|x| * r)). -Proof. - rewrite /continuousR_on_at. - move => /cvg_ballP H. - have H': (0 < 1) by []. - have : \forall x \near within (fun x : V => F x) (nbhs 0), ball (f 0) 1 (f x). - apply: H. by []. - have f0 : f 0 = 0. - suff -> : f 0 = f (0 + (-1)*: 0) by rewrite linfF // mulNr mul1r addrN. - by rewrite scaleNr scaler0 addrN. - rewrite /( _ @ _ ) //= nearE /(within _ ) f0 //=. rewrite near_simpl. - rewrite -nbhs_nearE => H0 {H} ; move : (nbhs_ex H0) => [tp H] {H0}. - (*pose t := tp%:num . *) - exists (2*(tp%:num)^-1). split=> //. - move=> x. case: (lem (x=0)). - - by move=> ->; rewrite f0 normr0 normr0 //= mul0r. - - move/eqP=> xneq0 Fx. - pose a : V := (`|x|^-1 * (tp%:num)/2 ) *: x. - have Btp : ball 0 (tp%:num) a. - apply : ball_sym ; rewrite -ball_normE /ball_ /= subr0. - rewrite normrZ mulrC normrM. - rewrite !gtr0_norm //= ; last first. - rewrite pmulr_lgt0 // ?invr_gt0 ?normr_gt0 //. - rewrite mulrC -mulrA -mulrA ltr_pdivrMl; last by rewrite normr_gt0. - rewrite mulrC -mulrA gtr_pMl. - rewrite invf_lt1 //=. - by rewrite ltr1n. - by rewrite pmulr_lgt0 // !normr_gt0. - have Fa : F a by rewrite -[a]add0r; apply: linF. - have : `|f a| < 1. - by move: (H _ Btp Fa); rewrite /ball /ball_ //= sub0r normrN. - suff -> : ( f a = ( (`|x|^-1) * (tp%:num)/2 ) * ( f x)) . - rewrite normrM (gtr0_norm) //. - rewrite mulrC mulrC -mulrA -mulrA ltr_pdivrMl //= ; - last by rewrite normr_gt0. - rewrite mulrC [(_*1)]mulrC mul1r. - rewrite -[X in _ * X < _ ]invf_div ltr_pdivrMr //=; apply: ltW. - by rewrite !mulr_gt0 ?normr_gt0 // ?invr_gt0 normr_gt0. - suff -> : a = 0+ (`|x|^-1 * tp%:num /2) *: x by rewrite linfF // f0 add0r. - by rewrite add0r. -Qed. +Let setF := [set x : V | exists (z : F), val z = x]. -Notation myHB := - (HahnBanachold F0 linF linfF). +(* TODO : define (F : subNormedModType V) so as to have (f : {linear_continuous F -> +R}), and to obtain the first hypothesis of the following theorem through the +lemmas continuous_linear_bounded*) Theorem HB_geom_normed : - continuousR_on_at F 0 f -> - exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall x, F x -> (g x = f x)). + (exists r , (r > 0 ) /\ (forall (z : F), (`|f z| ) <= `|(val z)| * r)) -> + exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall (x : F), (g (val x) = f x)). Proof. - move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}. + move=> [r [ltr0 fxrx]]. pose p:= fun x : V => `|x|*r. have convp: (@convex_function _ _ [set: V] p). rewrite /convex_function /conv => l v1 v2 _ _ /=. @@ -532,12 +419,10 @@ Proof. have -> : `|l%:num| = l%:num by apply/normr_idP. have -> : `|(l%:num).~| = (l%:num).~ by apply/normr_idP; apply: onem_ge0. by rewrite !mulrA. - have majfp : forall x, F x -> f x <= p x. - move => x Fx; rewrite /(p _) ; apply : le_trans ; last by []. - apply : le_trans. - apply : ler_norm. - by apply : (fxrx x Fx). - move: (myHB convp majfp) => [ g [majgp F_eqgf] ] {majfp}. + have majfp : forall z : F, f z <= p (\val z). + move => z; rewrite /(p _) ; apply : le_trans; last by []. + by apply : ler_norm. + move: (HahnBanachold convp majfp) => [ g [majgp F_eqgf] ] {majfp}. exists g; split; last by []. move=> x; rewrite /cvgP; apply: (continuousfor0_continuous). apply: bounded_linear_continuous. @@ -553,102 +438,3 @@ Proof. Qed. End HBGeom. - - -Section newHBGeom. - - (* TODO: port to ctvsType, by porting lemmas on continuous bounded linear functions there *) - -Variable (R : realType) (V: normedModType R) (F : subLmodType V) (f : {linear F -> R}). - -(* One needs to define the topological structure on F as the one induced by V, and make it a normedModtype, as was done for subLmodType *) - - -(* -Lemma mymysup : forall (A : set R) (a m : R), - A a -> ubound A m -> - {s : R | ubound A s /\ forall u, ubound A u -> s <= u}. -Proof. - move => A a m Aa majAm. - have [A0 Aub]: has_sup A. split; first by exists a. - by exists m => x; apply majAm. - exists (reals.sup A). -split. - by apply: sup_upper_bound. - by move => x; apply: sup_le_ub. -Qed. - -(*TODO: should be lb_le_inf: *) -Lemma mymyinf : forall (A : set R) (a m : R), - A a -> lbound A m -> - {s : R | lbound A s /\ forall u, lbound A u -> u <= s}. - move => A a m Aa minAm. - have [A0 Alb]: has_inf A. split; first by exists a. - by exists m => x; apply minAm. - exists (reals.inf A). - split. - exact: ge_inf. - by move => x; apply: lb_le_inf. -Qed. - - -Notation myHB := - (HahnBanach (boolp.EM) mymysup mymyinf F0 linF linfF). - *) - - Search "continuous" "subspace". -(* bounded_linear_continuous: forall [R : numFieldType] [V W : normedModType R] [f : {linear V -> W}], bounded_near f (nbhs (0 : V)) -> continuous f -linear_bounded_continuous: forall [R : numFieldType] [V W : normedModType R] (f : {linear V -> W}), bounded_near f (nbhs 0) <-> continuous f -continuous_linear_bounded: forall [R : numFieldType] [V W : normedModType R] (x : V) [f : {linear V -> W}], {for 0, continuous f} -> bounded_near f (nbhs x) *) - - (*TODO : clean the topological structure on F. Define subctvs ? *) -Theorem new_HB_geom_normed : - continuous (f : (@initial_topology (sub_type F) V val) -> R) -> - exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall (x : F), (g (val x) = f x)). -Proof. - move /(_ 0) => /= H; rewrite /from_subspace /=. - have f0 : {for 0, continuous ( (f : (@initial_topology (sub_type F) V val) -> R))}. - admit. - Check (continuous_linear_bounded). - (* TODO ; to apply this lemma, F needs to be given a normedmodtype structure *) - (* move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}. - (* want : r : - ltr0 : 0 < r - fxrx : forall x : V, F x -> `|f x| <= `|x| * r*) - pose p:= fun x : V => `|x|*r. - have convp: hahn_banach_theorem.convex p. - move=> v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl. - suff: `|l *: v1 + m *: v2| <= (l * `|v1| + m * `|v2|). - move => h; apply : ler_pM; last by []. - by apply : normr_ge0. - by apply : ltW. - by []. - have labs : `|l| = l by apply/normr_idP. - have mabs: `|m| = m by apply/normr_idP. - rewrite -[in(_*_)]labs -[in(m*_)]mabs. - rewrite -!normrZ. - by apply : ler_normD. - have majfp : forall x, F x -> f x <= p x. - move => x Fx; rewrite /(p _) ; apply : le_trans ; last by []. - apply : le_trans. - apply : ler_norm. - by apply : (fxrx x Fx). - move: (myHB convp majfp) => [ g [majgp F_eqgf] ] {majfp}. - exists g; split; last by []. - move=> x; rewrite /cvgP; apply: (continuousfor0_continuous). - apply: bounded_linear_continuous. - exists r. - split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *) - move => M m1; rewrite nbhs_ballP; exists 1 => /=; first by []. - move => y; rewrite -ball_normE //= sub0r => y1. - rewrite ler_norml; apply/andP. split. - - rewrite lerNl -linearN; apply: (le_trans (majgp (-y))). - by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. - - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. - apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. -Qed. -*) -Admitted. - - -End newHBGeom.