From 66bbe24282035838be6f1ecda635c8e1b751bed0 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Mar 2026 12:24:49 +0900 Subject: [PATCH 01/16] 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 b44ac9e97b..4f11e9bc74 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -220,6 +220,7 @@ - in `normed_module.v`, turned into `Let`'s: + local lemmas `add_continuous`, `scale_continuous`, `locally_convex` + ### Renamed - in `topology_structure.v` @@ -264,6 +265,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 66a143d7ee..c050e7834e 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 096f55960b..16cfdc7419 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 d9e4f68f6569e32b1d6922eb13bfc45fb7ae1793 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 6 Mar 2026 14:10:06 +0900 Subject: [PATCH 02/16] 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 4f11e9bc74..14e5333b3e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -70,6 +70,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. @@ -220,6 +223,8 @@ - in `normed_module.v`, turned into `Let`'s: + local lemmas `add_continuous`, `scale_continuous`, `locally_convex` +- moved from `tvs.v` to `convex.v` + + definition `convex` ### Renamed diff --git a/theories/convex.v b/theories/convex.v index c050e7834e..d44cadc1c5 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 d119bce20c..ed44d718e2 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. move=> B [x] [r] ->. rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 09c6de58a9..39148a936f 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. move=> B [x] [r] ->. rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE. @@ -587,8 +595,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 dac332469f5b3ab614532d76e4482ddda4d10439 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 21 Nov 2024 17:30:55 +0100 Subject: [PATCH 03/16] LinearContinuous structure --- theories/normedtype_theory/tvs.v | 160 +++++++++++++++++++++++++++++++ 1 file changed, 160 insertions(+) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 39148a936f..cdd1373cf4 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -609,3 +609,163 @@ HB.instance Definition _ := Uniform_isTvs.Build K (E * F)%type prod_locally_convex. End prod_Tvs. + + +HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) + (F : NbhsZmodule.type) s := + {f of @GRing.Linear K E F s f & @Continuous E F f }. + +HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) + (F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := { + linearP : linear_for s f ; + continuousP : continuous f + }. + +HB.builders Context K E F s f of @isLinearContinuous K E F s f. + +HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP. +HB.instance Definition _ := isContinuous.Build E F f continuousP. + +HB.end. + +Section lcfun_pred. +Context {K : numDomainType} {E : NbhsLmodule.type K} {F : NbhsZmodule.type} {s : K -> F -> F}. +Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ]. +Definition lcfun_key : pred_key lcfun. Proof. exact. Qed. +Canonical lcfun_keyed := KeyedPred lcfun_key. +End lcfun_pred. + +Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'" + (at level 0, U at level 98, V at level 99, + format "{ 'linear_continuous' U -> V | s }"). +Reserved Notation "'{' 'linear_continuous' U '->' V '}'" + (at level 0, U at level 98, V at level 99, + format "{ 'linear_continuous' U -> V }"). +Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s) + : type_scope. +Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R} + : type_scope. + +Section lcfun. +Context {R : numDomainType} {E : NbhsLmodule.type R} {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. +Notation T := {linear_continuous E -> F | s}. +Notation lcfun := (@lcfun _ E F s). + +Section Sub. +Context (f : E -> F) (fP : f \in lcfun). + +Definition lcfun_Sub_subproof := + @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)). +#[local] HB.instance Definition _ := lcfun_Sub_subproof. +Definition lcfun_Sub : {linear_continuous _ -> _ | _ } := f. +End Sub. + +Lemma lcfun_rect (K : T -> Type) : + (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u. +Proof. +move=> Ksub [f [[Pf]]]/=. +Admitted. + +Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _). +Proof. by []. Qed. + +HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP. + +Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. + +HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:]. + +End lcfun. + +(* Section lcfun_realType. *) +(* Context {E : sigmaRingType d} {F : realType}. *) + +(* HB.instance Definition _ := @isMeasurableFun.Build _ _ _ F *) +(* (@normr F F) (@normr_measurable F setT). *) + +(* HB.instance Definition _ := *) +(* isMeasurableFun.Build _ _ _ _ (@expR F) (@measurable_expR F). *) + +(* End lcfun_realType. *) + +Section lcfun_linearcontinuousType. +Context {R : numDomainType} {E : NbhsLmodule.type R} {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. + +Lemma measurableT_comp_subproof (f : {lcfun _ >-> F}) (g : {linear_continuous E -> F | s}) : + measurable_fun setT (f \o g). +Proof. exact: measurableT_comp. Qed. + +HB.instance Definition _ (f : {lcfun _ >-> F}) (g : {linear_continuous E -> F | s}) := + isMeasurableFun.Build _ _ _ _ (f \o g) (measurableT_comp_subproof _ _). + +End lcfun_measurableType. + +Section ring. +Context d (E : measurableType d) (F : realType). + +Lemma lcfun_subring_closed : subring_closed (@lcfun _ _ E F). +Proof. +split=> [|f g|f g]; rewrite !inE/=. +- exact: measurable_cst. +- exact: measurable_funB. +- exact: measurable_funM. +Qed. +HB.instance Definition _ := GRing.isSubringClosed.Build _ + (@lcfun d default_measure_display E F) lcfun_subring_closed. +HB.instance Definition _ := [SubChoice_isSubComRing of {linear_continuous E -> F | s} by <:]. + +Implicit Types (f g : {linear_continuous E -> F | s}). + +Lemma lcfun0 : (0 : {linear_continuous E -> F | s}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. +Lemma lcfun1 : (1 : {linear_continuous E -> F | s}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. +Lemma lcfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. +Lemma lcfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. +Lemma lcfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. +Lemma lcfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. +Lemma lcfun_sum I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma lcfun_prod I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma lcfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). +Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS lcfunM/= IHn. Qed. + +HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). +HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). +HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). +HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). + +Definition mindic (D : set E) of measurable D : E -> F := \1_D. + +Lemma mindicE (D : set E) (mD : measurable D) : + mindic mD = (fun x => (x \in D)%:R). +Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. + +HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ E F (mindic mD) + (@measurable_fun_indic _ E F setT D mD). + +Definition indic_lcfun (D : set E) (mD : measurable D) := + [the {linear_continuous E -> F | s} of mindic mD]. + +HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). +Definition scale_lcfun k f := [the {linear_continuous E -> F | s} of k \o* f]. + +Lemma max_lcfun_subproof f g : @isMeasurableFun d _ E F (f \max g). +Proof. by split; apply: measurable_maxr. Qed. + +HB.instance Definition _ f g := max_lcfun_subproof f g. + +Definition max_lcfun f g := [the {lcfun E >-> _} of f \max g]. + +End ring. + + + + +Section dual. + +Definition linear_continuous (f : E -> F) : linear f /\ continuous f. + +End dual. From b8d0cbd64453505c171b28aefecc019f89076f9c Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 21 Nov 2024 18:04:35 +0100 Subject: [PATCH 04/16] wip duality --- theories/normedtype_theory/tvs.v | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index cdd1373cf4..d50cd15469 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -647,7 +647,8 @@ Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type : type_scope. Section lcfun. -Context {R : numDomainType} {E : NbhsLmodule.type R} {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. +Context {R : numDomainType} {E : NbhsLmodule.type R} + {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. Notation T := {linear_continuous E -> F | s}. Notation lcfun := (@lcfun _ E F s). @@ -690,21 +691,29 @@ End lcfun. (* End lcfun_realType. *) Section lcfun_linearcontinuousType. -Context {R : numDomainType} {E : NbhsLmodule.type R} {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. +Context {R : numDomainType} {E F : NbhsLmodule.type R} + {S : NbhsZmodule.type} {s : GRing.Scale.law R S} + (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}). -Lemma measurableT_comp_subproof (f : {lcfun _ >-> F}) (g : {linear_continuous E -> F | s}) : - measurable_fun setT (f \o g). -Proof. exact: measurableT_comp. Qed. +Lemma lcfun_comp_subproof1 : linear_for s (g \o f). +Proof. by move=> *; move=> */=; rewrite !linearP. Qed. -HB.instance Definition _ (f : {lcfun _ >-> F}) (g : {linear_continuous E -> F | s}) := - isMeasurableFun.Build _ _ _ _ (f \o g) (measurableT_comp_subproof _ _). +(* TODO weaken proof continuous_comp to arbitrary nbhsType *) +Lemma lcfun_comp_subproof2 : continuous (g \o f). +Proof. by move=> x; move=> A /cts_fun /cts_fun. Qed. -End lcfun_measurableType. +HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) + lcfun_comp_subproof1 lcfun_comp_subproof2. + +(* TODO: do the identity? *) + +End lcfun_linearcontinuousType. Section ring. -Context d (E : measurableType d) (F : realType). +Context {R : numDomainType} {E : NbhsLmodule.type R} + {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. -Lemma lcfun_subring_closed : subring_closed (@lcfun _ _ E F). +Lemma lcfun_submod_closed : submod_closed (@lcfun R E F s). Proof. split=> [|f g|f g]; rewrite !inE/=. - exact: measurable_cst. From d3caf2dac65dc43e233a3a07d7a071ca3c22ddb5 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 29 Jan 2025 19:29:55 +0100 Subject: [PATCH 05/16] lcfun_lmodtype and lcfun_topologicaltype - HB saturate bug - had to add a missing join --- classical/filter.v | 5 + .../pseudometric_normed_Zmodule.v | 4 +- theories/normedtype_theory/tvs.v | 282 ++++++++++++++---- 3 files changed, 227 insertions(+), 64 deletions(-) diff --git a/classical/filter.v b/classical/filter.v index 4d4c625fdf..881e098d8e 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -245,6 +245,11 @@ HB.structure Definition Nbhs := {T of Choice T & hasNbhs T}. #[short(type="pnbhsType")] HB.structure Definition PointedNbhs := {T of Pointed T & hasNbhs T}. +HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. +HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. +HB.structure Definition NbhsLmodule (K : numDomainType) := + {M of Nbhs M & GRing.Lmodule K M}. + Definition filter_from {I T : Type} (D : set I) (B : I -> set T) : set_system T := [set P | exists2 i, D i & B i `<=` P]. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index ab179df0b3..b2b2371dbe 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -124,8 +124,8 @@ Unshelve. all: by end_near. Qed. End at_left_right_topologicalType. -HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. -HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. +(*HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. +HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}.*) HB.structure Definition PreTopologicalNmodule := {M of Topological M & GRing.Nmodule M}. HB.structure Definition PreTopologicalZmodule := diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index d50cd15469..229f0851d3 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -76,8 +76,6 @@ Local Open Scope ring_scope. (* HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}. *) (* HB.structure Definition FilteredLmodule (K : numDomainType) := *) (* {M of Filtered M M & GRing.Lmodule K M}. *) -HB.structure Definition NbhsLmodule (K : numDomainType) := - {M of Nbhs M & GRing.Lmodule K M}. HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M & PreTopologicalNmodule M := { @@ -134,6 +132,10 @@ HB.instance Definition _ := HB.end. +(*HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. +HB.structure Definition UniformLmodule (K : numDomainType) := + {M of Uniform M & GRing.Lmodule K M}.*) + Section TopologicalZmoduleTheory. Variables (M : topologicalZmodType). @@ -268,6 +270,27 @@ End UniformZmoduleTheory. HB.structure Definition PreUniformLmodule (K : numDomainType) := {M of Uniform M & GRing.Lmodule K M}. +(** Due to a bug of HB.saturate, we need to define these instances +right after the definition of the topological instances **) + +(* HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. *) +(* HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. *) +(* HB.structure Definition NbhsLmodule (K : numDomainType) := *) +(* {M of Nbhs M & GRing.Lmodule K M}. *) + +(* HB.structure Definition TopologicalNmodule := *) +(* {M of Topological M & GRing.Nmodule M}. *) +(* HB.structure Definition TopologicalZmodule := *) +(* {M of Topological M & GRing.Zmodule M}. *) + +(*#[short(type="topologicalLmodType")] +HB.structure Definition TopologicalLmodule (K : numDomainType) := + {M of Topological M & GRing.Lmodule K M}.*) + +(* HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. *) +(* HB.structure Definition UniformLmodule (K : numDomainType) := *) +(* {M of Uniform M & GRing.Lmodule K M}. *) + HB.mixin Record PreUniformLmodule_isUniformLmodule (R : numFieldType) M & PreUniformLmodule R M := { scale_unif_continuous : unif_continuous (fun z : R^o * M => z.1 *: z.2) ; @@ -664,8 +687,23 @@ End Sub. Lemma lcfun_rect (K : T -> Type) : (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u. Proof. +rewrite /lcfun_Sub /lcfun /=. move=> Ksub [f [[Pf]]]/=. -Admitted. +suff -> : Pf = (set_mem (@mem_set _ [set f | _] f Pf)). +move=> flin fcont. +Fail apply: (Ksub {| + LinearContinuous.sort := f; + LinearContinuous.class := + {| + LinearContinuous.GRing_isSemiAdditive_mixin := + {| GRing.isSemiAdditive.semi_additive_subproof := set_mem (mem_set Pf) |}; + LinearContinuous.GRing_isScalable_mixin := flin; + LinearContinuous.topology_structure_isContinuous_mixin := fcont + |} + |}). +admit. +by []. +Admitted. (* No idea what's going on here *) Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _). Proof. by []. Qed. @@ -676,21 +714,12 @@ Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g. Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:]. - End lcfun. -(* Section lcfun_realType. *) -(* Context {E : sigmaRingType d} {F : realType}. *) - -(* HB.instance Definition _ := @isMeasurableFun.Build _ _ _ F *) -(* (@normr F F) (@normr_measurable F setT). *) -(* HB.instance Definition _ := *) -(* isMeasurableFun.Build _ _ _ _ (@expR F) (@measurable_expR F). *) +Section lcfun_linearcontinuousType. -(* End lcfun_realType. *) -Section lcfun_linearcontinuousType. Context {R : numDomainType} {E F : NbhsLmodule.type R} {S : NbhsZmodule.type} {s : GRing.Scale.law R S} (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}). @@ -709,72 +738,201 @@ HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) End lcfun_linearcontinuousType. -Section ring. -Context {R : numDomainType} {E : NbhsLmodule.type R} - {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. -Lemma lcfun_submod_closed : submod_closed (@lcfun R E F s). -Proof. -split=> [|f g|f g]; rewrite !inE/=. -- exact: measurable_cst. -- exact: measurable_funB. -- exact: measurable_funM. -Qed. -HB.instance Definition _ := GRing.isSubringClosed.Build _ - (@lcfun d default_measure_display E F) lcfun_subring_closed. -HB.instance Definition _ := [SubChoice_isSubComRing of {linear_continuous E -> F | s} by <:]. +Section lcfun_lmodtype. +Context {R : numDomainType} {E F : tvsType R} {s : GRing.Scale.law R F}. -Implicit Types (f g : {linear_continuous E -> F | s}). +Import GRing.Theory. -Lemma lcfun0 : (0 : {linear_continuous E -> F | s}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. -Lemma lcfun1 : (1 : {linear_continuous E -> F | s}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. -Lemma lcfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. -Lemma lcfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. -Lemma lcfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. -Lemma lcfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. -Lemma lcfun_sum I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma lcfun_prod I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma lcfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). -Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS lcfunM/= IHn. Qed. +Lemma null_fun_continuous : continuous (\0 : E -> F). +Proof. +by apply: cst_continuous. +Qed. -HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). -HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). -HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). -HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). -Definition mindic (D : set E) of measurable D : E -> F := \1_D. +Lemma null_fun_is_linear: linear_for s (\0 : E -> F). +Proof. +move => r x y /=. +rewrite addr0. +apply/esym. +Fail rewrite raddf0. +Abort. +(*Where is that defined in ssralg? I have additive and scalable, but not +linear *) + +Fail HB.instance Definition _ := @isLinearContinuous.Build R E F s (\0 : E -> F) + null_fun_is_linear null_fun_continuous. + +(* Program Definition lcfun_zmodMixin (R : numDomainType) (E F : NbhsLmodule.type R) := *) +(* @GRing.isZmodule.Build {linear_continuous E -> F} \0 (fun f x => - f x) (fun f g => f \+ g) *) +(* _ _ _ _. *) +(* Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite addrA. Qed. *) +(* Next Obligation. by move=> T M f g; rewrite funeqE=> x /=; rewrite addrC. Qed. *) +(* Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite add0r. Qed. *) +(* Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite addNr. Qed. *) +(* HB.instance Definition _ (T : Type) (M : zmodType) := fct_zmodMixin T M. *) + +(* Program Definition lcfun_lmodMixin := @GRing.Zmodule_isLmodule.Build R {linear_continuous E -> F} *) +(* (fun k f => k \*: f) _ _ _ _. *) +(* Next Obligation. by move=> k f v; rewrite funeqE=> x; exact: scalerA. Qed. *) +(* Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite scale1r. Qed. *) +(* Next Obligation. *) +(* by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr. *) +(* Qed. *) +(* Next Obligation. *) +(* by move=> f g h; rewrite funeqE => x /=; rewrite scalerDl. *) +(* Qed. *) +(* HB.instance Definition _ := lcfun_lmodMixin. *) +(* End fct_lmod. *) + +End lcfun_lmodtype. + +(* make use of {family fam, U -> V} *) + +Section test. + +Import GRing. +Context {F : numFieldType}. +Check (F : Nbhs.type). +Check (F : Zmodule.type). +(*HB.saturate F.*) (*numFieldType. *) (*hypothese : on a créé les +instances de nbhs et zmodtype sur F : numFieldType avant de créer le +join entre les deux structures *) +Check (F : NbhsZmodule.type). + +(* Section ring. *) +(* Import GRing. *) +(* Context {R : numDomainType} {E : NbhsLmodule.type R} *) +(* {F : numFieldType} {s : GRing.Scale.law R F}. *) + +(* HB.instance Definition _ := NbhsZmodule.on F. *) + +(* Lemma lcfun_submod_closed : submod_closed (@lcfun R E F s). *) +(* Proof. *) +(* split=> [|f g|f g]; rewrite !inE/=. *) +(* - exact: measurable_cst. *) +(* - exact: measurable_funB. *) +(* - exact: measurable_funM. *) +(* Qed. *) +(* HB.instance Definition _ := GRing.isSubringClosed.Build _ *) +(* (@lcfun d default_measure_display E F) lcfun_subring_closed. *) +(* HB.instance Definition _ := [SubChoice_isSubComRing of {linear_continuous E -> F | s} by <:]. *) + +(* Implicit Types (f g : {linear_continuous E -> F | s}). *) + +(* Lemma lcfun0 : (0 : {linear_continuous E -> F | s}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. *) +(* Lemma lcfun1 : (1 : {linear_continuous E -> F | s}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. *) +(* Lemma lcfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. *) +(* Lemma lcfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. *) +(* Lemma lcfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. *) +(* Lemma lcfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. *) +(* Lemma lcfun_sum I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : *) +(* (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. *) +(* Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. *) +(* Lemma lcfun_prod I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : *) +(* (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. *) +(* Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. *) +(* Lemma lcfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). *) +(* Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS lcfunM/= IHn. Qed. *) + +(* HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). *) +(* HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). *) +(* HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). *) +(* HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). *) + +(* Definition mindic (D : set E) of measurable D : E -> F := \1_D. *) + +(* Lemma mindicE (D : set E) (mD : measurable D) : *) +(* mindic mD = (fun x => (x \in D)%:R). *) +(* Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. *) + +(* HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ E F (mindic mD) *) +(* (@measurable_fun_indic _ E F setT D mD). *) + +(* Definition indic_lcfun (D : set E) (mD : measurable D) := *) +(* [the {linear_continuous E -> F | s} of mindic mD]. *) + +(* HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). *) +(* Definition scale_lcfun k f := [the {linear_continuous E -> F | s} of k \o* f]. *) + +(* Lemma max_lcfun_subproof f g : @isMeasurableFun d _ E F (f \max g). *) +(* Proof. by split; apply: measurable_maxr. Qed. *) + +(* HB.instance Definition _ f g := max_lcfun_subproof f g. *) + +(* Definition max_lcfun f g := [the {lcfun E >-> _} of f \max g]. *) + +(* End ring. *) + +End test. + +(* TODO : define bornology and topology of uniform convergence, show it's a +tvstype *) +(* Not used in the following *) +(* Class Bornology {T : Type} (B : set_system T) := { *) +(* bornoC : forall x, exists b, (B b) /\ (b x) ; *) +(* bornoU : forall P Q : set T, B P -> B Q -> B (P `|` Q) ; *) +(* bornoS : forall P Q : set T, P `<=` Q -> B Q -> B P *) +(* }. *) + +(* Global Hint Mode Bornology - ! : typeclass_instances. *) + +(* (*why with typeclasses and not with HB ? *) *) + +(*What follows is adapted from {family fam, U -> V} in +function_space.v. Should we copy instances from family fam to family_lcfun fam ? *) +Definition uniform_lcfun_family R {E : tvsType R} (F : tvsType R) (s : GRing.Scale.law R F) + (fam : set E -> Prop) := + {linear_continuous E -> F | s}. + +HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system E) := { + bornoC : forall x : E, exists b : set E, (B b) /\ (b x) ; + bornoU : forall P Q : set E, B P -> B Q -> B (P `|` Q) ; + bornoS : forall P Q : set E, P `<=` Q -> B Q -> B P + }. -Lemma mindicE (D : set E) (mD : measurable D) : - mindic mD = (fun x => (x \in D)%:R). -Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. +Reserved Notation "{ 'family_lcfun' fam , U -> V '|' s }" + (at level 0, U at level 69, format "{ 'family_lcfun' fam , U -> V | s }"). +Reserved Notation "{ 'family_lcfun' fam , U -> V }" + (at level 0, U at level 69, format "{ 'family_lcfun' fam , U -> V }"). -HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ E F (mindic mD) - (@measurable_fun_indic _ E F setT D mD). +Notation "{ 'family_lcfun' fam , U -> V '|' s }" := (@uniform_lcfun_family _ U V s fam). +Notation "{ 'family_lcfun' fam , U -> V }" := (@uniform_lcfun_family _ U V ( *:%R) fam). +(* Notation "{ 'family_lcfun' fam , F --> f '|' s }" := *) +(* (cvg_to F (@nbhs _ {family_lcfun fam, _ -> _ | _ } f)) : type_scope. *) +(* Notation "{ 'family_lcfun' fam , F --> f }" := *) +(* (cvg_to F (@nbhs _ {family_lcfun fam, _ -> _ } f)) : type_scope. *) -Definition indic_lcfun (D : set E) (mD : measurable D) := - [the {linear_continuous E -> F | s} of mindic mD]. -HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). -Definition scale_lcfun k f := [the {linear_continuous E -> F | s} of k \o* f]. +Fail HB.instance Definition _ {R} {U V : tvsType R} (s : GRing.Scale.law R V) + (fam : set U -> Prop) := + Uniform.copy {family_lcfun fam, U -> V | s} (sup_topology (fun k : sigT fam => + Uniform.class {uniform` projT1 k -> V})). -Lemma max_lcfun_subproof f g : @isMeasurableFun d _ E F (f \max g). -Proof. by split; apply: measurable_maxr. Qed. +(* HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system E) of Topological {family_lcfun B , E -> F} & GRing.Lmodule {linear_continuous E -> F} := { *) +(* bornoC : forall x : E, exists b : set E, (B b) /\ (b x) ; *) +(* bornoU : forall P Q : set E, B P -> B Q -> B (P `|` Q) ; *) +(* bornoS : forall P Q : set E, P `<=` Q -> B Q -> B P *) +(* }. *) -HB.instance Definition _ f g := max_lcfun_subproof f g. +(* HB.builders Context R E F B of UniformLinCont_isTvs R E F B. *) -Definition max_lcfun f g := [the {lcfun E >-> _} of f \max g]. -End ring. +(* (* HB.instance Definition _ := TopologicalLmod_isTvs {linearcontinuous E -> F} *) *) +(* (* entourage_filter entourage_refl *) *) +(* (* entourage_inv entourage_split_ex *) *) +(* (* nbhsE. *) *) +(* (* HB.end. *) *) +Section dual. +Context {R : numDomainType} {E : tvsType R}. +(* Reserved Notation " E ''' " (at level 80, format "E ''' "). *) -Section dual. +Notation " E ''' ":= {linear_continuous E -> R^o} (at level 80). -Definition linear_continuous (f : E -> F) : linear f /\ continuous f. +Check (E)'. +Notation " E ''' ":= {linear_continuous E -> R^o} (at level 80). End dual. From b1640667ee1baa287c53bcbde8585859efecbc75 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 7 Feb 2025 10:18:16 +0100 Subject: [PATCH 06/16] fix Co-authored-by: Reynald Affeldt --- theories/normedtype_theory/tvs.v | 57 ++++++++++++++++++-------------- 1 file changed, 33 insertions(+), 24 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 229f0851d3..864289ba80 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -738,7 +738,6 @@ HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) End lcfun_linearcontinuousType. - Section lcfun_lmodtype. Context {R : numDomainType} {E F : tvsType R} {s : GRing.Scale.law R F}. @@ -749,28 +748,39 @@ Proof. by apply: cst_continuous. Qed. +Lemma it_is_additive r : @Algebra.isNmodMorphism F F (s r). +Proof. +split. +by apply: GRing.Scale.op_nmod_morphism. +Qed. + +Fail Check (s 0 : {additive F -> F}). + +HB.instance Definition _ r := it_is_additive r. + +Check (s 0 : {additive F -> F}). Lemma null_fun_is_linear: linear_for s (\0 : E -> F). Proof. move => r x y /=. -rewrite addr0. -apply/esym. -Fail rewrite raddf0. -Abort. -(*Where is that defined in ssralg? I have additive and scalable, but not -linear *) - -Fail HB.instance Definition _ := @isLinearContinuous.Build R E F s (\0 : E -> F) - null_fun_is_linear null_fun_continuous. - -(* Program Definition lcfun_zmodMixin (R : numDomainType) (E F : NbhsLmodule.type R) := *) -(* @GRing.isZmodule.Build {linear_continuous E -> F} \0 (fun f x => - f x) (fun f g => f \+ g) *) -(* _ _ _ _. *) -(* Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite addrA. Qed. *) -(* Next Obligation. by move=> T M f g; rewrite funeqE=> x /=; rewrite addrC. Qed. *) -(* Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite add0r. Qed. *) -(* Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite addNr. Qed. *) -(* HB.instance Definition _ (T : Type) (M : zmodType) := fct_zmodMixin T M. *) +by rewrite raddf0 addr0. +Qed. + +HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous. + +Check (\0 : {linear_continuous E -> F}). + +(* Fail HB.instance Definition _ := @isLinearContinuous.Build R E F s (\0 : E -> F) *) +(* null_fun_is_linear null_fun_continuous. *) + +Fail Program Definition lcfun_zmodMixin (R : numDomainType) (E F : tvsType R):= + @GRing.isZmodule.Build {linear_continuous E -> F} (\0 : {linear_continuous E -> F}) (fun f x => - f x) (fun f g => f \+ g) + _ _ _ _. +(*Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite addrA. Qed. +Next Obligation. by move=> T M f g; rewrite funeqE=> x /=; rewrite addrC. Qed. +Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite add0r. Qed. +Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite addNr. Qed. +HB.instance Definition _ (T : Type) (M : zmodType) := fct_zmodMixin T M.*) (* Program Definition lcfun_lmodMixin := @GRing.Zmodule_isLmodule.Build R {linear_continuous E -> F} *) (* (fun k f => k \*: f) _ _ _ _. *) @@ -903,11 +913,10 @@ Notation "{ 'family_lcfun' fam , U -> V }" := (@uniform_lcfun_family _ U V ( *: (* Notation "{ 'family_lcfun' fam , F --> f }" := *) (* (cvg_to F (@nbhs _ {family_lcfun fam, _ -> _ } f)) : type_scope. *) - -Fail HB.instance Definition _ {R} {U V : tvsType R} (s : GRing.Scale.law R V) - (fam : set U -> Prop) := - Uniform.copy {family_lcfun fam, U -> V | s} (sup_topology (fun k : sigT fam => - Uniform.class {uniform` projT1 k -> V})). +(* HB.instance Definition _ {R} {U V : tvsType R} (s : GRing.Scale.law R V) *) +(* (fam : set U -> Prop) := *) +(* Uniform.copy {family_lcfun fam, U -> V | s} (sup_topology (fun k : sigT fam => *) +(* Uniform.class {uniform` projT1 k -> V})). *) (* HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system E) of Topological {family_lcfun B , E -> F} & GRing.Lmodule {linear_continuous E -> F} := { *) (* bornoC : forall x : E, exists b : set E, (B b) /\ (b x) ; *) From c1f78ca6af4a4ee95d2ce748022bf35ca0be3437 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 10 Feb 2025 11:16:33 +0100 Subject: [PATCH 07/16] wip --- theories/derive.v | 28 +++--- theories/normedtype_theory/tvs.v | 164 ++++++++++++++++++++++--------- theories/numfun.v | 10 +- theories/sequences.v | 2 +- 4 files changed, 138 insertions(+), 66 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index b0862eb08c..207f63cf22 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -322,9 +322,9 @@ evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first. rewrite funeqE=> h. by rewrite -[_ - _]addrA addrC subrKA scalerDr addrC linearZ scalerA /g. apply: cvg_lim => //. -pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v. -pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ). -rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD. +pose g1 := fun h => (h^-1 * h) *: 'd f a v. +pose g2 := fun h : R => h^-1 *: k (h *: v ). +rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: pseudometric_normed_Zmodule.cvgD. rewrite -(scale1r (_ _ v)); apply: cvgZr_tmp => /= X [e e0]. rewrite /ball_ /= => eX. apply/nbhs_ballP. @@ -415,7 +415,7 @@ Fact dadd (f g : V -> W) x : continuous ('d f x \+ 'd g x) /\ (f + g) \o shift x = cst ((f + g) x) + ('d f x \+ 'd g x) +o_ 0 id. Proof. -move=> df dg; split => [?|]; do ?exact: continuousD. +move=> df dg; split => [?|]; do ?exact: normed_module.continuousD. apply/(@eqaddoE R); rewrite funeqE => y /=. by rewrite !fctE ![_ (_ + x)]diff_locallyx// addrACA addox addrACA. Qed. @@ -424,7 +424,7 @@ Fact dopp (f : V -> W) x : differentiable f x -> continuous (- ('d f x : V -> W)) /\ (- f) \o shift x = cst (- f x) \- 'd f x +o_ 0 id. Proof. -move=> df; split; first by move=> ?; apply: continuousN. +move=> df; split; first by move=> ?; apply: normed_module.continuousN. apply/eqaddoE; rewrite funeqE => y /=. by rewrite -[(- f) _]/(- (_ _)) diff_locallyx// !opprD oppox. Qed. @@ -820,7 +820,7 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : (fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id. Proof. move=> fc; split=> [q|]. - by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2)); + by apply: (@normed_module.continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2)); move=> A /(fc (_.1, _.2)) /= /nbhs_ballP [_ /posnumP[e] fpqe_A]; apply/nbhs_ballP; exists e%:num => //= r [? ?]; exact: (fpqe_A (_.1, _.2)). apply/eqaddoE; rewrite funeqE => q /=. @@ -1130,7 +1130,7 @@ move=> df dg. evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=; last first. rewrite funeqE => h. by rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr /fg. -exact: cvgD. +exact: pseudometric_normed_Zmodule.cvgD. Qed. Lemma deriveD f g (x v : V) : derivable f x v -> derivable g x v -> @@ -1286,7 +1286,7 @@ evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first. by rewrite !scalerBr -addrA ![g x *: _]mulrC addKr. rewrite scalerDr scalerA mulrC -scalerA. by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg. -apply: cvgD; last exact: cvgZl_tmp df. +apply: pseudometric_normed_Zmodule.cvgD; last exact: cvgZl_tmp df. apply: cvg_comp2 (@scale_continuous _ _ (_, _)) => /=; last exact: dg. suff : {for 0, continuous (fun h : R => f(h *: v + x))}. by move=> /continuous_withinNx; rewrite scale0r add0r. @@ -1447,7 +1447,7 @@ pose g t : R := (sup (f @` A) - f t)^-1. have invf_continuous : {within A, continuous g}. rewrite continuous_subspace_in => t tA; apply: cvgV => //=. by rewrite subr_eq0 gt_eqF// AfsupfA//; rewrite inE in tA. - by apply: cvgD; [exact: cst_continuous | apply: cvgN; exact: cf]. + by apply: pseudometric_normed_Zmodule.cvgD; [exact: cst_continuous | apply: cvgN; exact: cf]. have /ex_strict_bound_gt0[k k_gt0 /= imVfltk] : bounded_set (g @` A). exact/compact_bounded/continuous_compact. have [_ [t tA <-]] : exists2 y, (f @` A) y & sup (f @` A) - k^-1 < y. @@ -1465,7 +1465,7 @@ Lemma compact_EVT_min (T : topologicalType) (R : realType) (f : T -> R) Proof. move=> A0 cA cf. have /(compact_EVT_max A0 cA)[c cinA fcmin] : {within A, continuous (- f)}. - by move=> ?; apply: continuousN => ?; exact: cf. + by move=> ?; apply: normed_module.continuousN => ?; exact: cf. by exists c => // t tA; rewrite -lerN2 fcmin. Qed. @@ -1604,8 +1604,8 @@ set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)). have gdrvbl x : x \in `]a, b[%R -> derivable g x 1. by move=> /fdrvbl dfx; apply/derivableB/derivable1_diffP. have gcont : {within `[a, b], continuous g}. - move=> x; apply: continuousD _ ; first exact: fcont. - exact/continuousN/continuous_subspaceT/scalel_continuous. + move=> x; apply: normed_module.continuousD _ ; first exact: fcont. + exact/normed_module.continuousN/continuous_subspaceT/scalel_continuous. have gaegb : g a = g b. rewrite /g -![(_ - _ : _ -> _) _]/(_ - _). apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl. @@ -1690,7 +1690,7 @@ apply: ger0_derive1_le. - move => x xab; exact/derivableN/df. - move => x xab; rewrite derive1E deriveN; last exact: df. by rewrite -derive1E oppr_ge0 dfle0. -by move=> x; exact/continuousN/cf. +by move=> x; exact/normed_module.continuousN/cf. Qed. Lemma ler0_derive1_le_cc :{within `[a, b], continuous f} -> @@ -1797,7 +1797,7 @@ apply: gtr0_derive1_lt. - move => x xab; exact/derivableN/df. - move => x xab; rewrite derive1E deriveN; last exact: df. by rewrite -derive1E oppr_gt0 dflt0. -by move=> x; exact/continuousN/cf. +by move=> x; exact/normed_module.continuousN/cf. Qed. Lemma ltr0_derive1_lt_cc : {within `[a, b], continuous f} -> diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 864289ba80..954e1b27bc 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -656,6 +656,7 @@ Context {K : numDomainType} {E : NbhsLmodule.type K} {F : NbhsZmodule.type} {s Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ]. Definition lcfun_key : pred_key lcfun. Proof. exact. Qed. Canonical lcfun_keyed := KeyedPred lcfun_key. + End lcfun_pred. Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'" @@ -669,6 +670,7 @@ Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%typ Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R} : type_scope. + Section lcfun. Context {R : numDomainType} {E : NbhsLmodule.type R} {F : NbhsZmodule.type} {s : GRing.Scale.law R F}. @@ -687,23 +689,25 @@ End Sub. Lemma lcfun_rect (K : T -> Type) : (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u. Proof. -rewrite /lcfun_Sub /lcfun /=. -move=> Ksub [f [[Pf]]]/=. -suff -> : Pf = (set_mem (@mem_set _ [set f | _] f Pf)). -move=> flin fcont. -Fail apply: (Ksub {| - LinearContinuous.sort := f; - LinearContinuous.class := - {| - LinearContinuous.GRing_isSemiAdditive_mixin := - {| GRing.isSemiAdditive.semi_additive_subproof := set_mem (mem_set Pf) |}; - LinearContinuous.GRing_isScalable_mixin := flin; - LinearContinuous.topology_structure_isContinuous_mixin := fcont - |} - |}). -admit. -by []. -Admitted. (* No idea what's going on here *) +move=> Ksub [f [[Pf1] [Pf2] [Pf3]]]. +set G := (G in K G). +have Pf : f \in lcfun. + by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2. +suff -> : G = lcfun_Sub Pf by apply: Ksub. +rewrite {}/G. +congr LinearContinuous.Pack. +congr LinearContinuous.Class. +- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance. +- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance. +- by congr isContinuous.Axioms_; apply: Prop_irrelevance. +Qed. + +(* Lemma lcfun_elim (K : ( E -> F) -> Type) : *) +(* ( forall u : T, K u) -> (forall f (Pf : f \in lcfun), K f). *) +(* Proof. *) +(* Admitted. (* HB.pack*) *) (* marche pas bien avec la tactique elim *) + + Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _). Proof. by []. Qed. @@ -716,8 +720,24 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:]. End lcfun. +Variant lcfun_spec (R : numDomainType) (E : tvsType R) (F : tvsType R) (f : E -> F) : + (E -> F) -> bool -> Type := + | Islcfun (l : {linear_continuous E -> F}) : lcfun_spec f (l) true. + +Check posnumP. + +(*to be renamed ?*) +Lemma lcfunE (R : numDomainType) (E : tvsType R) (F : tvsType R) (s : GRing.Scale.law R F) + (f : E -> F) : + (f \in (@lcfun R E F s) ) -> + lcfun_spec f f (f \in (@lcfun R E F s)). +Proof. + move=> f_lc. have -> : (f \in lcfun) = true. admit. + have {2}-> :(f = (@lcfun_Sub R E F s f f_lc)) by rewrite lcfun_valP. + Fail constructor. +Admitted. -Section lcfun_linearcontinuousType. +Section lcfun_comp. Context {R : numDomainType} {E F : NbhsLmodule.type R} @@ -736,10 +756,12 @@ HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) (* TODO: do the identity? *) -End lcfun_linearcontinuousType. +End lcfun_comp. Section lcfun_lmodtype. -Context {R : numDomainType} {E F : tvsType R} {s : GRing.Scale.law R F}. +Context {R : numFieldType} {E F G: tvsType R} {s : GRing.Scale.law R F}. + +Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}). Import GRing.Theory. @@ -768,35 +790,85 @@ Qed. HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous. -Check (\0 : {linear_continuous E -> F}). - -(* Fail HB.instance Definition _ := @isLinearContinuous.Build R E F s (\0 : E -> F) *) -(* null_fun_is_linear null_fun_continuous. *) - -Fail Program Definition lcfun_zmodMixin (R : numDomainType) (E F : tvsType R):= - @GRing.isZmodule.Build {linear_continuous E -> F} (\0 : {linear_continuous E -> F}) (fun f x => - f x) (fun f g => f \+ g) - _ _ _ _. -(*Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite addrA. Qed. -Next Obligation. by move=> T M f g; rewrite funeqE=> x /=; rewrite addrC. Qed. -Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite add0r. Qed. -Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite addNr. Qed. -HB.instance Definition _ (T : Type) (M : zmodType) := fct_zmodMixin T M.*) - -(* Program Definition lcfun_lmodMixin := @GRing.Zmodule_isLmodule.Build R {linear_continuous E -> F} *) -(* (fun k f => k \*: f) _ _ _ _. *) -(* Next Obligation. by move=> k f v; rewrite funeqE=> x; exact: scalerA. Qed. *) -(* Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite scale1r. Qed. *) -(* Next Obligation. *) -(* by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr. *) -(* Qed. *) -(* Next Obligation. *) -(* by move=> f g h; rewrite funeqE => x /=; rewrite scalerDl. *) -(* Qed. *) -(* HB.instance Definition _ := lcfun_lmodMixin. *) -(* End fct_lmod. *) +Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. + +(* NB TODO: move section cvg_composition_pseudometric in normedtype.v here, to generalize it on tvstype *) +(*Next lemmas are duplicates *) + +Lemma cvgD (U : set_system E) {FF : Filter U} f g a b : f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. +Proof. +move=> fa ga. +apply: continuous2_cvg; [|by []..]. +apply @add_continuous. (* TODO: c'est louche d'avoir besoin du @ *) +Qed. + +Lemma continuousD f g : continuous (f \+ g). +Proof. by move=> /= x; apply: cvgD; apply: cts_fun. Qed. + +Lemma continuousN f : continuous (\- f). +Proof. +Admitted. + +HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@continuousD f g). + +Lemma cvgZ (U : set_system E) {FF : Filter U} l f r a : l @ U --> r -> f @ U --> a -> + l x *: f x @[x --> U] --> r *: a. +Proof. move=> ? ?; apply: continuous2_cvg => //. Fail apply: scale_continuous. +Admitted. (* weird, normedtype uses "apply scale_continuous" which leads to infinite computation here *) + +Lemma cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a. +Proof. apply: cvgZ => //; exact: cvg_cst. Qed. + +Lemma continuousM r g : continuous (r \*: g). +Proof. by move=> /= x; apply: cvgZr; apply: cts_fun. Qed. + +HB.instance Definition _ r g := isContinuous.Build E F (r \*: g) (@continuousM r g). + +Lemma continuousB f : continuous (\- f). +Proof. +Admitted. + +HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousB f). + +Lemma add_fun_is_linear f g : linear (f \+ g). +Proof. +Admitted. + +HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousN f). + +(* Context (f g : {linear_continuous E -> F}) (r : R). *) +(* Check (r \*: f \+ g : {linear_continuous E -> F}). *) + +Lemma lcfun_submod_closed : submod_closed (@lcfun R E F s). +Proof. + split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous. + move=> r /= _ _ /lcfunE[f] /lcfunE[g]. +(* rewrite !inE /= => [[lf cf] [lg cg]]; split.*) + (* HB pack et subst *) (* move => l u v. apply/linearP.*) + rewrite inE /=; split. + Fail apply: (@GRing.add_fun_is_semi_additive E F ( s r f) g). + Fail apply: add_fun_is_linear. + move => l a b. + rewrite /= ?raddf0 ?addr0// !raddfD /=. + Fail rewrite (@raddfD _ _ (r \*: f \+ g) (l *: a) b). + rewrite addrCA -!addrA addrCA /=. Check linearZ_LR. Check (@linearZ_LR R E F _ ((r \*: f + g)) l a). + Fail rewrite -[s]/(GRing.scale). + Unset Printing Notations. + admit. + apply: continuousD. +Admitted. + +HB.instance Definition _ := + @GRing.isSubmodClosed.Build _ _ lcfun lcfun_submod_closed. + +HB.instance Definition _ := + [SubChoice_isSubLmodule of {linear_continuous E -> F | s} by <:]. + +Check {linear_continuous E -> F |s } : lmodType _ . End lcfun_lmodtype. + (* make use of {family fam, U -> V} *) Section test. diff --git a/theories/numfun.v b/theories/numfun.v index d56e400fbf..998e5c7004 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1095,10 +1095,10 @@ move=> cA cB A0 xy; move/normal_separatorP : normalX => urysohn_ext. have /(@uniform_separatorP _ R)[f [cf f01 f0 f1]] := urysohn_ext R _ _ cA cB A0. pose g : X -> R := line_path x y \o f; exists g; split; rewrite /g /=. move=> t; apply: continuous_comp; first exact: cf. - apply: (@continuousD R R^o). - apply: continuousM; last exact: cvg_cst. - by apply: (@continuousB R R^o) => //; exact: cvg_cst. - by apply: continuousM; [exact: cvg_id|exact: cvg_cst]. + apply: (@normed_module.continuousD R R^o). + apply: normed_module.continuousM; last exact: cvg_cst. + by apply: (@normed_module.continuousB R R^o) => //; exact: cvg_cst. + by apply: normed_module.continuousM; [exact: cvg_id|exact: cvg_cst]. - by rewrite -image_comp => z /= [? /f0 -> <-]; rewrite line_path0. - by rewrite -image_comp => z /= [? /f1 -> <-]; rewrite line_path1. - rewrite -image_comp; apply: (subset_trans (image_subset _ f01)). @@ -1224,7 +1224,7 @@ exists (lim (h_ @ \oo)); split. near_simpl; apply: nearW; elim. by rewrite /h_ /series /= big_geq// => ?; exact: cvg_cst. move=> n; rewrite /h_ /series /= big_nat_recr /= // => IH t. - by apply: continuousD; [exact: IH|exact: g_cts]. + by apply: normed_module.continuousD; [exact: IH|exact: g_cts]. - move=> t. have /pointwise_cvgP/(_ t)/(cvg_lim (@Rhausdorff _)) := [elaborate pointwise_uniform_cvg _ cvgh]. diff --git a/theories/sequences.v b/theories/sequences.v index d7bca62318..a7e2f5b350 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -837,7 +837,7 @@ suff abel : forall n, rewrite -(add0r l). rewrite (_ : u_ = u_ - arithmetic_mean u_ + arithmetic_mean u_); last first. by rewrite funeqE => n; rewrite subrK. - exact: cvgD. + exact: pseudometric_normed_Zmodule.cvgD. rewrite (_ : _ - arithmetic_mean u_ = (fun n => \sum_(1 <= k < n.+1) k%:R / n.+1%:R * a_ k.-1)); last first. by rewrite funeqE. From 94acc80f4fc6826fd3a6f547b77a3231eb1540cc Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 9 Apr 2025 17:35:20 +0200 Subject: [PATCH 08/16] end lcfun_lmodtype Co-authored-by: Cyril Cohen --- theories/normedtype_theory/tvs.v | 95 ++++++++++++++------------------ 1 file changed, 40 insertions(+), 55 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 954e1b27bc..606af80fb8 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -531,7 +531,6 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//. by near: z; near: M; exact: (@cvg_bounded _ R^o _ _ _ _ _ (@cvg_refl _ _)). 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 : @@ -635,7 +634,7 @@ End prod_Tvs. HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) - (F : NbhsZmodule.type) s := + (F : NbhsZmodule.type) (s : K -> F -> F) := {f of @GRing.Linear K E F s f & @Continuous E F f }. HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) @@ -669,7 +668,6 @@ Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%typ : type_scope. Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R} : type_scope. - Section lcfun. Context {R : numDomainType} {E : NbhsLmodule.type R} @@ -702,13 +700,6 @@ congr LinearContinuous.Class. - by congr isContinuous.Axioms_; apply: Prop_irrelevance. Qed. -(* Lemma lcfun_elim (K : ( E -> F) -> Type) : *) -(* ( forall u : T, K u) -> (forall f (Pf : f \in lcfun), K f). *) -(* Proof. *) -(* Admitted. (* HB.pack*) *) (* marche pas bien avec la tactique elim *) - - - Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _). Proof. by []. Qed. @@ -718,28 +709,21 @@ Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g. Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:]. -End lcfun. - -Variant lcfun_spec (R : numDomainType) (E : tvsType R) (F : tvsType R) (f : E -> F) : - (E -> F) -> bool -> Type := - | Islcfun (l : {linear_continuous E -> F}) : lcfun_spec f (l) true. -Check posnumP. +Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type := + | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true. (*to be renamed ?*) -Lemma lcfunE (R : numDomainType) (E : tvsType R) (F : tvsType R) (s : GRing.Scale.law R F) - (f : E -> F) : - (f \in (@lcfun R E F s) ) -> - lcfun_spec f f (f \in (@lcfun R E F s)). -Proof. - move=> f_lc. have -> : (f \in lcfun) = true. admit. - have {2}-> :(f = (@lcfun_Sub R E F s f f_lc)) by rewrite lcfun_valP. - Fail constructor. -Admitted. +Lemma lcfunE (f : E -> F) : (f \in lcfun) -> lcfun_spec f f (f \in lcfun). +Proof. +move=> /[dup] f_lc ->. +have {2}-> :(f = (lcfun_Sub f_lc)) by rewrite lcfun_valP. +constructor. +Qed. +End lcfun. Section lcfun_comp. - Context {R : numDomainType} {E F : NbhsLmodule.type R} {S : NbhsZmodule.type} {s : GRing.Scale.law R S} (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}). @@ -755,11 +739,11 @@ HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) lcfun_comp_subproof1 lcfun_comp_subproof2. (* TODO: do the identity? *) - End lcfun_comp. Section lcfun_lmodtype. -Context {R : numFieldType} {E F G: tvsType R} {s : GRing.Scale.law R F}. + Context {R : numFieldType} {E F G: tvsType R}. + (* {s : GRing.Scale.law R F}. *) Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}). @@ -770,6 +754,7 @@ Proof. by apply: cst_continuous. Qed. +(* Lemma it_is_additive r : @Algebra.isNmodMorphism F F (s r). Proof. split. @@ -787,13 +772,16 @@ Proof. move => r x y /=. by rewrite raddf0 addr0. Qed. +*) HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous. Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. -(* NB TODO: move section cvg_composition_pseudometric in normedtype.v here, to generalize it on tvstype *) -(*Next lemmas are duplicates *) +(* NB TODO: move section cvg_composition_pseudometric in normedtype.v here, to +generalize it on tvstype *) +(* Next lemmas are duplicates *) +(* TODO once PR1544 is merged *) Lemma cvgD (U : set_system E) {FF : Filter U} f g a b : f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. Proof. @@ -813,8 +801,9 @@ HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@continuousD f Lemma cvgZ (U : set_system E) {FF : Filter U} l f r a : l @ U --> r -> f @ U --> a -> l x *: f x @[x --> U] --> r *: a. -Proof. move=> ? ?; apply: continuous2_cvg => //. Fail apply: scale_continuous. -Admitted. (* weird, normedtype uses "apply scale_continuous" which leads to infinite computation here *) +Proof. +move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)). +Qed. Lemma cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a. Proof. apply: cvgZ => //; exact: cvg_cst. Qed. @@ -824,24 +813,9 @@ Proof. by move=> /= x; apply: cvgZr; apply: cts_fun. Qed. HB.instance Definition _ r g := isContinuous.Build E F (r \*: g) (@continuousM r g). -Lemma continuousB f : continuous (\- f). -Proof. -Admitted. - -HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousB f). - -Lemma add_fun_is_linear f g : linear (f \+ g). -Proof. -Admitted. - -HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousN f). - -(* Context (f g : {linear_continuous E -> F}) (r : R). *) -(* Check (r \*: f \+ g : {linear_continuous E -> F}). *) - -Lemma lcfun_submod_closed : submod_closed (@lcfun R E F s). +Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R). Proof. - split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous. +(* split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous. move=> r /= _ _ /lcfunE[f] /lcfunE[g]. (* rewrite !inE /= => [[lf cf] [lg cg]]; split.*) (* HB pack et subst *) (* move => l u v. apply/linearP.*) @@ -855,20 +829,31 @@ Proof. Fail rewrite -[s]/(GRing.scale). Unset Printing Notations. admit. - apply: continuousD. -Admitted. + apply: continuousD.*) +split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous. +move=> r /= _ _ /lcfunE[f] /lcfunE[g]. +by rewrite inE /=; split; [exact: linearP | exact: continuousD]. +Qed. + +(*HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousB f).*) + +Lemma add_fun_is_linear f g : linear (f \+ g). +Proof. +Admitted. + +HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousN f). + +(* Context (f g : {linear_continuous E -> F}) (r : R). *) +(* Check (r \*: f \+ g : {linear_continuous E -> F}). *) HB.instance Definition _ := @GRing.isSubmodClosed.Build _ _ lcfun lcfun_submod_closed. HB.instance Definition _ := - [SubChoice_isSubLmodule of {linear_continuous E -> F | s} by <:]. - -Check {linear_continuous E -> F |s } : lmodType _ . + [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:]. End lcfun_lmodtype. - (* make use of {family fam, U -> V} *) Section test. From 7e40efda666dbba87811f362700e616cd4889b50 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 10 Apr 2025 13:58:38 +0200 Subject: [PATCH 09/16] wip, notations --- theories/normedtype_theory/tvs.v | 115 +++++++++++++++++++------------ 1 file changed, 72 insertions(+), 43 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 606af80fb8..c3231cc940 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -57,6 +57,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (******************************************************************************) Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *) + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -783,35 +784,36 @@ generalize it on tvstype *) (* Next lemmas are duplicates *) (* TODO once PR1544 is merged *) -Lemma cvgD (U : set_system E) {FF : Filter U} f g a b : f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. +Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b : + f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. Proof. move=> fa ga. apply: continuous2_cvg; [|by []..]. apply @add_continuous. (* TODO: c'est louche d'avoir besoin du @ *) Qed. -Lemma continuousD f g : continuous (f \+ g). -Proof. by move=> /= x; apply: cvgD; apply: cts_fun. Qed. +Lemma lcfun_continuousD f g : continuous (f \+ g). +Proof. by move=> /= x; apply: lcfun_cvgD; apply: cts_fun. Qed. -Lemma continuousN f : continuous (\- f). +Lemma lcfun_continuousN f : continuous (\- f). Proof. Admitted. -HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@continuousD f g). +HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g). -Lemma cvgZ (U : set_system E) {FF : Filter U} l f r a : l @ U --> r -> f @ U --> a -> +Lemma lcfun_cvgZ (U : set_system E) {FF : Filter U} l f r a : l @ U --> r -> f @ U --> a -> l x *: f x @[x --> U] --> r *: a. Proof. move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)). Qed. -Lemma cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a. -Proof. apply: cvgZ => //; exact: cvg_cst. Qed. +Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a. +Proof. apply: lcfun_cvgZ => //; exact: cvg_cst. Qed. -Lemma continuousM r g : continuous (r \*: g). -Proof. by move=> /= x; apply: cvgZr; apply: cts_fun. Qed. +Lemma lcfun_continuousM r g : continuous (r \*: g). +Proof. by move=> /= x; apply: lcfun_cvgZr; apply: cts_fun. Qed. -HB.instance Definition _ r g := isContinuous.Build E F (r \*: g) (@continuousM r g). +HB.instance Definition _ r g := isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g). Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R). Proof. @@ -830,9 +832,9 @@ Proof. Unset Printing Notations. admit. apply: continuousD.*) -split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous. +split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous. move=> r /= _ _ /lcfunE[f] /lcfunE[g]. -by rewrite inE /=; split; [exact: linearP | exact: continuousD]. +by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD]. Qed. (*HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousB f).*) @@ -841,7 +843,7 @@ Lemma add_fun_is_linear f g : linear (f \+ g). Proof. Admitted. -HB.instance Definition _ f := isContinuous.Build E F (\- f) (@continuousN f). +HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f). (* Context (f g : {linear_continuous E -> F}) (r : R). *) (* Check (r \*: f \+ g : {linear_continuous E -> F}). *) @@ -852,6 +854,7 @@ HB.instance Definition _ := HB.instance Definition _ := [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:]. +Check ({linear_continuous E -> F} : lmodType R). End lcfun_lmodtype. (* make use of {family fam, U -> V} *) @@ -948,34 +951,60 @@ tvstype *) (*What follows is adapted from {family fam, U -> V} in function_space.v. Should we copy instances from family fam to family_lcfun fam ? *) -Definition uniform_lcfun_family R {E : tvsType R} (F : tvsType R) (s : GRing.Scale.law R F) - (fam : set E -> Prop) := - {linear_continuous E -> F | s}. - -HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system E) := { - bornoC : forall x : E, exists b : set E, (B b) /\ (b x) ; - bornoU : forall P Q : set E, B P -> B Q -> B (P `|` Q) ; - bornoS : forall P Q : set E, P `<=` Q -> B Q -> B P - }. - -Reserved Notation "{ 'family_lcfun' fam , U -> V '|' s }" - (at level 0, U at level 69, format "{ 'family_lcfun' fam , U -> V | s }"). -Reserved Notation "{ 'family_lcfun' fam , U -> V }" - (at level 0, U at level 69, format "{ 'family_lcfun' fam , U -> V }"). +Definition uniform_lcfun_family R {E : tvsType R} (F : tvsType R) (fam : set E -> Prop) : Type := + {linear_continuous E -> F}. -Notation "{ 'family_lcfun' fam , U -> V '|' s }" := (@uniform_lcfun_family _ U V s fam). -Notation "{ 'family_lcfun' fam , U -> V }" := (@uniform_lcfun_family _ U V ( *:%R) fam). +(* Reserved Notation "'{' 'family_lcfun' fam , U '->' V '|' s '}'" *) +(* (at level 0, U at level 98, V at level 99, *) +(* format "{ 'family_lcfun' fam , U -> V | s }"). *) +Reserved Notation "'{' 'family_lcfun' fam , U '->' V '}'" + (at level 0, U at level 98, V at level 99, + format "{ 'family_lcfun' fam , U -> V }"). +(* Reserved Notation "'{' 'family_lcfun' fam , F '-->' f '|' s '}'" *) +(* (at level 0, F at level 98, f at level 99, *) +(* format "{ 'family_lcfun' fam , F --> f | s }"). *) +Reserved Notation "'{' 'family_lcfun' fam , F '-->' f '}'" + (at level 0, F at level 98, f at level 99, + format "{ 'family_lcfun' fam , F --> f }"). +(* Notation "{ 'family_lcfun' fam , U -> V '|' s }" := (@uniform_lcfun_family _ U V s fam). *) +Notation "{ 'family_lcfun' fam , U -> V }" := (@uniform_lcfun_family _ U V fam). (* Notation "{ 'family_lcfun' fam , F --> f '|' s }" := *) -(* (cvg_to F (@nbhs _ {family_lcfun fam, _ -> _ | _ } f)) : type_scope. *) -(* Notation "{ 'family_lcfun' fam , F --> f }" := *) -(* (cvg_to F (@nbhs _ {family_lcfun fam, _ -> _ } f)) : type_scope. *) +(* (cvg_to F (@nbhs _ {family_lcfun fam , _ -> _ | _ } f)) : type_scope. *) + +Notation "{ 'family_lcfun' fam , F --> f }" := + (cvg_to F (@nbhs _ {family_lcfun fam, _ -> _ } f)) : type_scope. + +(* we can´t use unfiorm, it is defined on E -> F and not on our space. We need to define it on {linear_continuous E -> F} , inducing its topology from uniform` E- > F *) + +Locate sup_topology. +Search (continuousType _ _). Locate continuousEP. + +(** examples **) +(* HB.instance Definition _ (U : Type) (T : U -> topologicalType) := *) +(* Topological.copy (forall x : U, T x) (prod_topology T). *) + +(* HB.instance Definition _ (U : Type) (T : U -> uniformType) := *) +(* Uniform.copy (forall x : U, T x) (prod_topology T). *) + +(* HB.instance Definition _ (U T : topologicalType) := *) +(* Topological.copy *) +(* (continuousType U T) *) +(* (weak_topology (id : continuousType U T -> (U -> T))). *) + +(* HB.instance Definition _ (U : topologicalType) (T : uniformType) := *) +(* Uniform.copy *) +(* (continuousType U T) *) +(* (weak_topology (id : continuousType U T -> (U -> T))). *) + +(* HB.instance Definition _ R {E : tvsType R} (F : tvsType R) (fam : set E -> Prop) := *) +(* Topological.copy {family_lcfun fam, E -> F} (sup_topology (fun k : sigT fam => *) +(* Uniform.class {uniform` projT1 k -> F})). *) -(* HB.instance Definition _ {R} {U V : tvsType R} (s : GRing.Scale.law R V) *) -(* (fam : set U -> Prop) := *) -(* Uniform.copy {family_lcfun fam, U -> V | s} (sup_topology (fun k : sigT fam => *) -(* Uniform.class {uniform` projT1 k -> V})). *) +(* HB.instance Definition _ {R} {U V : tvsType R} (fam : set U -> Prop) := *) +(* Uniform.copy {family_lcfun fam, U -> V} (sup_topology (fun k : sigT fam => *) +(* Uniform.class {uniform` projT1 k -> V})). *) -(* HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system E) of Topological {family_lcfun B , E -> F} & GRing.Lmodule {linear_continuous E -> F} := { *) +(* HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system E) of Topological {family_lcfun B , E -> F} & GRing.Lmodule {linear_continuous E -> F } := { *) (* bornoC : forall x : E, exists b : set E, (B b) /\ (b x) ; *) (* bornoU : forall P Q : set E, B P -> B Q -> B (P `|` Q) ; *) (* bornoS : forall P Q : set E, P `<=` Q -> B Q -> B P *) @@ -984,11 +1013,11 @@ Notation "{ 'family_lcfun' fam , U -> V }" := (@uniform_lcfun_family _ U V ( *: (* HB.builders Context R E F B of UniformLinCont_isTvs R E F B. *) -(* (* HB.instance Definition _ := TopologicalLmod_isTvs {linearcontinuous E -> F} *) *) -(* (* entourage_filter entourage_refl *) *) -(* (* entourage_inv entourage_split_ex *) *) -(* (* nbhsE. *) *) -(* (* HB.end. *) *) +(* HB.instance Definition _ := TopologicalLmod_isTvs {linearcontinuous E -> F} *) +(* entourage_filter entourage_refl *) +(* entourage_inv entourage_split_ex *) +(* nbhsE. *) +(* HB.end. *) Section dual. From aed91e5540107c730e3d0a2f346d55d4fb1f81c5 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 11 Apr 2025 14:27:44 +0200 Subject: [PATCH 10/16] change name to ConvexTvs and ctvs --- theories/normedtype_theory/normed_module.v | 6 +-- theories/normedtype_theory/tvs.v | 44 ++++++++++++++-------- 2 files changed, 32 insertions(+), 18 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index ed44d718e2..5477f31a20 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -77,13 +77,13 @@ Local Open Scope ring_scope. (** Modules with a norm depending on a numDomain *) HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V - & PseudoMetricNormedZmod K V & Tvs K V := { + & PseudoMetricNormedZmod K V & ConvexTvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := - {T of PseudoMetricNormedZmod K T & Tvs K T + {T of PseudoMetricNormedZmod K T & ConvexTvs K T & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V @@ -146,7 +146,7 @@ HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous. -HB.instance Definition _ := Uniform_isTvs.Build K V locally_convex. +HB.instance Definition _ := Uniform_isConvexTvs.Build K V locally_convex. HB.instance Definition _ := PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index c3231cc940..7bc6d70cd9 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -332,15 +332,15 @@ HB.instance Definition _ := HB.end. -HB.mixin Record Uniform_isTvs (R : numDomainType) E +HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E & Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B }. -#[short(type="tvsType")] -HB.structure Definition Tvs (R : numDomainType) := - {E of Uniform_isTvs R E & Uniform E & TopologicalLmodule R E}. +#[short(type="ctvsType")] +HB.structure Definition ConvexTvs (R : numDomainType) := + {E of Uniform_isConvexTvs R E & Uniform E & TopologicalLmodule R E}. Section properties_of_topologicalLmodule. Context (R : numDomainType) (E : preTopologicalLmodType R) (U : set E). @@ -378,7 +378,7 @@ Unshelve. all: by end_near. Qed. End properties_of_topologicalLmodule. -HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E +HB.factory Record TopologicalLmod_isConvexTvs (R : numDomainType) E & Topological E & GRing.Lmodule R E := { add_continuous : continuous (fun x : E * E => x.1 + x.2) ; scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; @@ -386,7 +386,7 @@ HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E (forall b, b \in B -> convex b) & basis B }. -HB.builders Context R E & PreTopologicalLmod_isTvs R E. +HB.builders Context R E & TopologicalLmod_isConvexTvs R E. Definition entourage : set_system (E * E) := fun P => exists (U : set E), nbhs (0 : E) U /\ @@ -476,7 +476,7 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E HB.end. Section Tvs_numDomain. -Context (R : numDomainType) (E : tvsType R) (U : set E). +Context (R : numDomainType) (E : ctvsType R) (U : set E). Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). Proof. exact/nbhs0N_subproof/scale_continuous. Qed. @@ -491,7 +491,7 @@ End Tvs_numDomain. Section Tvs_numField. -Lemma nbhs0Z (R : numFieldType) (E : tvsType R) (U : set E) (r : R) : +Lemma nbhs0Z (R : numFieldType) (E : ctvsType R) (U : set E) (r : R) : r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ). Proof. move=> r0 U0; have /= := scale_continuous (r^-1, 0) U. @@ -500,7 +500,7 @@ near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r. by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x]. Unshelve. all: by end_near. Qed. -Lemma nbhsZ (R : numFieldType) (E : tvsType R) (U : set E) (r : R) (x :E) : +Lemma nbhsZ (R : numFieldType) (E : ctvsType R) (U : set E) (r : R) (x :E) : r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ). Proof. move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U. @@ -570,12 +570,13 @@ HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous. -HB.instance Definition _ := Uniform_isTvs.Build R R^o standard_locally_convex. +HB.instance Definition _ := Uniform_isConvexTvs.Build R R^o + standard_locally_convex. End standard_topology. Section prod_Tvs. -Context (K : numFieldType) (E F : tvsType K). +Context (K : numFieldType) (E F : ctvsType K). Local Lemma prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2). Proof. @@ -629,7 +630,7 @@ HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build K (E * F)%type prod_scale_continuous. HB.instance Definition _ := - Uniform_isTvs.Build K (E * F)%type prod_locally_convex. + Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex. End prod_Tvs. @@ -743,7 +744,7 @@ HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) End lcfun_comp. Section lcfun_lmodtype. - Context {R : numFieldType} {E F G: tvsType R}. + Context {R : numFieldType} {E F G: ctvsType R}. (* {s : GRing.Scale.law R F}. *) Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}). @@ -951,7 +952,7 @@ tvstype *) (*What follows is adapted from {family fam, U -> V} in function_space.v. Should we copy instances from family fam to family_lcfun fam ? *) -Definition uniform_lcfun_family R {E : tvsType R} (F : tvsType R) (fam : set E -> Prop) : Type := +Definition uniform_lcfun_family R {E : ctvsType R} (F : ctvsType R) (fam : set E -> Prop) : Type := {linear_continuous E -> F}. (* Reserved Notation "'{' 'family_lcfun' fam , U '->' V '|' s '}'" *) @@ -979,6 +980,19 @@ Notation "{ 'family_lcfun' fam , F --> f }" := Locate sup_topology. Search (continuousType _ _). Locate continuousEP. + +(*md +Define bounded +Define bornology +Define uniform convergence on bornology +Prove continuous embedding into topologies already defined on spaces of functions. +*) + +(*First lemma to formalize : Prop 1 in 2.10 Jarchow *) + +(* W is a 0-basis for a linear topology 3~aonG iff 38 consists ofG-bounded +sets only. In that case, if F is Hausdorff and 38 covers X, then J~a is Hausdorff*) + (** examples **) (* HB.instance Definition _ (U : Type) (T : U -> topologicalType) := *) (* Topological.copy (forall x : U, T x) (prod_topology T). *) @@ -1021,7 +1035,7 @@ Search (continuousType _ _). Locate continuousEP. Section dual. -Context {R : numDomainType} {E : tvsType R}. +Context {R : numDomainType} {E : ctvsType R}. (* Reserved Notation " E ''' " (at level 80, format "E ''' "). *) From 80574c1df5367855a4944cb325f380230c60264a Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 11 Apr 2025 17:42:16 +0200 Subject: [PATCH 11/16] wip bornology --- theories/normedtype_theory/tvs.v | 86 +++++++++++++++++++++++++------- 1 file changed, 69 insertions(+), 17 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 7bc6d70cd9..21afe0f4dd 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -940,20 +940,13 @@ End test. (* TODO : define bornology and topology of uniform convergence, show it's a tvstype *) (* Not used in the following *) -(* Class Bornology {T : Type} (B : set_system T) := { *) -(* bornoC : forall x, exists b, (B b) /\ (b x) ; *) -(* bornoU : forall P Q : set T, B P -> B Q -> B (P `|` Q) ; *) -(* bornoS : forall P Q : set T, P `<=` Q -> B Q -> B P *) -(* }. *) - -(* Global Hint Mode Bornology - ! : typeclass_instances. *) (* (*why with typeclasses and not with HB ? *) *) (*What follows is adapted from {family fam, U -> V} in function_space.v. Should we copy instances from family fam to family_lcfun fam ? *) -Definition uniform_lcfun_family R {E : ctvsType R} (F : ctvsType R) (fam : set E -> Prop) : Type := - {linear_continuous E -> F}. + Definition uniform_lcfun_family R {E : ctvsType R} (F : ctvsType R) (fam : set E -> Prop) : Type := + {linear_continuous E -> F}. (* Reserved Notation "'{' 'family_lcfun' fam , U '->' V '|' s '}'" *) (* (at level 0, U at level 98, V at level 99, *) @@ -977,21 +970,79 @@ Notation "{ 'family_lcfun' fam , F --> f }" := (* we can´t use unfiorm, it is defined on E -> F and not on our space. We need to define it on {linear_continuous E -> F} , inducing its topology from uniform` E- > F *) -Locate sup_topology. -Search (continuousType _ _). Locate continuousEP. - (*md Define bounded -Define bornology +TODO generalize bounded_fun_norm in sequence.v +Define bornology and bounded function - prove continuous -> bounded +Generalize bounded_near in normedtype.v Define uniform convergence on bornology Prove continuous embedding into topologies already defined on spaces of functions. -*) -(*First lemma to formalize : Prop 1 in 2.10 Jarchow *) +Pour E_{sigma} : utiliser des tags, ie des identité annotées + *) + + +Reserved Notation "'{' 'linear_continuous_' B , U '->' V '}'" + (at level 0, U at level 98, V at level 99, + format "{ 'linear_continuous_' B , U -> V }"). +Reserved Notation "'{' 'linear_continuous_' B , F '-->' f '}'" + (at level 0, F at level 98, f at level 99, + format "{ 'linear_continuous_' B , F --> f }"). + + +Definition bounded (R : numFieldType) (E : ctvsType R) (b : set E) := forall (V : set E), (nbhs 0 V -> exists r, b `<=` ((fun x => r *: x )@` V)). + +Notation "{ 'linear_continuous_' fam , U -> V }" := (@uniform_lcfun_family _ U V fam). +Notation "{ 'linear_continuous_' fam , F --> f }" := + (cvg_to F (@nbhs _ {linear_continuous_ fam, _ -> _ } f)) : type_scope. + +Definition nbhs_lineartopology (R : numFieldType) (E : ctvsType R) (F : ctvsType R) b U := + [set f : {linear_continuous E -> F}| f @` b `<=` U ]. + + +HB.mixin Record isBornology (R : numFieldType) (E : ctvsType R) (B : set_system E) := { + bornoC : forall x, exists b, (B b) /\ (b x) ; + bornoS : forall P Q : set E, P `<=` Q -> B Q -> B P; + bornoI : forall P Q : set E, B P -> B Q -> B (P `&` Q); (*wikipedia*) + (* bornoZ : forall r : R, forall Q : set E, B Q -> exists P, (B P /\ (((fun x => r *: x )@`Q `<=` P))) (*why ??*) In Jarchow*) + }. + +#[short(type="bornologyType")] + HB.structure Definition Bornology R E := {B of @isBornology R E B}. + +(* +Pointed Type on linear_continuous, filteredtype, nbhsType, topologicaltype + + *) + +(* Reco Cyril: copier / généraliser les defs de function_space.v, puis montrer que la prebase c ést nbhs_lineartopology. Compliqué parce que +Notation "{ 'uniform`' A -> V }" := (@uniform_fun _ A V) : type_scope. +ne se généralise pas facilement en +Notation "{ 'linear_continuous` `' A -> V }" := (linear_continuous A -> V) : type_scope. + +(* HB.instance Definition _ {R} {U V : tvsType R} (fam : set U -> Prop) := *) +(* Uniform.copy {family_lcfun fam, U -> V} (sup_topology (fun k : sigT fam => *) +(* Uniform.class {uniform` projT1 k -> V})). *) + +(* HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system E) of Topological {family_lcfun B , E -> F} & GRing.Lmodule {linear_continuous E -> F } := { *) +(* bornoC : forall x : E, exists b : set E, (B b) /\ (b x) ; *) +(* bornoU : forall P Q : set E, B P -> B Q -> B (P `|` Q) ; *) +(* bornoS : forall P Q : set E, P `<=` Q -> B Q -> B P *) +(* }. *) + +(* HB.builders Context R E F B of UniformLinCont_isTvs R E F B. *) + + + + +(*First lemmas to formalize : +- Prop 1 in 2.10 Jarchow (* W is a 0-basis for a linear topology 3~aonG iff 38 consists ofG-bounded +sets only. In that case, if F is Hausdorff and 38 covers X, then J~a is Hausdorf *) +- Prop 2 in 8.4 Jarchow + +Then define notations and prove compatibility with function_spaces.v notations*) -(* W is a 0-basis for a linear topology 3~aonG iff 38 consists ofG-bounded -sets only. In that case, if F is Hausdorff and 38 covers X, then J~a is Hausdorff*) (** examples **) (* HB.instance Definition _ (U : Type) (T : U -> topologicalType) := *) @@ -1045,3 +1096,4 @@ Check (E)'. Notation " E ''' ":= {linear_continuous E -> R^o} (at level 80). End dual. +*) From 70603bf2e070c0092ad27897a545e1ce2fb20107 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 13 Feb 2026 15:05:55 +0900 Subject: [PATCH 12/16] copy hahn banach from old branch - use convex.v - does not compile yet --- _CoqProject | 2 + theories/Make | 3 + theories/hahn_banach_theorem.v | 1076 ++++++++++++++++++++ theories/normedtype_theory/normed_module.v | 11 +- theories/normedtype_theory/tvs.v | 12 +- 5 files changed, 1094 insertions(+), 10 deletions(-) create mode 100644 theories/hahn_banach_theorem.v diff --git a/_CoqProject b/_CoqProject index 8b90d48615..8aa22648c1 100644 --- a/_CoqProject +++ b/_CoqProject @@ -143,6 +143,8 @@ theories/kernel.v theories/pi_irrational.v theories/gauss_integral.v +theories/hahn_banach_theorem.v + theories/all_analysis.v theories/showcase/summability.v diff --git a/theories/Make b/theories/Make index 75ab71c748..4e88887225 100644 --- a/theories/Make +++ b/theories/Make @@ -104,6 +104,9 @@ probability_theory/beta_distribution.v probability_theory/probability.v convex.v + +hahn_banach_theorem.v + charge.v kernel.v pi_irrational.v diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v new file mode 100644 index 0000000000..b28a480cf7 --- /dev/null +++ b/theories/hahn_banach_theorem.v @@ -0,0 +1,1076 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import interval_inference. +From mathcomp Require Import boolp classical_sets topology reals. + +(* 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 linear 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. + + +(* A handful of axioms, stated here without trying to minimize the + interface. *) + + Axiom Prop_irrelevance : forall (P : Prop) (x y : P), x = y. + Axiom funext : forall (T U : Type) (f g : T -> U), (f =1 g) -> f = g. + Axiom propext : forall (P Q : Prop), (P <-> Q) -> (P = Q). + + Definition Choice_prop := ((forall T U (Q : T -> U -> Prop), + (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t)))) . + Definition EM := forall (P : Prop), P \/ ~ P. + + +Section Diaconescu. + + Lemma contrapos (P Q : Prop) : (P -> Q) -> (~Q -> ~P). + Proof. + move => H nQ p. + by pose bot := nQ (H p). + Qed. + + Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q). + Proof. by apply: propext; split=> [->|/propext]. Qed. + + Lemma funeqE {T U : Type} (f g : T -> U) : (f = g) = (f =1 g). + Proof. by rewrite propeqE; split=> [->//|/funext]. Qed. + + Lemma predeqE {T} (P Q : T -> Prop) : (P = Q) = (forall x, P x <-> Q x). + Proof. + by rewrite propeqE; split=> [->//|?]; rewrite funeqE=> x; rewrite propeqE. + Qed. + + + + (*the following is directly borrowed from coq.stdlib/Coq.Logic.Diaconescu *) + + Lemma Relational_Choice : Choice_prop -> forall A B (R:A->B->Prop), + (forall x : A, exists y : B, R x y) -> + (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y). + Proof. + move => H A B R Hex. case (H A B R Hex) => [f P]. + exists (fun x y => y = (f x)). + split. + move => x y -> ; exact : (P x). + move => x ; exists (f x) ; split. + by []. + by move => z ->. + Qed. + + + Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : + Choice_prop -> (forall A B (P : A ->Prop), forall R : A->B->Prop, + (forall x : A, P x -> exists y : B, R x y) -> + (exists R' : A->B->Prop, + subrelation R' R /\ forall x, P x -> exists! y, R' x y)). + Proof. + move => choice_prop. + pose rel_choice := Relational_Choice choice_prop. + move => A B P R H. + destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)). + intros (x,HPx). + destruct (H x HPx) as (y,HRxy). + exists y; exact HRxy. + set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). + exists R''; split. + intros x y (HPx,HR'xy). + change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy. + intros x HPx. + destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)). + exists y; split. exists HPx; exact HR'xy. + intros y' (H'Px,HR'xy'). + apply Huniq. + rewrite (Prop_irrelevance HPx H'Px); exact HR'xy'. +Qed. + + Lemma AC_bool_subset_to_bool : + Choice_prop -> + (exists R : (bool -> Prop) -> bool -> Prop, + (forall P:bool -> Prop, + (exists b : bool, P b) -> + exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b'))). + Proof. + move => choice_prop. + destruct ( (rel_choice_and_proof_irrel_imp_guarded_rel_choice choice_prop) _ _ + (fun Q:bool -> Prop => exists y : _, Q y) + (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). + exact (fun _ H => H). + exists R; move => P HP. + case (HR P HP) as (y,(Hy,Huni)). + exists y; firstorder. +Qed. + + + +End Diaconescu. + + + +Section Classical. + + Variable EM : forall (P : Prop), P \/ ~ P. + + Lemma double_neg_elim (P : Prop) : ~ ( ~ P) <-> P. + Proof. + split. + - move => nnP. case : (EM P) ; first by []. + by move => nP ; pose bot := nnP nP. + - by move => p np. + Qed. + + Lemma neg_exists (T : Type) (P : T -> Prop) : ~ ( exists s, ( P s)) -> forall s, ~ ( P s ). + Proof. + by move => H s Ps ; have : exists s : T, P s by exists s. + Qed. + + Lemma contrap P Q : ( ~ P -> ~ Q) -> ( Q -> P ). + Proof. + move => H p. + case : (EM P) ; first by []. + move => nQ. + have bot : False by exact : ((H nQ)p) . + by []. + Qed. + + Lemma neg_forall (T : Type) (P : T -> Prop) : ~ (forall s, (P s)) -> exists s, ~ ( P s). + Proof. + apply : contrap. + move => nE. apply : (proj2 (double_neg_elim (forall s, (P s)))). + move => s. apply : (proj1 (double_neg_elim (P s))). + exact : ((neg_exists nE) s). + Qed. + +Lemma neg_impl (P Q : Prop) : ~ ( P -> Q) -> (P /\ ~Q). + Proof. +by rewrite not_implyE. +Qed. + +End Classical. + + Local Open Scope ring_scope. + Import GRing.Theory. + Import Num.Theory. + +Section SetPredRels. + + Variables T U : Type. + Implicit Types f g : T -> U -> Prop. + + Definition set (A : Type) := A -> Prop. + + Definition total_on T (A : set T) (R : T -> T -> Prop) := + forall s t, A s -> A t -> R s t \/ R t s. + + (* Extends is just relation inclusion *) + Definition extends f g := forall v r, f v r -> g v r. + + Lemma extends_refl f : extends f f. Proof. by []. Qed. + + Lemma extends_trans f2 f1 f3 : extends f1 f2 -> extends f2 f3 -> extends f1 f3. + Proof. by move=> h1 h2 v r /h1 /h2. Qed. + + (* We make use of funext and propext here. Ideally we would word on hprops. *) + Lemma extends_antisym f g : extends f g -> extends g f -> f = g. + Proof. + move=> efg egf; apply: funext => v; apply: funext=> r; apply: propext; split. + - exact: efg. + - exact: egf. + Qed. + + + (* Functional (possibly empty or partial) graphs *) + Definition functional f := + forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. + + (* Graph of a function *) + Definition graph_of (h : T -> U) v r : Prop := r = h v. + + (* The relation f includes the graph of function h on set A *) + (* the intension is that f is the graph of a function h, which + coincides with f on F *) + Definition extends_fun_on (A : set T) f h := forall v, A v -> f v (h v). + +End SetPredRels. + + + + + + + +Section StrictInductiveFixpoint. + (*We prove a fixpoint lemma for increasing functions on strictly + inductive sets, following ALgebra by Lang*) + (* Choice is not necessary, but EM is*) + + Variable EM : forall P, P \/ ~ P. + + Variable (T : Type) ( R : T -> T -> Prop) (f : T -> T). + + + Hypothesis f_incr : forall t, R t (f t). + + Hypothesis R_ref : forall t, R t t. + + Hypothesis R_trans : forall r s t, R r s -> R s t -> R r t. + + Hypothesis R_antisym : forall r s, R r s -> R s r -> r=s. + + Definition maj ( T: Type) (R : T -> T -> Prop) A t := forall s, A s -> R s t. + + Definition sup A t := (maj R A t)/\(forall r, (maj R A r) -> R t r ). + + + Hypothesis R_strind : (forall A : set T, total_on A R -> exists t, sup A t). + + + (*Beginning by lemmas on sets, least upper bounds and the subset relation *) + + + Lemma sup_uniq A r s : sup A r -> sup A s -> s = r. + Proof. + move => [majr supr] [majs sups]. + exact (R_antisym (sups r majr) (supr s majs)). + Qed. + + (* It seems that we don't need to reason on nonempy subsets, contr. to Lang*) + (*Definition nonempty (A: set T) := exists x_0, A x_0.*) + + Definition subset (A B: set T) := forall x, A x -> B x. + + Lemma subset_refl : forall A, subset A A. + Proof. by move => A s. Qed. + + Lemma subset_trans : forall A B C, subset A B -> subset B C -> subset A C. + Proof. by move => A B C HAB HBC s As; apply : HBC s (HAB s As). Qed. + + Lemma subset_antisym : forall A B, subset A B -> subset B A -> A = B. + Proof. + move => A B HAB HBA; apply : funext => s; apply: propext; split. + exact (HAB s). + exact (HBA s). + Qed. + + (*An admissible subset is stable by f and contains the least upper bounds + of its subsets*) + + Definition adm (B :set T) := (forall x , B x -> (B (f x)) ) /\ + (forall C : set T, subset C B -> total_on C R -> + forall t, (sup C t -> B t)). + (* M is the intersection of all admissible subsets *) + + Definition M := fun x => ( forall B, adm B -> B x). + + (* This is how we prove the existence of a fixpoint *) + Lemma fixpoint_tot M : adm M -> (total_on M R) -> exists t, t = f t. + Proof. + move => adM totM. + have idM : forall x, M x -> M x by []. + case : (R_strind totM) => [t supt]. + exists t. + pose Mt := (proj2 adM) M idM totM t supt. + pose ht := ((proj1 supt) ((f t))) ( (proj1 adM) t Mt). + exact (R_antisym (f_incr t) ht) . + Qed. + + Lemma stabM : forall x, M x -> M (f x). + Proof. move => x Mx B admB ; exact ((proj1 admB) x (Mx B admB)). Qed. + + (*To prove that M is itself admissible, we must now show that it contains + the least upper bounds of its totally ordered subsets*) + + Lemma BsubsetM : forall B, adm B -> subset M B. Proof. + by move => B admB x Mx ; apply : Mx B admB. + Qed. + + Lemma adm_M : adm M. + Proof. + split. + - exact : stabM. + - move => C MC totC ; move : (R_strind totC) => [t tsupC] r rsupC. + rewrite (sup_uniq tsupC rsupC) => B [f_B sup_int_B]. + have BC : subset C B by move => x Cx ; apply : (MC x Cx B). + exact : (sup_int_B C BC totC). + Qed. + + (* To prove totality of M we need a few lemmas*) + + Definition extreme c := M c /\ (forall (x:T), M x -> ((x <> c) -> R x c-> R (f x) c)). + + Lemma extrM : subset extreme M. + Proof. by move => x extrx ; apply : proj1 extrx. Qed. + + Definition extr_set c := fun x => (M x /\ ((R x c) \/ ( R (f c) x))). + + Lemma subextrM (c :T) : extreme c -> subset (extr_set c) M. + Proof. + move => extrc x extrcx ; exact (proj1 extrcx). + Qed. + + + Lemma MextrM c : extreme c -> (forall x , M x -> extr_set c x). + Proof. + move => [Mc extrc]. + have extrMc : extreme c. split ; first by exact : Mc. + exact : extrc. + have extr_adm : adm (extr_set c). + split. + - move => x [Mx extrcx] ; case : (EM (x =c)). + - move => H ; split. + exact (stabM Mx). + by right; rewrite H. + - move => neq_xc ; case : extrcx. + - move => Rxc ; split. + - exact : stabM. + - left ; exact (extrc x Mx neq_xc Rxc). + - move => Rfcx ; split. + - exact : stabM. + - right; exact : (R_trans Rfcx (f_incr x)). + - move => C Cextrc totC t supCt. + split. + - exact: (proj2 adm_M C (subset_trans Cextrc ((subextrM extrMc) )) totC t supCt). + - case : (EM (maj R C c)). + - move => H ; left ; exact : (proj2 supCt c H). + - move => /(neg_forall EM)-[s ps]. + have [Cs nRsc] := neg_impl ps => {ps}. (*short*) + have lem : R (f c) s . + case : (EM (R ( f c) s )) ; first by []. + case : (proj2 (Cextrc s Cs)). + - move => H ; pose bot := nRsc H; by []. + - by []. + right. exact : (R_trans lem (proj1 supCt s Cs)). + move => x mx. exact : ( mx (extr_set c) extr_adm). + Qed. + + + Lemma all_extr : forall c, M c -> extreme c. + Proof. + have admE : adm extreme. + have f_E : forall c, extreme c -> extreme ( f c ). + move => c [Mc extrc]. split. by apply : stabM. + have extrec : extreme c. split. by []. by []. + move => x Mx neq_xfc. + case : (proj2 (MextrM extrec Mx)). + case : (EM (x =c )). + - by move => -> . + - move => neq_xc Rxc Rxfc ; + exact ( R_trans (extrc x Mx neq_xc Rxc) (f_incr c)). + - by move => Rfcx Rxfc ; pose bot := (neq_xfc (R_antisym Rxfc Rfcx)). + have sup_E : (forall C , subset C extreme -> total_on C R -> + forall t, (sup C t -> extreme t)). + move => C subCE totC t supCt. + have Mt : M t + by apply : (proj2 adm_M) C (subset_trans subCE extrM) totC t supCt. + split. exact: Mt. + move => x Mx neq_xt Rxt. + case : (EM (forall c, C c -> R (f c) x )). + - move => H. + have lem : maj R C x. move => c Cc ; exact : ( R_trans (f_incr c) (H c Cc)). + by pose bot := neq_xt (R_antisym Rxt (proj2 supCt x lem)). + - move => /(neg_forall EM)-[c H1]. pose H2 := neg_impl H1. + move : H2 ; move => [Cc nRfcx] {H1}. (*short ?*) + have extrec : extreme c by apply :subCE c Cc. + case : (proj2 ( MextrM extrec Mx)). + - case : (EM (x =c)). + - move => eq_xc ; move : neq_xt ; rewrite eq_xc => neq_ct. + move : extrec. rewrite -eq_xc => extrx. + case : (proj2 (MextrM extrx Mt)). + - move : neq_ct; rewrite -eq_xc => neq_xt. (*short*) + by move => Rtx; pose bot := neq_xt (R_antisym Rxt Rtx). + - by []. + - move => neq_xc Rxc. + exact : (R_trans ((proj2 extrec) x Mx neq_xc Rxc) (proj1 supCt c Cc)) . + - move => Rfcx ; by pose bot := nRfcx Rfcx. + split. + exact : f_E. + exact : sup_E. + by move => c Mc; exact : (Mc extreme admE). + Qed. + + + (*Now we can prove totality of R on M and conclude *) + Lemma tot_M : total_on M R. + Proof. + move => x y Mx My. + case : (proj2 (MextrM (all_extr Mx) My)). + by move => Ryx ; right. + by move => Rfxy ; left ; apply : R_trans (f_incr x) Rfxy. + Qed. + + + Lemma fixpoint : exists t, t = f t. + Proof. + exact (fixpoint_tot adm_M tot_M). + Qed. + + +End StrictInductiveFixpoint. + + + +Section Zorn. + + + (*This proof of Zorn using the fixpoint theorem follows Lang, Algebra, Appendix 2*) + (* We first prove Zorn for strictly inductive sets*) + + Variable Choice_prop : forall T U (P : T -> U -> Prop), + (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). + + Variable EM : forall P, P \/ ~P. + + Lemma Zorn_strict : forall (T : Type) ( R : T -> T -> Prop), + (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) -> + (forall s t, R s t -> R t s -> s = t) -> + (forall A : set T, total_on A R -> exists t, + (maj R A t)/\(forall r, (maj R A r) -> R t r )) -> + exists t, forall s, R t s -> s = t. + Proof. + move => T R Hrefl Htrans Hord Hchain. + case : (EM (exists t, forall s: T, R t s -> s= t)) ; first by []. + move => /neg_exists Habs. + have Hsucc : (forall t, exists s, R t s /\ t <> s). + move => t. case : (EM ( exists s : T, R t s /\ t <> s)) ; first by []. + move => /neg_exists H. + have lem : (forall s : T, R t s -> s=t). + move => s Rts. case : (EM (t=s)) ; first by []. + move => sneqt ; have lem2 : (R t s /\ t <> s) by split . + by have bot := H s lem2. + by have bot := Habs t lem. + case : (Choice_prop Hsucc) => {Hsucc} f Hf ; have Hmaj := fun a => proj1 (Hf a). + pose Hfix := fixpoint EM Hmaj Hrefl Htrans Hord Hchain. + case : Hfix => t hfix. + by have bot := (proj2 (Hf t) hfix ). + Qed. + + + + (*Then we deduce the more general Zorn Lemma for orders. + This is done by applying Zorn_strict to the totally ordered subsets of T + ordered by inculsion *) + + + Variable ( T : Type) ( R : T -> T -> Prop). + + Record tot_subset : Type := Tot_subset + {car : set T ; tot : total_on car R}. + + Lemma tot_subset_eq U1 U2 : car U1 = car U2 -> U1 = U2. + Proof. + case: U1 => m1 pm1; case: U2 => m2 pm2 /= e; + move: pm1 pm2; rewrite e => pm1 pm2. + by congr Tot_subset; apply: Prop_irrelevance. + Qed. + + + + Definition subsett ( C D : tot_subset) := subset (car C) (car D). + + Lemma Zorn : + (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) -> + (forall s t, R s t -> R t s -> s = t) -> + (forall A : set T, total_on A R -> exists t, forall s, A s -> R s t) -> + exists t, forall s, R t s -> s = t. + Proof. + move => Rrefl Rtrans Rantis Rind. + have subset_strict_ind : (forall W : set (tot_subset), total_on W subsett -> + exists A, (maj subsett W A)/\(forall B, (maj subsett W B) -> subsett A B )). + move => W Htot. + pose U := fun (t : T) => exists A, (W A) /\ (car A t). + have tot_U : total_on U R. + move => t s [[cAt tot_At] [Wt ct]] [[cAs tot_As] [Ws cs]]. + case: (Htot (Tot_subset tot_At) (Tot_subset tot_As) Wt Ws). + by move => Ats ; exact (tot_As t s (Ats t ct) cs). + by move => Ast ; rewrite or_comm ; exact (tot_At s t (Ast s cs) ct). + pose Utot := Tot_subset tot_U. + have UsupW : (maj subsett W Utot)/\ + (forall B, (maj subsett W B) -> subsett Utot B). + split ; first by move => B WB tB ctB //= ; exists B ; split. + move => B majWB t //= [A [ ]] WA cAt ; exact (majWB A WA t cAt). + by exists Utot. + have subsett_maj : exists (A : tot_subset), + forall (B : tot_subset), subsett A B -> B = A. + apply : Zorn_strict. + by move => t; apply : subset_refl. + by move => r s t ; apply : subset_trans. + by move => s t Hst Hts ; apply : tot_subset_eq ; apply : subset_antisym. + exact : subset_strict_ind. + case : subsett_maj => [[cA PA]] majA. + pose tot_A := Tot_subset PA. + (*we want to handle A as a subset and as a totally ordered subset *) + case : (Rind cA PA) => t t_maj. + exists t ; move => s Rts. + pose B := fun u => (cA u)\/(u=s). + have lem : total_on B R. + move => u v Bu Bv ; case : Bv; case : Bu. + exact : PA. + by move => -> Av ; right ; apply : Rtrans v t s (t_maj v Av) Rts. + by move => Au -> ; left ; apply : Rtrans u t s (t_maj u Au) Rts. + by move => -> -> ; left ;apply : Rrefl s. + pose tot_B := Tot_subset lem. + have HAB : subsett tot_A tot_B by move => u Au ; left. + have eq_A_B : tot_B = tot_A by apply : majA tot_B HAB. + have eqc_A_B : cA = B. + have lem1 : B = car (tot_B) by [] ; rewrite lem1. + have lem2 : cA = car (tot_A) by [] ; rewrite lem2 . + by rewrite eq_A_B => {lem1} {lem2}. + have As : cA s. + have Bs : B s by right . + by rewrite eqc_A_B. + exact : Rantis s t (t_maj s As) Rts. +Qed. + +End Zorn. + + + + + + +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). + + Definition convex (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. + + Variable EM : forall P, P \/ ~ P. + + Variable Choice_prop : forall T U (P : T -> U -> Prop), + (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). + + Variables (R : realFieldType) (V : lmodType R). + + Variables (F G : 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. + + Hypothesis p_cvx : convex 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) := extends (carrier z1) (carrier z2). + + Lemma zorn_rel_refl z : zorn_rel z z. + Proof. rewrite /zorn_rel. exact: extends_refl. Qed. + + Lemma zorn_rel_trans z1 z2 z3 : + zorn_rel z1 z2 -> zorn_rel z2 z3 -> zorn_rel z1 z3. + Proof. rewrite /zorn_rel; exact: extends_trans. Qed. + + Lemma zorn_rel_antisym z1 z2 : zorn_rel z1 z2 -> zorn_rel z2 z1 -> z1 = z2. + Proof. + rewrite /zorn_rel /= => s12 s21; apply: zorn_type_eq; exact: extends_antisym. + Qed. + + Lemma zorn_rel_maj (A : set zorn_type) : total_on A zorn_rel -> + exists t, forall s, A s -> zorn_rel s t. + Proof. + move=> htot. + case: (EM (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 [] : zorn_rel a b \/ zorn_rel b a by exact: htot. + - rewrite /zorn_rel; case: b Ab bvr2 {Aa} => s2 [fs2 _ _ _] /= _ s2vr2 ecas2. + by move/ecas2: avr1 => /fs2 /(_ s2vr2). + - rewrite /zorn_rel; case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 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 [sc12 | sc21] := htot _ _ 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]; rewrite /zorn_rel /= => v r cvr; exists a. + Qed. + + Lemma zorn_rel_ex : exists g : zorn_type, forall z, zorn_rel g z -> z = g. + Proof. + apply: Zorn. + - exact : Choice_prop. + - exact : EM. + - exact: zorn_rel_refl. + - exact: zorn_rel_trans. + - exact: zorn_rel_antisym. + - exact: zorn_rel_maj. + 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 domain_extend (z : zorn_type) v : + exists2 ze : zorn_type, (zorn_rel z ze) & (exists r, (carrier ze) v r). + Proof. + case: (EM (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; apply: p_cvx. + split. + rewrite divr_ge0 //=. + by apply : ltW. + by rewrite addr_ge0 //= ; apply: ltW. + rewrite divr_ge0 //=. + by apply : ltW. + by rewrite addr_ge0 //= ; apply: ltW. + by rewrite -mulrDl mulfV //; apply: lt0r_neq0; rewrite addr_gt0. + 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 : extends c z'. + 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. +have [h hP] : exists h, forall v, carrier g v (h v) by exact: Choice_prop tot_g. +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 HahnBanach. +(* 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. *) +Variable EM : forall P, P \/ ~P. + +Variable Choice_prop : forall T U (P : T -> U -> Prop), + (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). + +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}. + +(* F and G are of type V -> bool, as required by the Mathematical Components + interfaces. f is a linear application from (the entire) V to R. *) +Variables (F G : 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). + +(* In fact we do not need G to be a superset of F *) +(* Hypothesis sFG : subpred F G. *) + +Hypothesis p_cvx : convex p. + +Hypothesis f_bounded_by_p : forall x, F x -> f x <= p x. + +Theorem HahnBanach : 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 EM Choice_prop graphFP. +pose FP v : Prop := F v. +have FP0 : FP 0 by []. +have [g gP]:= hb_witness EM Choice_prop 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. + +End HahnBanach. + +From mathcomp Require Import filter reals normedtype. +Import numFieldNormedType.Exports. +Local Open Scope classical_set_scope. + +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). + + +Hypothesis (Choice_prop : ((forall T U (Q : T -> U -> Prop), + (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t))))). + + +(*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 []. + move: (H 1) {H'}. + have f0 : f 0 = 0. + suff -> : f 0 = f (0 + (-1)*: 0) by rewrite linfF // mulNr mul1r addrN. + by rewrite scaleNr scaler0 addrN. +(* rewrite near_simpl /( _ @ _ ) //= nearE /(within _ ) near_simpl f0. + rewrite -nbhs_nearE => H0 {H} ; move : (nbhs_ex H0) => [tp H] {H0}. + pose t := tp%:num . + exists (2*t^-1). split=> //. + move=> x. case: (boolp.EM (x=0)). + - by move=> ->; rewrite f0 normr0 normr0 //= mul0r. + - move/eqP=> xneq0 Fx. + pose a : V := (`|x|^-1 * t/2 ) *: x. + have Btp : ball 0 t a. + apply : ball_sym ; rewrite -ball_normE /ball_ subr0. + rewrite normmZ mulrC normrM. + rewrite !gtr0_norm //= ; last by rewrite pmulr_lgt0 // invr_gt0 normr_gt0. + rewrite mulrC -mulrA -mulrA ltr_pdivr_mull; last by rewrite normr_gt0. + rewrite mulrC -mulrA gtr_pmull. + rewrite invf_lt1 //=. + by have lt01 : 0 < 1 by []; have le11 : 1 <= 1 by [] ; apply : ltr_spaddr. + 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) * t/2 ) * ( f x)) . + rewrite normrM (gtr0_norm) //. + rewrite mulrC mulrC -mulrA -mulrA ltr_pdivr_mull //= ; + last by rewrite normr_gt0. + rewrite mulrC [(_*1)]mulrC mul1r -ltr_pdivl_mulr //. + by rewrite invf_div => Ht; apply : ltW. + by rewrite !mulr_gt0 // invr_gt0 normr_gt0. + suff -> : a = 0+ (`|x|^-1 * t/2) *: x by rewrite linfF // f0 add0r. + by rewrite add0r. +Qed.*) Admitted. + +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) Choice_prop 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: 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 ler_oppl -linearN; apply: (le_trans (majgp (-y))). + by rewrite /p -[X in _ <= X]mul1r; apply: ler_pmul; rewrite ?normr_ge0 ?ltW //=. + - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. + apply: ler_pmul; rewrite ?normr_ge0 ?ltW //=. +Qed.*) +Admitted. + +End HBGeom. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 5477f31a20..005cff6699 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -76,7 +76,7 @@ Local Open Scope ring_scope. (** Modules with a norm depending on a numDomain *) -HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V +HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V & PseudoMetricNormedZmod K V & ConvexTvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. @@ -84,7 +84,7 @@ HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := {T of PseudoMetricNormedZmod K T & ConvexTvs K T - & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. + & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}. HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V & PseudoMetricNormedZmod K V & GRing.Lmodule K V := { @@ -113,7 +113,6 @@ 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 (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B. Proof. @@ -148,7 +147,7 @@ HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous. HB.instance Definition _ := Uniform_isConvexTvs.Build K V locally_convex. HB.instance Definition _ := - PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ. + PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ. HB.end. @@ -158,7 +157,7 @@ Section standard_topology_normedMod. Variable R : numFieldType. HB.instance Definition _ := - PseudoMetricNormedZmod_Tvs_isNormedModule.Build R R^o (@normrM _). + PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _). End standard_topology_normedMod. @@ -1663,7 +1662,7 @@ Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed. HB.instance Definition _ := - PseudoMetricNormedZmod_Tvs_isNormedModule.Build K (U * V)%type + PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K (U * V)%type prod_norm_scale. End prod_NormedModule. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 21afe0f4dd..2bf7d57cef 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1,7 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector. -From mathcomp Require Import interval_inference. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. @@ -332,6 +331,8 @@ HB.instance Definition _ := HB.end. +Local Open Scope convex_scope. + HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E & Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set (set E), @@ -639,11 +640,14 @@ HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.ty (F : NbhsZmodule.type) (s : K -> F -> F) := {f of @GRing.Linear K E F s f & @Continuous E F f }. -HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) +(* https://github.com/math-comp/math-comp/issues/1536 + we use GRing.Scale.law even though it is claimed to be internal *) +HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) (F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := { + (* NB: why not (f : {linear E -> F | s} instead of linearP ? ) *) linearP : linear_for s f ; continuousP : continuous f - }. + }. HB.builders Context K E F s f of @isLinearContinuous K E F s f. From 6499ba41bcc06e96112e7c7c82e3fdaddc738b66 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 18 Feb 2026 15:23:09 +0900 Subject: [PATCH 13/16] update hahn_banach (wip) --- theories/hahn_banach_theorem.v | 176 ++++++++++++++++++++++++------- theories/normedtype_theory/tvs.v | 2 +- 2 files changed, 137 insertions(+), 41 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index b28a480cf7..df97c74fd8 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -939,18 +939,14 @@ Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Section HBGeom. +Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 0). -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). - +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). Hypothesis (Choice_prop : ((forall T U (Q : T -> U -> Prop), (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t))))). - (*Looked a long time for within *) Definition continuousR_on ( G : set V ) (g : V -> R) := {within G, continuous g}. @@ -966,41 +962,43 @@ Lemma continuousR_scalar_on_bounded : Proof. rewrite /continuousR_on_at. move => /cvg_ballP H. - have H': (0 < 1) by []. - move: (H 1) {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 near_simpl /( _ @ _ ) //= nearE /(within _ ) near_simpl f0. + 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*t^-1). split=> //. + (*pose t := tp%:num . *) + exists (2*(tp%:num)^-1). split=> //. move=> x. case: (boolp.EM (x=0)). - by move=> ->; rewrite f0 normr0 normr0 //= mul0r. - move/eqP=> xneq0 Fx. - pose a : V := (`|x|^-1 * t/2 ) *: x. - have Btp : ball 0 t a. - apply : ball_sym ; rewrite -ball_normE /ball_ subr0. - rewrite normmZ mulrC normrM. - rewrite !gtr0_norm //= ; last by rewrite pmulr_lgt0 // invr_gt0 normr_gt0. - rewrite mulrC -mulrA -mulrA ltr_pdivr_mull; last by rewrite normr_gt0. - rewrite mulrC -mulrA gtr_pmull. + 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 have lt01 : 0 < 1 by []; have le11 : 1 <= 1 by [] ; apply : ltr_spaddr. + 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) * t/2 ) * ( f x)) . + suff -> : ( f a = ( (`|x|^-1) * (tp%:num)/2 ) * ( f x)) . rewrite normrM (gtr0_norm) //. - rewrite mulrC mulrC -mulrA -mulrA ltr_pdivr_mull //= ; + rewrite mulrC mulrC -mulrA -mulrA ltr_pdivrMl //= ; last by rewrite normr_gt0. - rewrite mulrC [(_*1)]mulrC mul1r -ltr_pdivl_mulr //. - by rewrite invf_div => Ht; apply : ltW. - by rewrite !mulr_gt0 // invr_gt0 normr_gt0. - suff -> : a = 0+ (`|x|^-1 * t/2) *: x by rewrite linfF // f0 add0r. + 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.*) Admitted. +Qed. Lemma mymysup : forall (A : set R) (a m : R), A a -> ubound A m -> @@ -1028,17 +1026,15 @@ Lemma mymyinf : forall (A : set R) (a m : R), by move => x; apply: lb_le_inf. Qed. - Notation myHB := (HahnBanach (boolp.EM) Choice_prop mymysup mymyinf F0 linF linfF). - Theorem HB_geom_normed : - continuousR_on_at F 0 f -> + 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. + move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}. + 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|). @@ -1062,15 +1058,115 @@ Proof. 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 => M m1; rewrite nbhs_ballP; exists 1 => /=; first by []. move => y; rewrite -ball_normE //= sub0r => y1. - rewrite ler_norml; apply/andP; split. - - rewrite ler_oppl -linearN; apply: (le_trans (majgp (-y))). - by rewrite /p -[X in _ <= X]mul1r; apply: ler_pmul; rewrite ?normr_ge0 ?ltW //=. + 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_pmul; rewrite ?normr_ge0 ?ltW //=. -Qed.*) -Admitted. + 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 *) + +Hypothesis (Choice_prop : ((forall T U (Q : T -> U -> Prop), + (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t))))). + +(* +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) Choice_prop 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. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 2bf7d57cef..3b43120f9d 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -786,7 +786,7 @@ Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _). Proof. by (* NB TODO: move section cvg_composition_pseudometric in normedtype.v here, to generalize it on tvstype *) -(* Next lemmas are duplicates *) +(* Next lemmas are duplicates - do it more properly with appropriate conte*) (* TODO once PR1544 is merged *) Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b : From 100fe70c665fd8f220a23c043c8a2309337d35c6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 4 Mar 2026 16:50:48 +0900 Subject: [PATCH 14/16] clean classical axioms wip --- theories/hahn_banach_theorem.v | 683 ++++++--------------------------- 1 file changed, 122 insertions(+), 561 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index df97c74fd8..dcf0189361 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -1,12 +1,15 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp Require Import interval_inference. -From mathcomp Require Import boolp classical_sets topology reals. +From mathcomp Require Import wochoice boolp classical_sets topology reals. +From mathcomp Require Import filter reals normedtype. +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 linear form extending f. But this options seems much + 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 @@ -20,143 +23,11 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -(* A handful of axioms, stated here without trying to minimize the - interface. *) - - Axiom Prop_irrelevance : forall (P : Prop) (x y : P), x = y. - Axiom funext : forall (T U : Type) (f g : T -> U), (f =1 g) -> f = g. - Axiom propext : forall (P Q : Prop), (P <-> Q) -> (P = Q). - - Definition Choice_prop := ((forall T U (Q : T -> U -> Prop), - (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t)))) . - Definition EM := forall (P : Prop), P \/ ~ P. - - -Section Diaconescu. - - Lemma contrapos (P Q : Prop) : (P -> Q) -> (~Q -> ~P). - Proof. - move => H nQ p. - by pose bot := nQ (H p). - Qed. - - Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q). - Proof. by apply: propext; split=> [->|/propext]. Qed. - - Lemma funeqE {T U : Type} (f g : T -> U) : (f = g) = (f =1 g). - Proof. by rewrite propeqE; split=> [->//|/funext]. Qed. - - Lemma predeqE {T} (P Q : T -> Prop) : (P = Q) = (forall x, P x <-> Q x). - Proof. - by rewrite propeqE; split=> [->//|?]; rewrite funeqE=> x; rewrite propeqE. - Qed. - - - - (*the following is directly borrowed from coq.stdlib/Coq.Logic.Diaconescu *) - - Lemma Relational_Choice : Choice_prop -> forall A B (R:A->B->Prop), - (forall x : A, exists y : B, R x y) -> - (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y). - Proof. - move => H A B R Hex. case (H A B R Hex) => [f P]. - exists (fun x y => y = (f x)). - split. - move => x y -> ; exact : (P x). - move => x ; exists (f x) ; split. - by []. - by move => z ->. - Qed. - - - Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : - Choice_prop -> (forall A B (P : A ->Prop), forall R : A->B->Prop, - (forall x : A, P x -> exists y : B, R x y) -> - (exists R' : A->B->Prop, - subrelation R' R /\ forall x, P x -> exists! y, R' x y)). - Proof. - move => choice_prop. - pose rel_choice := Relational_Choice choice_prop. - move => A B P R H. - destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)). - intros (x,HPx). - destruct (H x HPx) as (y,HRxy). - exists y; exact HRxy. - set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). - exists R''; split. - intros x y (HPx,HR'xy). - change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy. - intros x HPx. - destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)). - exists y; split. exists HPx; exact HR'xy. - intros y' (H'Px,HR'xy'). - apply Huniq. - rewrite (Prop_irrelevance HPx H'Px); exact HR'xy'. -Qed. - - Lemma AC_bool_subset_to_bool : - Choice_prop -> - (exists R : (bool -> Prop) -> bool -> Prop, - (forall P:bool -> Prop, - (exists b : bool, P b) -> - exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b'))). - Proof. - move => choice_prop. - destruct ( (rel_choice_and_proof_irrel_imp_guarded_rel_choice choice_prop) _ _ - (fun Q:bool -> Prop => exists y : _, Q y) - (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). - exact (fun _ H => H). - exists R; move => P HP. - case (HR P HP) as (y,(Hy,Huni)). - exists y; firstorder. -Qed. - - - -End Diaconescu. - - - -Section Classical. - - Variable EM : forall (P : Prop), P \/ ~ P. - - Lemma double_neg_elim (P : Prop) : ~ ( ~ P) <-> P. - Proof. - split. - - move => nnP. case : (EM P) ; first by []. - by move => nP ; pose bot := nnP nP. - - by move => p np. - Qed. - - Lemma neg_exists (T : Type) (P : T -> Prop) : ~ ( exists s, ( P s)) -> forall s, ~ ( P s ). - Proof. - by move => H s Ps ; have : exists s : T, P s by exists s. - Qed. - - Lemma contrap P Q : ( ~ P -> ~ Q) -> ( Q -> P ). - Proof. - move => H p. - case : (EM P) ; first by []. - move => nQ. - have bot : False by exact : ((H nQ)p) . - by []. - Qed. +Search "choice_prop". - Lemma neg_forall (T : Type) (P : T -> Prop) : ~ (forall s, (P s)) -> exists s, ~ ( P s). - Proof. - apply : contrap. - move => nE. apply : (proj2 (double_neg_elim (forall s, (P s)))). - move => s. apply : (proj1 (double_neg_elim (P s))). - exact : ((neg_exists nE) s). - Qed. +Definition Choice_prop := ((forall T U (Q : T -> U -> Prop), + (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t)))). -Lemma neg_impl (P Q : Prop) : ~ ( P -> Q) -> (P /\ ~Q). - Proof. -by rewrite not_implyE. -Qed. - -End Classical. Local Open Scope ring_scope. Import GRing.Theory. @@ -166,378 +37,13 @@ Section SetPredRels. Variables T U : Type. Implicit Types f g : T -> U -> Prop. - - Definition set (A : Type) := A -> Prop. - - Definition total_on T (A : set T) (R : T -> T -> Prop) := - forall s t, A s -> A t -> R s t \/ R t s. - - (* Extends is just relation inclusion *) - Definition extends f g := forall v r, f v r -> g v r. - - Lemma extends_refl f : extends f f. Proof. by []. Qed. - - Lemma extends_trans f2 f1 f3 : extends f1 f2 -> extends f2 f3 -> extends f1 f3. - Proof. by move=> h1 h2 v r /h1 /h2. Qed. - - (* We make use of funext and propext here. Ideally we would word on hprops. *) - Lemma extends_antisym f g : extends f g -> extends g f -> f = g. - Proof. - move=> efg egf; apply: funext => v; apply: funext=> r; apply: propext; split. - - exact: efg. - - exact: egf. - Qed. - - (* Functional (possibly empty or partial) graphs *) Definition functional f := forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. - (* Graph of a function *) - Definition graph_of (h : T -> U) v r : Prop := r = h v. - - (* The relation f includes the graph of function h on set A *) - (* the intension is that f is the graph of a function h, which - coincides with f on F *) - Definition extends_fun_on (A : set T) f h := forall v, A v -> f v (h v). - End SetPredRels. - - - - - -Section StrictInductiveFixpoint. - (*We prove a fixpoint lemma for increasing functions on strictly - inductive sets, following ALgebra by Lang*) - (* Choice is not necessary, but EM is*) - - Variable EM : forall P, P \/ ~ P. - - Variable (T : Type) ( R : T -> T -> Prop) (f : T -> T). - - - Hypothesis f_incr : forall t, R t (f t). - - Hypothesis R_ref : forall t, R t t. - - Hypothesis R_trans : forall r s t, R r s -> R s t -> R r t. - - Hypothesis R_antisym : forall r s, R r s -> R s r -> r=s. - - Definition maj ( T: Type) (R : T -> T -> Prop) A t := forall s, A s -> R s t. - - Definition sup A t := (maj R A t)/\(forall r, (maj R A r) -> R t r ). - - - Hypothesis R_strind : (forall A : set T, total_on A R -> exists t, sup A t). - - - (*Beginning by lemmas on sets, least upper bounds and the subset relation *) - - - Lemma sup_uniq A r s : sup A r -> sup A s -> s = r. - Proof. - move => [majr supr] [majs sups]. - exact (R_antisym (sups r majr) (supr s majs)). - Qed. - - (* It seems that we don't need to reason on nonempy subsets, contr. to Lang*) - (*Definition nonempty (A: set T) := exists x_0, A x_0.*) - - Definition subset (A B: set T) := forall x, A x -> B x. - - Lemma subset_refl : forall A, subset A A. - Proof. by move => A s. Qed. - - Lemma subset_trans : forall A B C, subset A B -> subset B C -> subset A C. - Proof. by move => A B C HAB HBC s As; apply : HBC s (HAB s As). Qed. - - Lemma subset_antisym : forall A B, subset A B -> subset B A -> A = B. - Proof. - move => A B HAB HBA; apply : funext => s; apply: propext; split. - exact (HAB s). - exact (HBA s). - Qed. - - (*An admissible subset is stable by f and contains the least upper bounds - of its subsets*) - - Definition adm (B :set T) := (forall x , B x -> (B (f x)) ) /\ - (forall C : set T, subset C B -> total_on C R -> - forall t, (sup C t -> B t)). - (* M is the intersection of all admissible subsets *) - - Definition M := fun x => ( forall B, adm B -> B x). - - (* This is how we prove the existence of a fixpoint *) - Lemma fixpoint_tot M : adm M -> (total_on M R) -> exists t, t = f t. - Proof. - move => adM totM. - have idM : forall x, M x -> M x by []. - case : (R_strind totM) => [t supt]. - exists t. - pose Mt := (proj2 adM) M idM totM t supt. - pose ht := ((proj1 supt) ((f t))) ( (proj1 adM) t Mt). - exact (R_antisym (f_incr t) ht) . - Qed. - - Lemma stabM : forall x, M x -> M (f x). - Proof. move => x Mx B admB ; exact ((proj1 admB) x (Mx B admB)). Qed. - - (*To prove that M is itself admissible, we must now show that it contains - the least upper bounds of its totally ordered subsets*) - - Lemma BsubsetM : forall B, adm B -> subset M B. Proof. - by move => B admB x Mx ; apply : Mx B admB. - Qed. - - Lemma adm_M : adm M. - Proof. - split. - - exact : stabM. - - move => C MC totC ; move : (R_strind totC) => [t tsupC] r rsupC. - rewrite (sup_uniq tsupC rsupC) => B [f_B sup_int_B]. - have BC : subset C B by move => x Cx ; apply : (MC x Cx B). - exact : (sup_int_B C BC totC). - Qed. - - (* To prove totality of M we need a few lemmas*) - - Definition extreme c := M c /\ (forall (x:T), M x -> ((x <> c) -> R x c-> R (f x) c)). - - Lemma extrM : subset extreme M. - Proof. by move => x extrx ; apply : proj1 extrx. Qed. - - Definition extr_set c := fun x => (M x /\ ((R x c) \/ ( R (f c) x))). - - Lemma subextrM (c :T) : extreme c -> subset (extr_set c) M. - Proof. - move => extrc x extrcx ; exact (proj1 extrcx). - Qed. - - - Lemma MextrM c : extreme c -> (forall x , M x -> extr_set c x). - Proof. - move => [Mc extrc]. - have extrMc : extreme c. split ; first by exact : Mc. - exact : extrc. - have extr_adm : adm (extr_set c). - split. - - move => x [Mx extrcx] ; case : (EM (x =c)). - - move => H ; split. - exact (stabM Mx). - by right; rewrite H. - - move => neq_xc ; case : extrcx. - - move => Rxc ; split. - - exact : stabM. - - left ; exact (extrc x Mx neq_xc Rxc). - - move => Rfcx ; split. - - exact : stabM. - - right; exact : (R_trans Rfcx (f_incr x)). - - move => C Cextrc totC t supCt. - split. - - exact: (proj2 adm_M C (subset_trans Cextrc ((subextrM extrMc) )) totC t supCt). - - case : (EM (maj R C c)). - - move => H ; left ; exact : (proj2 supCt c H). - - move => /(neg_forall EM)-[s ps]. - have [Cs nRsc] := neg_impl ps => {ps}. (*short*) - have lem : R (f c) s . - case : (EM (R ( f c) s )) ; first by []. - case : (proj2 (Cextrc s Cs)). - - move => H ; pose bot := nRsc H; by []. - - by []. - right. exact : (R_trans lem (proj1 supCt s Cs)). - move => x mx. exact : ( mx (extr_set c) extr_adm). - Qed. - - - Lemma all_extr : forall c, M c -> extreme c. - Proof. - have admE : adm extreme. - have f_E : forall c, extreme c -> extreme ( f c ). - move => c [Mc extrc]. split. by apply : stabM. - have extrec : extreme c. split. by []. by []. - move => x Mx neq_xfc. - case : (proj2 (MextrM extrec Mx)). - case : (EM (x =c )). - - by move => -> . - - move => neq_xc Rxc Rxfc ; - exact ( R_trans (extrc x Mx neq_xc Rxc) (f_incr c)). - - by move => Rfcx Rxfc ; pose bot := (neq_xfc (R_antisym Rxfc Rfcx)). - have sup_E : (forall C , subset C extreme -> total_on C R -> - forall t, (sup C t -> extreme t)). - move => C subCE totC t supCt. - have Mt : M t - by apply : (proj2 adm_M) C (subset_trans subCE extrM) totC t supCt. - split. exact: Mt. - move => x Mx neq_xt Rxt. - case : (EM (forall c, C c -> R (f c) x )). - - move => H. - have lem : maj R C x. move => c Cc ; exact : ( R_trans (f_incr c) (H c Cc)). - by pose bot := neq_xt (R_antisym Rxt (proj2 supCt x lem)). - - move => /(neg_forall EM)-[c H1]. pose H2 := neg_impl H1. - move : H2 ; move => [Cc nRfcx] {H1}. (*short ?*) - have extrec : extreme c by apply :subCE c Cc. - case : (proj2 ( MextrM extrec Mx)). - - case : (EM (x =c)). - - move => eq_xc ; move : neq_xt ; rewrite eq_xc => neq_ct. - move : extrec. rewrite -eq_xc => extrx. - case : (proj2 (MextrM extrx Mt)). - - move : neq_ct; rewrite -eq_xc => neq_xt. (*short*) - by move => Rtx; pose bot := neq_xt (R_antisym Rxt Rtx). - - by []. - - move => neq_xc Rxc. - exact : (R_trans ((proj2 extrec) x Mx neq_xc Rxc) (proj1 supCt c Cc)) . - - move => Rfcx ; by pose bot := nRfcx Rfcx. - split. - exact : f_E. - exact : sup_E. - by move => c Mc; exact : (Mc extreme admE). - Qed. - - - (*Now we can prove totality of R on M and conclude *) - Lemma tot_M : total_on M R. - Proof. - move => x y Mx My. - case : (proj2 (MextrM (all_extr Mx) My)). - by move => Ryx ; right. - by move => Rfxy ; left ; apply : R_trans (f_incr x) Rfxy. - Qed. - - - Lemma fixpoint : exists t, t = f t. - Proof. - exact (fixpoint_tot adm_M tot_M). - Qed. - - -End StrictInductiveFixpoint. - - - -Section Zorn. - - - (*This proof of Zorn using the fixpoint theorem follows Lang, Algebra, Appendix 2*) - (* We first prove Zorn for strictly inductive sets*) - - Variable Choice_prop : forall T U (P : T -> U -> Prop), - (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). - - Variable EM : forall P, P \/ ~P. - - Lemma Zorn_strict : forall (T : Type) ( R : T -> T -> Prop), - (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) -> - (forall s t, R s t -> R t s -> s = t) -> - (forall A : set T, total_on A R -> exists t, - (maj R A t)/\(forall r, (maj R A r) -> R t r )) -> - exists t, forall s, R t s -> s = t. - Proof. - move => T R Hrefl Htrans Hord Hchain. - case : (EM (exists t, forall s: T, R t s -> s= t)) ; first by []. - move => /neg_exists Habs. - have Hsucc : (forall t, exists s, R t s /\ t <> s). - move => t. case : (EM ( exists s : T, R t s /\ t <> s)) ; first by []. - move => /neg_exists H. - have lem : (forall s : T, R t s -> s=t). - move => s Rts. case : (EM (t=s)) ; first by []. - move => sneqt ; have lem2 : (R t s /\ t <> s) by split . - by have bot := H s lem2. - by have bot := Habs t lem. - case : (Choice_prop Hsucc) => {Hsucc} f Hf ; have Hmaj := fun a => proj1 (Hf a). - pose Hfix := fixpoint EM Hmaj Hrefl Htrans Hord Hchain. - case : Hfix => t hfix. - by have bot := (proj2 (Hf t) hfix ). - Qed. - - - - (*Then we deduce the more general Zorn Lemma for orders. - This is done by applying Zorn_strict to the totally ordered subsets of T - ordered by inculsion *) - - - Variable ( T : Type) ( R : T -> T -> Prop). - - Record tot_subset : Type := Tot_subset - {car : set T ; tot : total_on car R}. - - Lemma tot_subset_eq U1 U2 : car U1 = car U2 -> U1 = U2. - Proof. - case: U1 => m1 pm1; case: U2 => m2 pm2 /= e; - move: pm1 pm2; rewrite e => pm1 pm2. - by congr Tot_subset; apply: Prop_irrelevance. - Qed. - - - - Definition subsett ( C D : tot_subset) := subset (car C) (car D). - - Lemma Zorn : - (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) -> - (forall s t, R s t -> R t s -> s = t) -> - (forall A : set T, total_on A R -> exists t, forall s, A s -> R s t) -> - exists t, forall s, R t s -> s = t. - Proof. - move => Rrefl Rtrans Rantis Rind. - have subset_strict_ind : (forall W : set (tot_subset), total_on W subsett -> - exists A, (maj subsett W A)/\(forall B, (maj subsett W B) -> subsett A B )). - move => W Htot. - pose U := fun (t : T) => exists A, (W A) /\ (car A t). - have tot_U : total_on U R. - move => t s [[cAt tot_At] [Wt ct]] [[cAs tot_As] [Ws cs]]. - case: (Htot (Tot_subset tot_At) (Tot_subset tot_As) Wt Ws). - by move => Ats ; exact (tot_As t s (Ats t ct) cs). - by move => Ast ; rewrite or_comm ; exact (tot_At s t (Ast s cs) ct). - pose Utot := Tot_subset tot_U. - have UsupW : (maj subsett W Utot)/\ - (forall B, (maj subsett W B) -> subsett Utot B). - split ; first by move => B WB tB ctB //= ; exists B ; split. - move => B majWB t //= [A [ ]] WA cAt ; exact (majWB A WA t cAt). - by exists Utot. - have subsett_maj : exists (A : tot_subset), - forall (B : tot_subset), subsett A B -> B = A. - apply : Zorn_strict. - by move => t; apply : subset_refl. - by move => r s t ; apply : subset_trans. - by move => s t Hst Hts ; apply : tot_subset_eq ; apply : subset_antisym. - exact : subset_strict_ind. - case : subsett_maj => [[cA PA]] majA. - pose tot_A := Tot_subset PA. - (*we want to handle A as a subset and as a totally ordered subset *) - case : (Rind cA PA) => t t_maj. - exists t ; move => s Rts. - pose B := fun u => (cA u)\/(u=s). - have lem : total_on B R. - move => u v Bu Bv ; case : Bv; case : Bu. - exact : PA. - by move => -> Av ; right ; apply : Rtrans v t s (t_maj v Av) Rts. - by move => Au -> ; left ; apply : Rtrans u t s (t_maj u Au) Rts. - by move => -> -> ; left ;apply : Rrefl s. - pose tot_B := Tot_subset lem. - have HAB : subsett tot_A tot_B by move => u Au ; left. - have eq_A_B : tot_B = tot_A by apply : majA tot_B HAB. - have eqc_A_B : cA = B. - have lem1 : B = car (tot_B) by [] ; rewrite lem1. - have lem2 : cA = car (tot_A) by [] ; rewrite lem2 . - by rewrite eq_A_B => {lem1} {lem2}. - have As : cA s. - have Bs : B s by right . - by rewrite eqc_A_B. - exact : Rantis s t (t_maj s As) Rts. -Qed. - -End Zorn. - - - - - - Section OrderRels. Variable (R : numDomainType). @@ -559,7 +65,7 @@ Section OrderRels. Variables (R : numDomainType) (V : lmodType R). - Definition convex (p : V -> R) := forall v1 v2 l m, + Definition convex_fun (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) := @@ -598,8 +104,6 @@ Section OrderRels. Section HBPreparation. - Variable EM : forall P, P \/ ~ P. - Variable Choice_prop : forall T U (P : T -> U -> Prop), (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). @@ -620,7 +124,7 @@ have -> : 0 = 0 + (-1) *: 0 :> V by rewrite scaler0 addr0. by rewrite linphiF // mulN1r addrN. Qed. - Hypothesis p_cvx : convex p. + Hypothesis p_cvx : convex_fun p. Hypothesis sup : forall (A : set R) (a m : R), A a -> ubd A m -> @@ -651,38 +155,36 @@ Qed. by congr ZornType; apply: Prop_irrelevance. Qed. - Definition zorn_rel (z1 z2 : zorn_type) := extends (carrier z1) (carrier z2). - - Lemma zorn_rel_refl z : zorn_rel z z. - Proof. rewrite /zorn_rel. exact: extends_refl. Qed. - - Lemma zorn_rel_trans z1 z2 z3 : - zorn_rel z1 z2 -> zorn_rel z2 z3 -> zorn_rel z1 z3. - Proof. rewrite /zorn_rel; exact: extends_trans. Qed. - - Lemma zorn_rel_antisym z1 z2 : zorn_rel z1 z2 -> zorn_rel z2 z1 -> z1 = z2. - Proof. - rewrite /zorn_rel /= => s12 s21; apply: zorn_type_eq; exact: extends_antisym. - Qed. - - Lemma zorn_rel_maj (A : set zorn_type) : total_on A zorn_rel -> - exists t, forall s, A s -> zorn_rel s t. + 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. - move=> htot. - case: (EM (exists a, A a)) => [[w Aw] | eA]; last first. + 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 [] : zorn_rel a b \/ zorn_rel b a by exact: htot. - - rewrite /zorn_rel; case: b Ab bvr2 {Aa} => s2 [fs2 _ _ _] /= _ s2vr2 ecas2. + 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 /zorn_rel; case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 ecbs1. + - 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 [sc12 | sc21] := htot _ _ Aa1 Aa2. + 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. @@ -692,20 +194,10 @@ Qed. 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]; rewrite /zorn_rel /= => v r cvr; exists a. - Qed. - - Lemma zorn_rel_ex : exists g : zorn_type, forall z, zorn_rel g z -> z = g. - Proof. - apply: Zorn. - - exact : Choice_prop. - - exact : EM. - - exact: zorn_rel_refl. - - exact: zorn_rel_trans. - - exact: zorn_rel_antisym. - - exact: zorn_rel_maj. - Qed. + 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. @@ -716,7 +208,7 @@ Qed. Lemma domain_extend (z : zorn_type) v : exists2 ze : zorn_type, (zorn_rel z ze) & (exists r, (carrier ze) v r). Proof. - case: (EM (exists r, (carrier z v r))). + 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. @@ -790,7 +282,7 @@ Qed. 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 : extends c z'. + 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. @@ -848,24 +340,24 @@ by have -> // := fg v r (h v). Qed. -End HBPreparation. + End HBPreparation. -Section HahnBanach. + 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. *) -Variable EM : forall P, P \/ ~P. + Variable Choice_prop : forall T U (P : T -> U -> Prop), (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). - + 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}. + {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), @@ -881,17 +373,17 @@ Variables (F G : pred V) (f : V -> R) (p : V -> R). 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 -> +Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> f (v1 + l *: v2) = f v1 + l * (f v2). (* In fact we do not need G to be a superset of F *) (* Hypothesis sFG : subpred F G. *) -Hypothesis p_cvx : convex p. +Hypothesis p_cvx : convex_fun p. Hypothesis f_bounded_by_p : forall x, F x -> f x <= p x. -Theorem HahnBanach : exists g : {scalar V}, +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 ->] [_ ->]. @@ -902,10 +394,10 @@ 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 EM Choice_prop graphFP. +have [z zmax]:= zorn_rel_ex graphFP. pose FP v : Prop := F v. have FP0 : FP 0 by []. -have [g gP]:= hb_witness EM Choice_prop linfF FP0 p_cvx sup inf zmax. +have [g gP]:= hb_witness Choice_prop linfF FP0 p_cvx sup inf zmax. have scalg : linear_for *%R g. case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. have addg : additive g. @@ -932,11 +424,80 @@ have grxtf v : F v -> g v = f v. by case: z {zmax} gP => [c [_ _ bp _]] /= gP; apply/bp/gP. Qed. -End HahnBanach. +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. *) + +Variable Choice_prop : forall T U (P : T -> U -> Prop), + (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). + +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_fun 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 Choice_prop 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. -From mathcomp Require Import filter reals normedtype. -Import numFieldNormedType.Exports. -Local Open Scope classical_set_scope. Section HBGeom. Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 0). @@ -972,7 +533,7 @@ Proof. 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: (boolp.EM (x=0)). + 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. @@ -1027,7 +588,7 @@ Lemma mymyinf : forall (A : set R) (a m : R), Qed. Notation myHB := - (HahnBanach (boolp.EM) Choice_prop mymysup mymyinf F0 linF linfF). + (HahnBanachold Choice_prop mymysup mymyinf F0 linF linfF). Theorem HB_geom_normed : continuousR_on_at F 0 f -> @@ -1035,7 +596,7 @@ Theorem HB_geom_normed : Proof. move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}. pose p:= fun x : V => `|x|*r. - have convp: hahn_banach_theorem.convex p. + have convp: convex_fun 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 []. From d382cf7f081ff9dba403d26c33e38829cd60d24d Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Mar 2026 09:20:42 +0900 Subject: [PATCH 15/16] clean axiom choice --- theories/hahn_banach_theorem.v | 31 +++++-------------------------- 1 file changed, 5 insertions(+), 26 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index dcf0189361..5b44a7a40a 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -23,10 +23,6 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Search "choice_prop". - -Definition Choice_prop := ((forall T U (Q : T -> U -> Prop), - (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t)))). Local Open Scope ring_scope. @@ -104,9 +100,6 @@ Section OrderRels. Section HBPreparation. - Variable Choice_prop : forall T U (P : T -> U -> Prop), - (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). - Variables (R : realFieldType) (V : lmodType R). Variables (F G : set V) (phi : V -> R) (p : V -> R). @@ -332,9 +325,7 @@ Qed. Lemma hb_witness : exists h : V -> R, forall v r, carrier g v r <-> (h v = r). Proof. -have [h hP] : exists h, forall v, carrier g v (h v) by exact: Choice_prop tot_g. -exists h => v r. -split; last by move<-. +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. @@ -349,10 +340,6 @@ Qed. on R. We do not make use of the 'vector' interface as the latter enforces finite dimension. *) - -Variable Choice_prop : forall T U (P : T -> U -> Prop), - (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). - Variables (R : realFieldType) (V : lmodType R). Hypothesis sup : forall (A : set R) (a m : R), @@ -397,7 +384,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 Choice_prop linfF FP0 p_cvx sup inf 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. @@ -434,9 +421,6 @@ Section HahnBanachnew. on R. We do not make use of the 'vector' interface as the latter enforces finite dimension. *) -Variable Choice_prop : forall T U (P : T -> U -> Prop), - (forall t : T, exists u : U, P t u) -> (exists e, forall t, P t (e t)). - Variables (R : realFieldType) (V : lmodType R). Hypothesis sup : forall (A : set R) (a m : R), @@ -468,7 +452,7 @@ have [z zmax]:= zorn_rel_ex graphFP. *) pose FP v : Prop := F v. have FP0 : FP 0 by []. -have [g gP]:= hb_witness Choice_prop linfF FP0 p_cvx sup inf 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. @@ -505,9 +489,6 @@ Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 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). -Hypothesis (Choice_prop : ((forall T U (Q : T -> U -> Prop), - (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t))))). - (*Looked a long time for within *) Definition continuousR_on ( G : set V ) (g : V -> R) := {within G, continuous g}. @@ -588,7 +569,7 @@ Lemma mymyinf : forall (A : set R) (a m : R), Qed. Notation myHB := - (HahnBanachold Choice_prop mymysup mymyinf F0 linF linfF). + (HahnBanachold mymysup mymyinf F0 linF linfF). Theorem HB_geom_normed : continuousR_on_at F 0 f -> @@ -640,8 +621,6 @@ Variable (R : realType) (V: normedModType R) (F : subLmodType V) (f : {linear F (* 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 *) -Hypothesis (Choice_prop : ((forall T U (Q : T -> U -> Prop), - (forall t : T, exists u : U, Q t u) -> (exists e, forall t, Q t (e t))))). (* Lemma mymysup : forall (A : set R) (a m : R), @@ -672,7 +651,7 @@ Qed. Notation myHB := - (HahnBanach (boolp.EM) Choice_prop mymysup mymyinf F0 linF linfF). + (HahnBanach (boolp.EM) mymysup mymyinf F0 linF linfF). *) Search "continuous" "subspace". From 5d61806435bf280f96f8979cf7d1caf5a7f9b722 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Mar 2026 11:39:41 +0900 Subject: [PATCH 16/16] convex function generalization wip --- CHANGELOG_UNRELEASED.md | 3 ++ theories/hahn_banach_theorem.v | 70 ++++++++++++++++++---------------- 2 files changed, 40 insertions(+), 33 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 14e5333b3e..335d7aefaa 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -226,6 +226,9 @@ - moved from `tvs.v` to `convex.v` + definition `convex` +- in convex.v + + definition `convex_function` generalized from a realspace as domain to a lmodType as domain + ### Renamed - in `topology_structure.v` diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 5b44a7a40a..8258fecb73 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -1,8 +1,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp Require Import interval_inference. -From mathcomp Require Import wochoice boolp classical_sets topology reals. -From mathcomp Require Import filter reals normedtype. +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. @@ -25,7 +25,8 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory. - Local Open Scope ring_scope. +Local Open Scope ring_scope. +Local Open Scope convex_scope. Import GRing.Theory. Import Num.Theory. @@ -60,10 +61,12 @@ Section OrderRels. Section LinAndCvx. Variables (R : numDomainType) (V : lmodType R). - - Definition convex_fun (p : V -> R) := forall v1 v2 l m, + (* + 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). @@ -102,14 +105,13 @@ Section OrderRels. Variables (R : realFieldType) (V : lmodType R). - Variables (F G : set V) (phi : V -> R) (p : V -> 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. +Hypothesis F0 : F 0. Fact phi0 : phi 0 = 0. Proof. @@ -117,7 +119,8 @@ have -> : 0 = 0 + (-1) *: 0 :> V by rewrite scaler0 addr0. by rewrite linphiF // mulN1r addrN. Qed. - Hypothesis p_cvx : convex_fun p. +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 -> @@ -198,6 +201,15 @@ Qed. (*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. @@ -229,16 +241,11 @@ Qed. 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; apply: p_cvx. - split. - rewrite divr_ge0 //=. - by apply : ltW. - by rewrite addr_ge0 //= ; apply: ltW. - rewrite divr_ge0 //=. - by apply : ltW. - by rewrite addr_ge0 //= ; apply: ltW. - by rewrite -mulrDl mulfV //; apply: lt0r_neq0; rewrite addr_gt0. + 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. @@ -351,9 +358,7 @@ 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 and G are of type V -> bool, as required by the Mathematical Components - interfaces. f is a linear application from (the entire) V to R. *) -Variables (F G : pred V) (f : 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. *) @@ -363,10 +368,7 @@ 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). -(* In fact we do not need G to be a superset of F *) -(* Hypothesis sFG : subpred F G. *) - -Hypothesis p_cvx : convex_fun p. +Hypothesis p_cvx : (@convex_function R V [set: V] p). Hypothesis f_bounded_by_p : forall x, F x -> f x <= p x. @@ -384,7 +386,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 zmax. +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. @@ -434,7 +436,7 @@ Hypothesis inf : forall (A : set R) (a m : R), Variables (F : subLmodType V) (f : {linear F -> R}) (p : V -> R). -Hypothesis p_cvx : convex_fun p. +Hypothesis p_cvx : (@convex_function R V [set: V] p). Hypothesis f_bounded_by_p : forall x : F, (f x) <= (p (val x)). @@ -490,12 +492,12 @@ 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) := +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) := +Definition continuousR_on_at (G : set V) (x : V) (g : V -> R) := g @ (within G (nbhs x)) --> (g x). Lemma continuousR_scalar_on_bounded : @@ -577,8 +579,10 @@ Theorem HB_geom_normed : Proof. move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}. pose p:= fun x : V => `|x|*r. - have convp: convex_fun p. - move=> v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl. + 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.