From fb9a6ff89af05b803d00df19b0a5d4638a4ca087 Mon Sep 17 00:00:00 2001 From: yosakaon Date: Thu, 4 Dec 2025 01:58:31 +0100 Subject: [PATCH 1/4] derive_sqrt --- theories/realfun.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/theories/realfun.v b/theories/realfun.v index 9ad09712e..922e3a440 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1878,7 +1878,16 @@ rewrite -[x]sqrtK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)). - rewrite !sqrtK//; split; first exact: exprn_derivable. by rewrite exp_derive expr1 scaler1. - by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0. -Unshelve. all: by end_near. Qed. + Unshelve. all: by end_near. Qed. + +Lemma derive_sqrt {K : realType} (r : K) : 0 < r -> + (Num.sqrt^`())%classic r = (2 * Num.sqrt r)^-1 :> K. +Proof. +move=> r0. +rewrite derive1E. +apply: derive_val. +exact: is_derive1_sqrt. +Qed. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. From 2d7da4af92950bdda9a842f89a6e1cf16c3d95e1 Mon Sep 17 00:00:00 2001 From: yosakaon Date: Thu, 4 Dec 2025 01:22:09 +0100 Subject: [PATCH 2/4] rsubmx and lsubmx diff lemmas --- theories/derive.v | 59 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index 616ba19ab..c7090b24c 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -693,6 +693,45 @@ have @f : {linear 'M[R]_(m, n) -> R}. rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous. Qed. +Lemma differentiable_rsubmx0 {n1 n2} t : + differentiable (@rsubmx R 1 n1 n2) t. +Proof. +have lin_rsubmx : linear (@rsubmx R 1 n1 n2). + move=> a b c. + by rewrite linearD//= linearZ. +pose build_lin_rsubmx := GRing.isLinear.Build _ _ _ _ _ lin_rsubmx. +pose Rsubmx : {linear 'rV[R^o]_(n1 + n2) -> 'rV[R^o]_n2} := HB.pack (@rsubmx R _ _ _) build_lin_rsubmx. +apply: (@linear_differentiable _ _ _ _). +move=> /= u A /=. +move/nbhs_ballP=> [e /= e0 eA]. +apply/nbhs_ballP; exists e => //= v [? uv]. +apply: eA; split => //. +(* TODO: lemma *) +move: uv; rewrite /ball/= /mx_ball/ball /= => uv i j. +apply: (le_lt_trans _ (uv i (rshift n1 j))). +by rewrite !mxE. +Qed. + +Lemma differentiable_lsubmx0{n1 n2} t : + differentiable (@lsubmx R 1 n1 n2) t. +Proof. +have lin_lsubmx : linear (@lsubmx R 1 n1 n2). + move=> a b c. + by rewrite linearD//= linearZ. +pose build_lin_lsubmx := GRing.isLinear.Build _ _ _ _ _ lin_lsubmx. +pose Lsubmx : {linear 'rV[R^o]_(n1 + n2) -> 'rV[R^o]_n1} := + HB.pack (@lsubmx R _ _ _) build_lin_lsubmx. +apply: (@linear_differentiable _ _ _ _). +move=> /= u A /=. +move/nbhs_ballP=> [e /= e0 eA]. +apply/nbhs_ballP; exists e => //= v [? uv]. +apply: eA; split => //. +(* TODO: lemma *) +move: uv; rewrite /ball/= /mx_ball/ball /= => uv i j. +apply: (le_lt_trans _ (uv i (lshift n2 j))). +by rewrite !mxE. +Qed. + Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) : continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|. Proof. @@ -760,6 +799,26 @@ move=> dfx dgfx; apply: DiffDef; first exact: differentiable_comp. by rewrite diff_comp // !diff_val. Qed. +Lemma differentiable_rsubmx {n1 n2} + (f : V -> 'rV[R]_(n1 + n2)) t : + (forall x, differentiable f x) -> + differentiable (fun x => rsubmx (f x)) t. +Proof. +move=> /= => df1. +apply: differentiable_comp => //. +exact: differentiable_rsubmx0. +Qed. + +Lemma differentiable_lsubmx {n1 n2} + (f : V -> 'rV[R]_(n1 + n2)) t : + (forall x, differentiable f x) -> + differentiable (fun x => lsubmx (f x)) t. +Proof. +move=> /= => df1. +apply: differentiable_comp => //. +exact: differentiable_lsubmx0. +Qed. + Lemma bilinear_schwarz (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) -> exists2 k, k > 0 & forall u v, `|f u v| <= k * `|u| * `|v|. From 185571f195a8726da6749f4d8349141f7332400e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Jan 2026 15:58:06 +0900 Subject: [PATCH 3/4] changelog, linting --- CHANGELOG_UNRELEASED.md | 5 ++ theories/derive.v | 63 +++---------------- .../normedtype_theory/matrix_normedtype.v | 2 +- theories/realfun.v | 11 +--- theories/topology_theory/matrix_topology.v | 3 +- theories/topology_theory/num_topology.v | 20 +++++- 6 files changed, 38 insertions(+), 66 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dd5e81e1d..cc7f17cab 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -109,6 +109,11 @@ - in `order_topology.v`: + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`, `POrderedPointedTopological` +- in `num_topology.v`: + + lemmas `continuous_rsubmx`, `continuous_lsubmx` + +- in `derive.v`: + + lemmas `differentiable_rsubmx`, `differentiable_lsubmx` ### Changed diff --git a/theories/derive.v b/theories/derive.v index c7090b24c..bfedb93b8 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval poly. From mathcomp Require Import sesquilinear. @@ -693,45 +693,6 @@ have @f : {linear 'M[R]_(m, n) -> R}. rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous. Qed. -Lemma differentiable_rsubmx0 {n1 n2} t : - differentiable (@rsubmx R 1 n1 n2) t. -Proof. -have lin_rsubmx : linear (@rsubmx R 1 n1 n2). - move=> a b c. - by rewrite linearD//= linearZ. -pose build_lin_rsubmx := GRing.isLinear.Build _ _ _ _ _ lin_rsubmx. -pose Rsubmx : {linear 'rV[R^o]_(n1 + n2) -> 'rV[R^o]_n2} := HB.pack (@rsubmx R _ _ _) build_lin_rsubmx. -apply: (@linear_differentiable _ _ _ _). -move=> /= u A /=. -move/nbhs_ballP=> [e /= e0 eA]. -apply/nbhs_ballP; exists e => //= v [? uv]. -apply: eA; split => //. -(* TODO: lemma *) -move: uv; rewrite /ball/= /mx_ball/ball /= => uv i j. -apply: (le_lt_trans _ (uv i (rshift n1 j))). -by rewrite !mxE. -Qed. - -Lemma differentiable_lsubmx0{n1 n2} t : - differentiable (@lsubmx R 1 n1 n2) t. -Proof. -have lin_lsubmx : linear (@lsubmx R 1 n1 n2). - move=> a b c. - by rewrite linearD//= linearZ. -pose build_lin_lsubmx := GRing.isLinear.Build _ _ _ _ _ lin_lsubmx. -pose Lsubmx : {linear 'rV[R^o]_(n1 + n2) -> 'rV[R^o]_n1} := - HB.pack (@lsubmx R _ _ _) build_lin_lsubmx. -apply: (@linear_differentiable _ _ _ _). -move=> /= u A /=. -move/nbhs_ballP=> [e /= e0 eA]. -apply/nbhs_ballP; exists e => //= v [? uv]. -apply: eA; split => //. -(* TODO: lemma *) -move: uv; rewrite /ball/= /mx_ball/ball /= => uv i j. -apply: (le_lt_trans _ (uv i (lshift n2 j))). -by rewrite !mxE. -Qed. - Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) : continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|. Proof. @@ -799,24 +760,18 @@ move=> dfx dgfx; apply: DiffDef; first exact: differentiable_comp. by rewrite diff_comp // !diff_val. Qed. -Lemma differentiable_rsubmx {n1 n2} - (f : V -> 'rV[R]_(n1 + n2)) t : - (forall x, differentiable f x) -> - differentiable (fun x => rsubmx (f x)) t. +Lemma differentiable_rsubmx m {n1 n2} (f : V -> 'M[R]_(m, n1 + n2)) v : + (forall x, differentiable f x) -> differentiable (rsubmx \o f) v. Proof. -move=> /= => df1. -apply: differentiable_comp => //. -exact: differentiable_rsubmx0. +move=> df; apply: differentiable_comp => //. +exact/linear_differentiable/continuous_rsubmx. Qed. -Lemma differentiable_lsubmx {n1 n2} - (f : V -> 'rV[R]_(n1 + n2)) t : - (forall x, differentiable f x) -> - differentiable (fun x => lsubmx (f x)) t. +Lemma differentiable_lsubmx m {n1 n2} (f : V -> 'M[R]_(m, n1 + n2)) v : + (forall x, differentiable f x) -> differentiable (lsubmx \o f) v. Proof. -move=> /= => df1. -apply: differentiable_comp => //. -exact: differentiable_lsubmx0. +move=> df1; apply: differentiable_comp => //. +exact/linear_differentiable/continuous_lsubmx. Qed. Lemma bilinear_schwarz (U V' W' : normedModType R) diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 3c9eb31d1..9d8e502c3 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum matrix interval. From mathcomp Require Import boolp classical_sets interval_inference reals. diff --git a/theories/realfun.v b/theories/realfun.v index 922e3a440..ff9dcfe56 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1878,16 +1878,11 @@ rewrite -[x]sqrtK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)). - rewrite !sqrtK//; split; first exact: exprn_derivable. by rewrite exp_derive expr1 scaler1. - by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0. - Unshelve. all: by end_near. Qed. +Unshelve. all: by end_near. Qed. Lemma derive_sqrt {K : realType} (r : K) : 0 < r -> - (Num.sqrt^`())%classic r = (2 * Num.sqrt r)^-1 :> K. -Proof. -move=> r0. -rewrite derive1E. -apply: derive_val. -exact: is_derive1_sqrt. -Qed. + 'D_1 Num.sqrt r = (2 * Num.sqrt r)^-1. +Proof. by move=> r0; apply: derive_val; exact: is_derive1_sqrt. Qed. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v index 87fbb1338..f51b940a3 100644 --- a/theories/topology_theory/matrix_topology.v +++ b/theories/topology_theory/matrix_topology.v @@ -1,8 +1,9 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. From mathcomp Require Import interval_inference topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. + (**md**************************************************************************) (* # Matrix topology *) (* ``` *) diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index b6ed480b0..8b036ca48 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -3,13 +3,13 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. -From mathcomp Require Import order_topology. +From mathcomp Require Import order_topology matrix_topology. (**md**************************************************************************) (* # Topological notions for numerical types *) (* *) (* We endow `numFieldType` with the types of topological notions (accessible *) -(* with `Import numFieldTopology.Exports). *) +(* with `Import numFieldTopology.Exports`). *) (* *) (******************************************************************************) @@ -378,3 +378,19 @@ have inj_nat_of_rat : injective nat_of_rat. exact/bij_inj. by exists (nat_of_rat \o f) => i j Di Dj /inj_nat_of_rat/inj_f; exact. Qed. + +Lemma continuous_rsubmx {R : numFieldType} m {n1 n2} : + continuous (rsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n2)). +Proof. +move=> u A /nbhs_ballP[e /= e0 eA]. +apply/nbhs_ballP; exists e => //= v [_ uv]; apply: eA; split => // i j. +by apply: (le_lt_trans _ (uv i (rshift n1 j))); rewrite !mxE. +Qed. + +Lemma continuous_lsubmx {R : numFieldType} m {n1 n2} : + continuous (lsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n1)). +Proof. +move=> u A /nbhs_ballP[e /= e0 eA]. +apply/nbhs_ballP; exists e => //= v [_ uv]; apply: eA; split => // i j. +by apply: (le_lt_trans _ (uv i (lshift n2 j))); rewrite !mxE. +Qed. From 0cfdb416bfc1b8293c44fa0c92830324e0f646a4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 5 Jan 2026 18:44:06 +0900 Subject: [PATCH 4/4] apply comments --- theories/derive.v | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index bfedb93b8..36e66ada9 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -760,19 +760,13 @@ move=> dfx dgfx; apply: DiffDef; first exact: differentiable_comp. by rewrite diff_comp // !diff_val. Qed. -Lemma differentiable_rsubmx m {n1 n2} (f : V -> 'M[R]_(m, n1 + n2)) v : - (forall x, differentiable f x) -> differentiable (rsubmx \o f) v. -Proof. -move=> df; apply: differentiable_comp => //. -exact/linear_differentiable/continuous_rsubmx. -Qed. +Lemma differentiable_rsubmx m {n1 n2} v : + differentiable (rsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n2)) v. +Proof. exact/linear_differentiable/continuous_rsubmx. Qed. -Lemma differentiable_lsubmx m {n1 n2} (f : V -> 'M[R]_(m, n1 + n2)) v : - (forall x, differentiable f x) -> differentiable (lsubmx \o f) v. -Proof. -move=> df1; apply: differentiable_comp => //. -exact/linear_differentiable/continuous_lsubmx. -Qed. +Lemma differentiable_lsubmx m {n1 n2} v : + differentiable (lsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n1)) v. +Proof. exact/linear_differentiable/continuous_lsubmx. Qed. Lemma bilinear_schwarz (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) ->