From 6ca700487faba07997a222e77c795d1e14475067 Mon Sep 17 00:00:00 2001 From: yosakaon Date: Wed, 29 Jul 2026 11:26:03 +0200 Subject: [PATCH 1/3] is_derive_trmx Co-authored-by: Reynald Affeldt --- theories/derive.v | 60 +++++++++++++++++++ .../normedtype_theory/matrix_normedtype.v | 28 +++++++++ 2 files changed, 88 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index bf30479a4c..1f1bb8e057 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2511,6 +2511,66 @@ apply/derivable_mxP => i0 j0. by have [] := MdM i0 j0. Qed. +Lemma derivable_trmx m n (M : V -> 'M[R]_(m, n)) t v : + derivable (fun x => (M x)^T) t v = derivable M t v. +Proof. +rewrite propeqE; split; rewrite /derivable/=. +- move=> /cvg_ex[/= l Hl]. + apply/cvg_ex => /=; exists l^T. + apply/cvgrPdist_le => /= e e0. + move/cvgrPdist_le : Hl => /(_ _ e0)[/= r r0 re]. + near=> x. + rewrite [leLHS](_ : _ = + `|l - x^-1 *: ((M (x *: v + t))^T - (M t)^T)|); last 2 first. + rewrite -[RHS]norm_trmx. + rewrite [in RHS]linearD/=. + rewrite [in RHS]linearN/=. + congr (`| _ - _ |). + rewrite [RHS]linearZ/=. + rewrite [in RHS]linearB. + by rewrite /= !trmxK. + apply: re => /=. + rewrite sub0r normrN. + by near: x; exact: dnbhs0_lt. + by near: x; exact: nbhs_dnbhs_neq. +- move=> /cvg_ex[/= l Hl]. + apply/cvg_ex => /=; exists l^T. + apply/cvgrPdist_le => /= e e0. + move/cvgrPdist_le : Hl => /(_ _ e0)[/= r r0 re]. + near=> x. + rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t)) - (M t))|); last 2 first. + rewrite -[RHS]norm_trmx. + rewrite [in RHS]linearD/=. + rewrite [in RHS]linearN/=. + congr (`| _ - _ |). + rewrite [RHS]linearZ/=. + by rewrite [in RHS]linearB. + apply: re => /=. + rewrite sub0r normrN. + by near: x; exact: dnbhs0_lt. + by near: x; exact: nbhs_dnbhs_neq. +Unshelve. all: by end_near. Qed. + +Lemma derive_trmx {m n : nat} (M : V -> 'M[R]_(m, n)) t v : + derivable M t v -> 'D_v (trmx \o M) t = ('D_v M t)^T. +Proof. +move=> Mt1. +rewrite !derive_mx//=. + by rewrite derivable_trmx. +apply/matrixP => i j; rewrite !mxE. +by under eq_fun do rewrite mxE. +Qed. + +Global Instance is_derive_trmx {m n : nat} + (f : V -> 'M[R]_(m, n)) (f' : 'M[R]_(m, n)) (t : V) w: + is_derive t w f f' -> is_derive t w (fun x => (f x)^T) f'^T. +Proof. +move=> fD. +have fDer : derivable f t w by case: fD. +apply/DeriveDef; last by have [_ <-] := fD; rewrite derive_trmx. +by rewrite derivable_trmx. +Qed. + Fact dmx {m n : nat} (M : V -> 'M[R]_(m, n)) (x : V) : let g := fun t : V => (\matrix_(i < m, j < n) 'd M x t i j) in differentiable M x -> diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 44adaa10ce..f804719303 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -172,6 +172,34 @@ Qed. End mx_norm. +Section norm_trmx. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import Order.Def. +Local Open Scope ring_scope. +Lemma nng_max0r {K : realFieldType} : left_id ((0:K)%:nng) (@maxr {nonneg K}). +Proof. +move=> x. +rewrite /max; case: ifPn => //. +rewrite -leNgt => x0. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + exact: x0. +by have : 0 <= x%:nngnum by []. (* NB: this should be automatic *) +Qed. + +HB.instance Definition _ {K : realFieldType} := + Monoid.isComLaw.Build {nonneg K} 0%:nng max maxA maxC nng_max0r. + +Lemma norm_trmx m n {R : realFieldType} (M : 'M[R]_(m, n)) : mx_norm (M^T) = mx_norm M. +Proof. +rewrite [LHS]mx_normE/=. +under eq_bigr do rewrite mxE /=. +rewrite -(pair_big xpredT xpredT (fun i j => `|M j i|%:nng))/=. +by rewrite exchange_big//= pair_big. +Qed. + +End norm_trmx. + Lemma mx_normrE (K : realDomainType) (m n : nat) (x : 'M[K]_(m, n)) : mx_norm x = \big[maxr/0]_ij `|x ij.1 ij.2|. Proof. From 6b551e2f87e89356a45ed15da4a22ddd3a6b3d92 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 23 Aug 2026 16:29:55 +0900 Subject: [PATCH 2/3] mv instance to unstable --- CHANGELOG_UNRELEASED.md | 6 +++ classical/unstable.v | 18 ++++++++ theories/derive.v | 42 +++++++------------ .../lebesgue_integral_theory/radon_nikodym.v | 2 - .../normedtype_theory/matrix_normedtype.v | 37 ++++------------ 5 files changed, 48 insertions(+), 57 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3caa73665c..6e2cb2a576 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -57,6 +57,12 @@ - in `measurable_realfun.v`: + lemma `measurable_bigmaxr` +- in `matrix_normedtype.v`: + + lemma `norm_trmx` + +- in `derive.v`: + + lemmas `derivable_trmx`, `derive_trmx` + + global instance `is_derive_trmx` ### Changed diff --git a/classical/unstable.v b/classical/unstable.v index cfa0e8083a..99367f8ff1 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -647,3 +647,21 @@ End Theory. Module Import Exports. HB.reexport. End Exports. End Norm. Export Norm.Exports. + +From mathcomp Require Import interval_inference. +Section nng_comlaw. +Import Num.Def. +Context {K : realFieldType}. + +Let nng_max0r : left_id ((0 : K)%:nng) (@maxr {nonneg K}). +Proof. +move=> x; rewrite /maxr; case: ifPn => //. +rewrite -leNgt => x0. +apply/eqP; rewrite eq_le x0 andbT. +by have : 0 <= x%:nngnum by []. (* NB: why isn't this automatic? *) +Qed. + +HB.instance Definition _ := + Monoid.isComLaw.Build {nonneg K} 0%:nng maxr maxA maxC nng_max0r. + +End nng_comlaw. diff --git a/theories/derive.v b/theories/derive.v index 1f1bb8e057..c0358b120a 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2511,58 +2511,46 @@ apply/derivable_mxP => i0 j0. by have [] := MdM i0 j0. Qed. -Lemma derivable_trmx m n (M : V -> 'M[R]_(m, n)) t v : +Lemma derivable_trmx {m n} (M : V -> 'M[R]_(m, n)) t v : derivable (fun x => (M x)^T) t v = derivable M t v. Proof. rewrite propeqE; split; rewrite /derivable/=. -- move=> /cvg_ex[/= l Hl]. - apply/cvg_ex => /=; exists l^T. +- move=> /cvg_ex[/= l Ml]; apply/cvg_ex => /=; exists l^T. apply/cvgrPdist_le => /= e e0. - move/cvgrPdist_le : Hl => /(_ _ e0)[/= r r0 re]. + move/cvgrPdist_le : Ml => /(_ _ e0)[/= r r0 re]. near=> x. - rewrite [leLHS](_ : _ = - `|l - x^-1 *: ((M (x *: v + t))^T - (M t)^T)|); last 2 first. - rewrite -[RHS]norm_trmx. - rewrite [in RHS]linearD/=. - rewrite [in RHS]linearN/=. + rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t))^T - (M t)^T)|). + rewrite -[RHS]norm_trmx [in RHS]linearD/= [in RHS]linearN/=. congr (`| _ - _ |). - rewrite [RHS]linearZ/=. - rewrite [in RHS]linearB. - by rewrite /= !trmxK. + by rewrite [RHS]linearZ/= [in RHS]linearB /= !trmxK. apply: re => /=. rewrite sub0r normrN. by near: x; exact: dnbhs0_lt. by near: x; exact: nbhs_dnbhs_neq. -- move=> /cvg_ex[/= l Hl]. - apply/cvg_ex => /=; exists l^T. +- move=> /cvg_ex[/= l Ml]; apply/cvg_ex => /=; exists l^T. apply/cvgrPdist_le => /= e e0. - move/cvgrPdist_le : Hl => /(_ _ e0)[/= r r0 re]. + move/cvgrPdist_le : Ml => /(_ _ e0)[/= r r0 re]. near=> x. - rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t)) - (M t))|); last 2 first. - rewrite -[RHS]norm_trmx. - rewrite [in RHS]linearD/=. - rewrite [in RHS]linearN/=. + rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t)) - (M t))|). + rewrite -[RHS]norm_trmx [in RHS]linearD/= [in RHS]linearN/=. congr (`| _ - _ |). - rewrite [RHS]linearZ/=. - by rewrite [in RHS]linearB. + by rewrite [RHS]linearZ/= [in RHS]linearB. apply: re => /=. rewrite sub0r normrN. by near: x; exact: dnbhs0_lt. by near: x; exact: nbhs_dnbhs_neq. Unshelve. all: by end_near. Qed. -Lemma derive_trmx {m n : nat} (M : V -> 'M[R]_(m, n)) t v : +Lemma derive_trmx {m n} (M : V -> 'M[R]_(m, n)) t v : derivable M t v -> 'D_v (trmx \o M) t = ('D_v M t)^T. Proof. -move=> Mt1. -rewrite !derive_mx//=. - by rewrite derivable_trmx. +move=> Mtv; rewrite !derive_mx//=; first by rewrite derivable_trmx. apply/matrixP => i j; rewrite !mxE. by under eq_fun do rewrite mxE. Qed. -Global Instance is_derive_trmx {m n : nat} - (f : V -> 'M[R]_(m, n)) (f' : 'M[R]_(m, n)) (t : V) w: +Global Instance is_derive_trmx {m n} (f : V -> 'M[R]_(m, n)) (f' : 'M[R]_(m, n)) + (t : V) w : is_derive t w f f' -> is_derive t w (fun x => (f x)^T) f'^T. Proof. move=> fD. diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v index 161f6cffd1..fed795f0b6 100644 --- a/theories/lebesgue_integral_theory/radon_nikodym.v +++ b/theories/lebesgue_integral_theory/radon_nikodym.v @@ -2,8 +2,6 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap fingroup perm rat. -#[warning="-warn-library-file-internal-analysis"] -From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets cardinality functions fsbigop set_interval reals. From mathcomp Require Import topology ereal numfun normedtype derive sequences. diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index f804719303..4c6fa0e4d1 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -172,34 +172,20 @@ Qed. End mx_norm. -Section norm_trmx. - -Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import Order.Def. -Local Open Scope ring_scope. -Lemma nng_max0r {K : realFieldType} : left_id ((0:K)%:nng) (@maxr {nonneg K}). -Proof. -move=> x. -rewrite /max; case: ifPn => //. -rewrite -leNgt => x0. -apply/eqP; rewrite eq_le; apply/andP; split; last first. - exact: x0. -by have : 0 <= x%:nngnum by []. (* NB: this should be automatic *) -Qed. - -HB.instance Definition _ {K : realFieldType} := - Monoid.isComLaw.Build {nonneg K} 0%:nng max maxA maxC nng_max0r. +HB.instance Definition _ {K : numDomainType} m n := + Num.Zmodule_isNormed.Build K 'M[K]_(m, n) + (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _) + (@mx_norm_natmul _ _ _) (@mx_normN _ _ _). -Lemma norm_trmx m n {R : realFieldType} (M : 'M[R]_(m, n)) : mx_norm (M^T) = mx_norm M. +Lemma norm_trmx {R : realFieldType} m n (M : 'M[R]_(m, n)) : + mx_norm (M^T) = mx_norm M. Proof. rewrite [LHS]mx_normE/=. -under eq_bigr do rewrite mxE /=. +under eq_bigr do rewrite mxE/=. rewrite -(pair_big xpredT xpredT (fun i j => `|M j i|%:nng))/=. by rewrite exchange_big//= pair_big. Qed. -End norm_trmx. - Lemma mx_normrE (K : realDomainType) (m n : nat) (x : 'M[K]_(m, n)) : mx_norm x = \big[maxr/0]_ij `|x ij.1 ij.2|. Proof. @@ -208,13 +194,8 @@ elim/big_ind2 : _ => //= a a' b b' ->{a'} ->{b'}. by have [ab|ab] := leP a b; [rewrite max_r | rewrite max_l // ltW]. Qed. -HB.instance Definition _ (K : numDomainType) (m n : nat) := - Num.Zmodule_isNormed.Build K 'M[K]_(m, n) - (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _) - (@mx_norm_natmul _ _ _) (@mx_normN _ _ _). - Section example_of_sharing. -Variables (K : numDomainType). +Context {K : numDomainType}. Example matrix_triangle m n (M N : 'M[K]_(m, n)) : `|M + N| <= `|M| + `|N|. @@ -226,7 +207,7 @@ Proof. exact: ler_normD. Qed. End example_of_sharing. Section matrix_pseudoMetricNormedZmod. -Variables (K : numFieldType) (m n : nat). +Context {K : numFieldType} {m n : nat}. Local Lemma ball_gt0 (x y : 'M[K]_(m, n)) e : ball x e y -> 0 < e. Proof. by case. Qed. From 9e14b323acb193c0a1c7cdd7dc607604ed976359 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 27 Aug 2026 11:18:18 +0900 Subject: [PATCH 3/3] addressed comments by Pierre Co-authored-by: Pierre Roux --- classical/unstable.v | 15 ++++++-- theories/derive.v | 37 ++++++------------- .../normedtype_theory/matrix_normedtype.v | 9 ++++- 3 files changed, 31 insertions(+), 30 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 99367f8ff1..7b50920ea6 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -38,6 +38,8 @@ From mathcomp Require Import vector archimedean interval matrix. (* K is a numDomainType. *) (* L is a lmodType K. *) (* The HB class is Norm. *) +(* Module MaxNngComLaw == contains on instance of Monoid.isComLaw on *) +(* (@maxr {nonneg _}) to be used with caution *) (* ``` *) (* *) (******************************************************************************) @@ -649,7 +651,10 @@ End Norm. Export Norm.Exports. From mathcomp Require Import interval_inference. -Section nng_comlaw. +(* NB: This module adds an instance of `Monoid.Law.sort` on `Order.max` + although there is already one. Use with caution. *) +Module MaxNngComLaw. +Section max_nng_comlaw. Import Num.Def. Context {K : realFieldType}. @@ -658,10 +663,14 @@ Proof. move=> x; rewrite /maxr; case: ifPn => //. rewrite -leNgt => x0. apply/eqP; rewrite eq_le x0 andbT. -by have : 0 <= x%:nngnum by []. (* NB: why isn't this automatic? *) +(* NB: the goal is `widen_itv 0%:itv <= x`, which does not match the syntax to + trigger the hint for `ge0` as can be seen at + https://github.com/math-comp/math-comp/blob/900e37912dbecbd3c04d3c1b320efe721d3f56dd/algebra/interval_inference.v#L770 *) +by rewrite -num_le/=. Qed. HB.instance Definition _ := Monoid.isComLaw.Build {nonneg K} 0%:nng maxr maxA maxC nng_max0r. -End nng_comlaw. +End max_nng_comlaw. +End MaxNngComLaw. diff --git a/theories/derive.v b/theories/derive.v index c0358b120a..e460223a4e 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2514,31 +2514,18 @@ Qed. Lemma derivable_trmx {m n} (M : V -> 'M[R]_(m, n)) t v : derivable (fun x => (M x)^T) t v = derivable M t v. Proof. -rewrite propeqE; split; rewrite /derivable/=. -- move=> /cvg_ex[/= l Ml]; apply/cvg_ex => /=; exists l^T. - apply/cvgrPdist_le => /= e e0. - move/cvgrPdist_le : Ml => /(_ _ e0)[/= r r0 re]. - near=> x. - rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t))^T - (M t)^T)|). - rewrite -[RHS]norm_trmx [in RHS]linearD/= [in RHS]linearN/=. - congr (`| _ - _ |). - by rewrite [RHS]linearZ/= [in RHS]linearB /= !trmxK. - apply: re => /=. - rewrite sub0r normrN. - by near: x; exact: dnbhs0_lt. - by near: x; exact: nbhs_dnbhs_neq. -- move=> /cvg_ex[/= l Ml]; apply/cvg_ex => /=; exists l^T. - apply/cvgrPdist_le => /= e e0. - move/cvgrPdist_le : Ml => /(_ _ e0)[/= r r0 re]. - near=> x. - rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t)) - (M t))|). - rewrite -[RHS]norm_trmx [in RHS]linearD/= [in RHS]linearN/=. - congr (`| _ - _ |). - by rewrite [RHS]linearZ/= [in RHS]linearB. - apply: re => /=. - rewrite sub0r normrN. - by near: x; exact: dnbhs0_lt. - by near: x; exact: nbhs_dnbhs_neq. +suff: forall N, derivable N t v -> derivable (fun x => (N x)^T) t v. + move=> suf; apply/propext; split; last exact: suf. + by move=> /suf; under eq_fun do rewrite trmxK. +move=> {}m {}n {}M /cvg_ex[/= l Ml]; apply/cvg_ex => /=; exists l^T. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : Ml => /(_ _ e0)[/= r r0 re]. +near=> x. +rewrite [leLHS](_ : _ = `|l - x^-1 *: (M (x *: v + t) - M t)|). + rewrite -[RHS]norm_trmx [in RHS]linearD/= [in RHS]linearN/=. + by congr (`| _ - _ |); rewrite [RHS]linearZ/= [in RHS]linearB. +apply: re => /=; last by near: x; exact: nbhs_dnbhs_neq. +by rewrite sub0r normrN; near: x; exact: dnbhs0_lt. Unshelve. all: by end_near. Qed. Lemma derive_trmx {m n} (M : V -> 'M[R]_(m, n)) t v : diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 4c6fa0e4d1..89085de736 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -109,7 +109,7 @@ by rewrite predeqE => x /=; split => [ _ | _ []//]; apply/rowP => -[]. Qed. Section mx_norm. -Variables (K : numDomainType) (m n : nat). +Context [K : numDomainType] {m n : nat}. Implicit Types x y : 'M[K]_(m, n). Definition mx_norm x : K := (\big[maxr/0%:nng]_i `|x i.1 i.2|%:nng)%:num. @@ -177,8 +177,11 @@ HB.instance Definition _ {K : numDomainType} m n := (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _) (@mx_norm_natmul _ _ _) (@mx_normN _ _ _). +Section norm_trmx. +Import MaxNngComLaw. + Lemma norm_trmx {R : realFieldType} m n (M : 'M[R]_(m, n)) : - mx_norm (M^T) = mx_norm M. + mx_norm M^T = mx_norm M. Proof. rewrite [LHS]mx_normE/=. under eq_bigr do rewrite mxE/=. @@ -186,6 +189,8 @@ rewrite -(pair_big xpredT xpredT (fun i j => `|M j i|%:nng))/=. by rewrite exchange_big//= pair_big. Qed. +End norm_trmx. + Lemma mx_normrE (K : realDomainType) (m n : nat) (x : 'M[K]_(m, n)) : mx_norm x = \big[maxr/0]_ij `|x ij.1 ij.2|. Proof.