diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a5849a853..57b19d910 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -32,6 +32,16 @@ + number notations in scopes `ereal_dual_scope` and `ereal_scope` + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope` +- in `tvs.v` + + lemmas `cvg_sum`, `sum_continuous` + +- in `normed_module.v`: + + structure `NormedVector` + + definitions `normedVectType`, `oo_norm`, `oo_space` + + lemmas `oo_norm_ge0`, `le_coord_oo_norm`, `ler_oo_normD`, `oo_norm0_eq0`, + `oo_normZ`, `oo_normMn`, `oo_normN`, `oo_closed_ball_compact`, + `equivalence_norms`, `linear_findim_continuous` + ### Changed - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`: diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 6af95b7d0..1ac0300a3 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -20,6 +20,9 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. (* normedModType K == interface type for a normed module *) (* structure over the numDomainType K *) (* The HB class is NormedModule. *) +(* normedVectType K == interface type for a normed vectType *) +(* structure over the numDomainType K *) +(* The HB class is NormedVector. *) (* `|x| == the norm of x (notation from ssrnum.v) *) (* ``` *) (* *) @@ -147,6 +150,10 @@ HB.instance Definition _ := HB.end. +#[short(type="normedVectType")] +HB.structure Definition NormedVector (K : numDomainType) := + {T of NormedModule K T & Vector K T}. + (**md see also `Section standard_topology_pseudoMetricNormedZmod` in `pseudometric_normed_Zmodule.v` *) Section standard_topology_normedMod. @@ -2079,3 +2086,241 @@ by rewrite interior_closed_ballE //; exact: ballxx. Qed. End Closed_Ball_normedModType. + +Section InfiniteNorm. +Variables (R : numFieldType) (V : vectType R) (B : (\dim (@fullv _ V)).-tuple V). +Let V' := @fullv _ V. +Hypothesis (Bbasis : basis_of V' B). + +Definition oo_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. + +Definition oo_space : Type := (fun=> V) Bbasis. + +HB.instance Definition _ := Vector.on oo_space. + +HB.instance Definition _ := Pointed.copy oo_space V^o. + +Lemma oo_norm_ge0 x : 0 <= oo_norm x. +Proof. +rewrite /oo_norm. +elim: (index_enum _) => /=; first by rewrite big_nil. +by move=> i l IHl; rewrite big_cons /Order.max/=; case: ifP. +Qed. + +Lemma le_coord_oo_norm x i : `|coord B i x| <= oo_norm x. +Proof. +rewrite /oo_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. +rewrite inE big_cons /Order.max/= => /orP[/eqP <-|/IHl {}IHl]; + case: ifP => [/ltW|]//. +move=> /negP/negP. +have bR: \big[Order.max/0]_(i <- l) `|coord B i x| \is Num.real. + exact: bigmax_real. +move: (real_comparable bR (normr_real (coord B j x))). +by move=> /comparable_leNgt <- /(le_trans IHl). +Qed. + +Lemma ler_oo_normD x y : oo_norm (x + y) <= oo_norm x + oo_norm y. +Proof. +apply: bigmax_le => [|/= i _]. + by apply: addr_ge0; apply: oo_norm_ge0. +rewrite raddfD/=. +by apply/(le_trans (ler_normD _ _))/lerD; apply: le_coord_oo_norm. +Qed. + +Lemma oo_norm0_eq0 x : oo_norm x = 0 -> x = 0. +Proof. +move=> x0. +rewrite (coord_basis Bbasis (memvf x)). +suff: forall i, coord B i x = 0. + move=> {}x0. + under eq_bigr do rewrite x0. + by rewrite -scaler_sumr scale0r. +move=> i; apply/normr0_eq0/le_anti/andP; split; last exact: normr_ge0. +by rewrite -x0; apply: le_coord_oo_norm. +Qed. + +Lemma oo_normZ r x : oo_norm (r *: x) = `|r| * oo_norm x. +Proof. +rewrite /oo_norm. +under eq_bigr do rewrite linearZ normrZ/=. +elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0. +by rewrite !big_cons IHl maxr_pMr. +Qed. + +Lemma oo_normMn x n : oo_norm (x *+ n) = oo_norm x *+ n. +Proof. by rewrite -scaler_nat oo_normZ normr_nat mulr_natl. Qed. + +Lemma oo_normN x : oo_norm (- x) = oo_norm x. +Proof. by rewrite -scaleN1r oo_normZ normrN1 mul1r. Qed. + +HB.instance Definition _ := Num.Zmodule_isNormed.Build R + oo_space ler_oo_normD oo_norm0_eq0 oo_normMn oo_normN. + +HB.instance Definition _ := + PseudoMetric.copy oo_space (pseudoMetric_normed oo_space). + +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R oo_space erefl. + +HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R oo_space oo_normZ. + +End InfiniteNorm. + +Section EquivalenceNorms. +Variables (R : realType) (V : vectType R). +Let V' := @fullv _ V. +Let Voo := oo_space (vbasisP (@fullv _ V)). + +(* N.B. Get Trocq to prove the continuity part automatically. *) +Lemma oo_closed_ball_compact : compact (closed_ball (0 : Voo) 1). +Proof. +rewrite closed_ballE/closed_ball_//=. +under eq_set do rewrite sub0r normrN. +rewrite -[forall x, _]/(compact _). +pose f (X : {ptws 'I_(\dim V') -> R^o}) : Voo := + \sum_(i < \dim V') (X i) *: (vbasis V')`_i. +have -> : + [set x : Voo | `|x| <= 1] = f @` [set X | forall i, `[-1, 1]%classic (X i)]. + apply/seteqP; split=> x/=. + move=> x1; exists (fun i => coord (vbasis V') i x); last first. + exact/esym/(@coord_vbasis _ _ (x : V))/memvf. + move=> i; rewrite in_itv/= -ler_norml. + apply: (le_trans _ x1). + exact: le_coord_oo_norm. + move=> [X] X1 <-. + rewrite /normr/=/oo_norm. + apply: bigmax_le => //= i _. + rewrite coord_sum_free; last exact/basis_free/vbasisP. + rewrite ler_norml. + exact: X1. +apply: (@continuous_compact _ _ f); last first. + apply: (@tychonoff 'I_(\dim V') (fun=> R^o) (fun=> `[-1, 1 : R^o]%classic)). + move=> _. + exact: segment_compact. +apply/continuous_subspaceT/sum_continuous => i _/= x. +exact/continuousZl/proj_continuous. +Qed. + +Lemma equivalence_norms (N : V -> R) : + N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) -> + (forall x y, N (x + y) <= N x + N y) -> + (forall r x, N (r *: x) = `|r| * N x) -> + exists M, 0 < M /\ forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. +Proof. +move=> N0 N_ge0 N0_eq0 ND NZ. +set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i. +have N_sum (I : Type) (r : seq I) (F : I -> V): + N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i). + elim: r => [|x r IHr]; first by rewrite !big_nil N0. + by rewrite !big_cons; apply/(le_trans (ND _ _))/lerD. +have leNoo: forall x : Voo, N x <= M0 * `|x|. + move=> x. + rewrite [in leLHS](coord_vbasis (memvf (x : V))). + apply: (le_trans (N_sum _ _ _)). + rewrite mulrDl mul1r mulr_suml -[leLHS]add0r. + apply: lerD => //. + apply: ler_sum => /= i _. + rewrite NZ mulrC; apply: ler_pM => //. + exact: le_coord_oo_norm. +have M00 : 0 < M0. + rewrite -[ltLHS]addr0. + by apply: ltr_leD => //; apply: sumr_ge0. +have NC0 : continuous (N : Voo -> R). + move=> /= x. + rewrite /continuous_at. + apply: cvg_zero; first exact: nbhs_filter. + apply/cvgr0Pnorm_le; first exact: nbhs_filter. + move=> /= e e0. + near=> y. + rewrite -[_ y]/(N y - N x). + apply: (@le_trans _ _ (N (y - x))). + apply/real_ler_normlP. + by apply: realB; apply: ger0_real. + have NB a b : N a <= N b + N (a - b). + by rewrite -[a in N a]addr0 -(subrr b) addrCA ND. + rewrite opprB !lerBlDl; split; last exact: NB. + by rewrite -opprB -scaleN1r NZ normrN1 mul1r NB. + apply: (le_trans (leNoo _)). + rewrite mulrC -ler_pdivlMr// -opprB normrN. + near: y; apply: cvgr_dist_le; first exact: cvg_id. + exact: divr_gt0. +have: compact [set x : Voo | `|x| = 1]. + apply: (subclosed_compact _ oo_closed_ball_compact); last first. + apply/subsetP => x. + rewrite closed_ballE// !inE/=. + by rewrite /closed_ball_/= sub0r normrN => ->. + apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq. + by rewrite /prop_in1 => + _; apply: norm_continuous. +move=> /(@continuous_compact _ _ (N : Voo -> R)) -/(_ _)/wrap[]. + exact: continuous_subspaceT. +move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[]. + move=> /= x. + rewrite /continuous_at. + apply: (@continuous_in_subspaceT _ _ + [set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)). + move=> r /set_mem/=[] y y1 <-. + apply: inv_continuous. + apply/negP => /eqP/N0_eq0 y0. + move: y1; rewrite y0 normr0 => /esym. + by move: (@oner_neq0 R) => /eqP. +move=> /compact_bounded[] M1 [] M1R /(_ (1 + M1)). +rewrite -subr_gt0 -addrA subrr addr0 => /(_ ltr01). +rewrite /globally/= => M1N. +exists (maxr M0 (1 + M1)). +split=> [|x]; first by apply: (lt_le_trans M00); rewrite le_max lexx. +split; last first. + apply/(le_trans (leNoo x))/ler_pM => //; first exact/ltW. + by rewrite /maxr; case: ifP => // /ltW. +have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0. +have Nx0: 0 < N x. + rewrite lt0r N_ge0 andbT. + by move: x0; apply: contra => /eqP/N0_eq0/eqP. +have normx0 : 0 < `|x|. + move: (lt_le_trans Nx0 (leNoo x)). + by rewrite pmulr_rgt0. +move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[]. + exists (N x / `|x|); last by rewrite invf_div. + exists (`|x|^-1 *: x); last first. + by rewrite NZ mulrC ger0_norm. + rewrite normrZ mulrC ger0_norm. + by rewrite divrr//; apply: unitf_gt0. + by rewrite invr_ge0; apply: ltW. +rewrite ger0_norm; last exact: divr_ge0. +rewrite ler_pdivrMr// => xle. +apply: (le_trans xle). +rewrite -subr_ge0 -mulrBl pmulr_lge0// subr_ge0. +by rewrite le_max lexx orbT. +Unshelve. all: by end_near. +Qed. + +End EquivalenceNorms. + +Section LinearContinuous. +Variables (R : realType) (V : normedVectType R) (W : normedModType R). + +Lemma linear_findim_continuous (f : {linear V -> W}) : continuous f. +Proof. +set V' := @fullv _ V. +set B := vbasis V' => /= x. +rewrite /continuous_at. +rewrite [x in f x](coord_vbasis (memvf x)) raddf_sum. +rewrite (@eq_cvg _ _ _ _ (fun y => \sum_(i < \dim V') coord B i y *: f B`_i)); + last first. + move=> y; rewrite [y in LHS](coord_vbasis (memvf y)) raddf_sum. + by apply: eq_big => // i _; apply: linearZ. +apply: cvg_sum => i _. +rewrite [X in _ --> X]linearZ/= -/B. +apply: cvgZl. +move: x; apply/linear_bounded_continuous/bounded_funP => r/=. +have := @equivalence_norms R V (@normr R V) (@normr0 _ _) (@normr_ge0 _ _) + (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _). +move=> [] M [] M0 MP. +exists (M * r) => x. +move: MP => /(_ x)[] Mx Mx' xr. +apply/(le_trans (le_coord_oo_norm _ _ _))/(le_trans Mx). +rewrite -subr_ge0 -mulrBr; apply: mulr_ge0; first exact: ltW. +by rewrite subr_ge0. +Qed. + +End LinearContinuous. + diff --git a/theories/tvs.v b/theories/tvs.v index fe4359304..46dfb0453 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -90,6 +90,22 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. +Section TopologicalNmodule_Theory. + +Lemma cvg_sum (T : Type) (U : TopologicalNmodule.type) (F : set_system T) + (I : Type) (r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U) : + Filter F -> (forall i, P i -> Ff i x @[x --> F] --> Fa i) -> + \sum_(i <- r | P i) Ff i x @[x --> F] --> \sum_(i <- r| P i) Fa i. +Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed. + +Lemma sum_continuous (T : topologicalType) (M : TopologicalNmodule.type) + (I : Type) (r : seq I) (P : pred I) (F : I -> T -> M) : + (forall i : I, P i -> continuous (F i)) -> + continuous (fun x1 : T => \sum_(i <- r | P i) F i x1). +Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. + +End TopologicalNmodule_Theory. + HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}.