From 85a2a77e5e6173062f400063d9f1d8d4638e04de Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 2 Mar 2026 09:08:51 +0900 Subject: [PATCH] specialized version of is_diff_mx --- CHANGELOG_UNRELEASED.md | 10 +++ theories/derive.v | 78 ++++++++++++++++++- .../normedtype_theory/matrix_normedtype.v | 24 +++++- 3 files changed, 108 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ff11a74fa..2bc3f43b2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,6 +81,16 @@ - in `measurable_structure.v`: + structure `PMeasurable`, notation `pmeasurableType` +- in `matrix_normedtype.v`: + + lemma `continuous_mx` + +- in `derive.v`: + + instance `is_derive_mx` + + fact `dmx` + + lemma `diffmx` + + lemma `is_diff_mx` + + instance `is_diff_mx` + ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: diff --git a/theories/derive.v b/theories/derive.v index 141c53c95..e4a340616 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum matrix interval poly. -From mathcomp Require Import sesquilinear. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum matrix interval. +From mathcomp Require Import poly sesquilinear. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp contra classical_sets. @@ -660,7 +660,7 @@ move=> df; set g := RHS; have glin : linear g. by move=> a u v; rewrite /g linearP /= scalerDl -scalerA. pose glM := GRing.isLinear.Build _ _ _ _ _ glin. pose gL : {linear _ -> _} := HB.pack g glM. -by apply:(@diff_unique _ _ _ gL); have [] := dscalel f df. +by apply: (@diff_unique _ _ _ gL); have [] := dscalel f df. Qed. Lemma differentiableZl (k : V -> R) (f : W) x : @@ -2328,4 +2328,76 @@ rewrite (le_trans (ler_normD _ _))// (splitr e) lerD//. by rewrite sub0r normrN; near: x; exact: dnbhs0_lt. Unshelve. all: by end_near. Qed. +Global Instance is_derive_mx {m n : nat} (M : V -> 'M[R]_(m, n)) + (dM : 'M[R]_(m, n)) (x v : V) : + (forall i j, is_derive x v (fun x => M x i j) (dM i j)) -> + is_derive x v M dM. +Proof. +move=> MdM; apply: DeriveDef; first exact/derivable_mxP. +apply/matrixP => i j. +have [_ <-] := MdM i j. +rewrite derive_mx ?mxE//. +apply/derivable_mxP => i0 j0. +by have [] := MdM i0 j0. +Qed. + +Fact dmx {m n : nat} (M : V -> 'M[R]_(m, n)) (x : V) : + let g := fun x0 : V => (\matrix_(i < m, j < n) 'd M x x0 i j) in + differentiable M x -> + continuous g /\ + M \o shift x = cst (M x) + g +o_ 0 id. +Proof. +move=> dM Mx; split => [|]. +- apply/continuous_mx => i j v; apply/cvgrPdist_le => /= e e0. + case: Mx => -[+ _] => /(_ v)/cvgrPdist_le/(_ _ e0). + apply: filterS => /= t; apply: le_trans. + by rewrite {2}/Num.norm/= mx_normrE (le_trans _ (le_bigmax _ _ (i, j))) ?mxE. +- apply/eqaddoE; rewrite funeqE => y /=. + rewrite (diff_locallyx Mx) /dM !fctE; congr (_ + _ + _). + by apply/matrixP => i j/=; rewrite mxE. +Qed. + +Lemma diffmx {m n : nat} (M : V -> 'M[R]_(m, n)) t : + differentiable M t -> + 'd M (nbhs_filter_on t) = + (fun x0 : V => \matrix_(i < m, j < n) 'd M t x0 i j) :> (_ -> _). +Proof. +move=> dM. +set g := fun x0 : V => \matrix_(i, j) 'd M t x0 i j. +have glin : linear (g : V -> _). + move=> a u w. + by rewrite /g linearD linearZ/=; apply/matrixP => i j; rewrite !mxE. +pose glM := GRing.isLinear.Build _ _ _ _ _ glin. +pose gL : {linear _ -> _} := HB.pack g glM. +by apply: (@diff_unique _ _ _ _ gL); have [? ?] := dmx dM. +Qed. + End pointwise_derive. + +Section Ris_diff_mx. +Local Open Scope classical_set_scope. +Context {R : realFieldType}. + +Global Instance is_diff_mx {m n : nat} (M dM : R -> 'M[R]_(m, n)) (x : R) : + (forall i j, is_diff x (fun x => M x i j) (fun x => dM x i j)) -> + is_diff x M dM. +Proof. +move=> /= MdM. +have diffM : differentiable M (nbhs_filter_on x). + apply/derivable1_diffP; apply/derivable_mxP => i j. + by have [/(@derivable1_diffP _ _ (fun x0 => M x0 i j) x)] := MdM i j. +have diffMx i j : differentiable (fun x0 : R => M x0 i j) x. + by have [/=] := MdM i j. +apply: DiffDef; first exact: diffM. +rewrite diffmx//=; apply/funext => /= v; apply/matrixP => i j. +rewrite !mxE. +have [diffMij dMdM] := MdM i j. +rewrite -deriveE//. +move/(congr1 (fun f => f v)) : dMdM. +rewrite -(deriveE _ diffMij) => <-. +rewrite derive_mx ?mxE//=. +apply/derivable_mxP => i0 j0/=. +by have [/diff_derivable-/(_ v)] := MdM i0 j0. +Qed. + +End Ris_diff_mx. diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 8f835f09c..3cd89248c 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -37,7 +37,7 @@ move=> /= M s /= /(nbhs_ballP (M i j)) [e e0 es]. by apply/nbhs_ballP; exists e => //= N [_ MN]; exact/es/MN. Qed. -#[local]Lemma rV_compact_nondegenerate (T : ptopologicalType) n +#[local] Lemma rV_compact_nondegenerate (T : ptopologicalType) n (A : 'I_n.+1 -> set T) : (forall i, compact (A i)) -> compact [ set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)]. @@ -252,3 +252,25 @@ HB.instance Definition _ (K : numFieldType) m n := (@mx_normZ K m n). End matrix_NormedModule. + +Lemma continuous_mx {V : topologicalType} {R : realFieldType} {m n : nat} + (f : V -> 'M[R]_(m, n)) : + (forall i j, continuous (fun x => f x i j)) <-> + continuous (fun x : V => \matrix_(i < m, j < n) f x i j). +Proof. +split => [cf x|cf i j v]. +- apply/cvgrPdist_le => /= e e0; near=> t. + rewrite /Num.norm/= mx_normrE/= (bigmax_le _ (ltW e0))// => -[i j] _. + rewrite !mxE/=. + move: i j; near: t. + apply: filter_forall => /= i; apply: filter_forall => /= j. + have /(@cvgrPdist_le _ R^o)/(_ _ e0) := cf i j x. + exact: filterS. +- apply/(@cvgrPdist_le _ R^o) => /= e e0. + have /cvgrPdist_le/(_ _ e0) := cf v. + apply: filterS => w. + apply: le_trans. + rewrite [in leRHS]/Num.norm/= mx_normrE/=. + apply: le_trans (le_bigmax _ _ (i, j)). + by rewrite !mxE. +Unshelve. all: by end_near. Qed.