changelog, linting

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -106,6 +106,11 @@
 
 - in `lebesgue_integrable.v`:
   + lemma `integrable_norm`
+- in `num_topology.v`:
+  + lemmas `continuous_rsubmx`, `continuous_lsubmx`
+
+- in `derive.v`:
+  + lemmas `differentiable_rsubmx`, `differentiable_lsubmx`
 
 ### Changed
 

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)

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.

theories/realfun.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 ssrint.
 From mathcomp Require Import archimedean interval.
@@ -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.

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                                                          *)
 (* ```                                                                        *)

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.