is_derive_trmx (#2060)

* is_derive_trmx

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

* mv instance to unstable

* addressed comments by Pierre

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

Author: 3 people

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
 

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       *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -647,3 +649,28 @@ End Theory.
 Module Import Exports. HB.reexport. End Exports.
 End Norm.
 Export Norm.Exports.
+
+From mathcomp Require Import interval_inference.
+(* 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}.
+
+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.
+(* 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 max_nng_comlaw.
+End MaxNngComLaw.

theories/derive.v

@@ -2511,6 +2511,41 @@ 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.
+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 :
+  derivable M t v -> 'D_v (trmx \o M) t = ('D_v M t)^T.
+Proof.
+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} (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 ->

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.

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.
@@ -172,6 +172,25 @@ Qed.
 
 End mx_norm.
 
+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 _ _ _).
+
+Section norm_trmx.
+Import MaxNngComLaw.
+
+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/=.
+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.
@@ -180,13 +199,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|.
@@ -198,7 +212,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.