From d4671d32a7bec8a38e333d8272260dcea7bf7291 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 Jan 2026 00:14:47 +0900 Subject: [PATCH 1/2] derive_mx --- theories/derive.v | 89 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index 18a80fa3df..c91e2e9680 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2125,3 +2125,92 @@ exact/derivable1_diffP/derivable_horner. Qed. End derive_horner. + +Section pointwise_derivable. +Context {R : realFieldType} {V W : normedModType R} {m n : nat}. +Implicit Types M : V -> 'M[R]_(m, n). + +Definition derivable_mx M t v := + forall i j, derivable (fun x => M x i j) t v. + +(* NB: from robot-rocq *) +Lemma derivable_mxP M t v : derivable_mx M t v <-> derivable M t v. +Proof. +split; rewrite /derivable_mx /derivable. +- move=> H. + apply/cvg_ex => /=. + pose l := \matrix_(i < m, j < n) sval (cid ((cvg_ex _).1 (H i j))). + exists l. + apply/cvgrPdist_le => /= e e0. + near=> x. + rewrite /Num.Def.normr/= mx_normrE. + apply: (bigmax_le _ (ltW e0)) => /= i _. + rewrite !mxE/=. + move: i. + near: x. + apply: filter_forall => /= i. + exact: ((@cvgrPdist_le _ _ _ _ (dnbhs_filter 0) _ _).1 + (svalP (cid ((cvg_ex _).1 (H i.1 i.2)))) _ e0). +- move=> /cvg_ex[/= l Hl] i j. + apply/cvg_ex; exists (l i j). + apply/cvgrPdist_le => /= e e0. + move/cvgrPdist_le : Hl => /(_ _ e0)[/= r r0] H. + near=> x. + apply: le_trans; last first. + apply: (H x). + rewrite /ball_/=. + rewrite sub0r normrN. + near: x. + exact: dnbhs0_lt. + near: x. + exact: nbhs_dnbhs_neq. + rewrite [leRHS]/Num.Def.normr/= mx_normrE. + apply: le_trans; last exact: le_bigmax. + by rewrite /= !mxE. +Unshelve. all: by end_near. Qed. + +End pointwise_derivable. + +Section pointwise_derive. +Local Open Scope classical_set_scope. +Context {R : realFieldType} {V W : normedModType R} . + +(* NB: from robot-rocq *) +Lemma derive_mx {m n : nat} (M : V -> 'M[R]_(m, n)) t v : + derivable M t v -> + 'D_v M t = \matrix_(i < m, j < n) 'D_v (fun t => M t i j) t. +Proof. +move=> /cvg_ex[/= l Hl]; apply/cvg_lim => //=. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : (Hl) => /(_ (e / 2)). +rewrite divr_gt0// => /(_ isT)[d /= d0 dle]. +near=> x. +rewrite [in leLHS]/Num.Def.normr/= mx_normrE. +apply/(bigmax_le _ (ltW e0)) => -[/= i j] _. +rewrite [in leLHS]mxE/= [X in _ + X]mxE -[X in X - _](subrK (l i j)). +rewrite -(addrA (_ - _)) (le_trans (ler_normD _ _))// (splitr e) lerD//. +- rewrite mxE. + suff : (h^-1 *: (M (h *: v + t) i j - M t i j)) @[h --> 0^'] --> l i j. + move/cvg_lim => /=; rewrite /derive /= => ->//. + by rewrite subrr normr0 divr_ge0// ltW. + apply/cvgrPdist_le => /= r r0. + move/cvgrPdist_le : Hl => /(_ r r0)[/= s s0] sr. + near=> y. + have : `|l - y^-1 *: (M (y *: v + t) - M t)| <= r. + rewrite sr//=; last by near: y; exact: nbhs_dnbhs_neq. + by rewrite sub0r normrN; near: y; exact: dnbhs0_lt. + apply: le_trans. + rewrite [in leRHS]/Num.Def.normr/= mx_normrE. + by under eq_bigr do rewrite !mxE; exact: (le_bigmax _ _ (i, j)). +- rewrite mxE. + have : `|l - x^-1 *: (M (x *: v + t) - M t)| <= e / 2. + apply: dle => //=; last by near: x; exact: nbhs_dnbhs_neq. + by rewrite sub0r normrN; near: x; exact: dnbhs0_lt. + apply: le_trans. + rewrite [in leRHS]/Num.Def.normr/= mx_normrE/=. + under eq_bigr do rewrite !mxE. + apply: le_trans; last exact: le_bigmax. + by rewrite !mxE. +Unshelve. all: by end_near. Qed. + +End pointwise_derive. From 322306c9fb84692d820bc6697aecf4b3e1b34a5c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 27 Feb 2026 10:00:40 +0900 Subject: [PATCH 2/2] lint --- CHANGELOG_UNRELEASED.md | 2 + theories/derive.v | 92 ++++++++++++++++------------------------- 2 files changed, 38 insertions(+), 56 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0a799011a8..4dd7666702 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -49,6 +49,8 @@ - in `measurable_realfun.v`: + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`, `emeasurable_fun_itv_cc` +- in `derive.v`: + + lemmas `derivable_mxP`, `derive_mx` ### Changed - in `set_interval.v` diff --git a/theories/derive.v b/theories/derive.v index c91e2e9680..2822109ff9 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2130,43 +2130,29 @@ Section pointwise_derivable. Context {R : realFieldType} {V W : normedModType R} {m n : nat}. Implicit Types M : V -> 'M[R]_(m, n). -Definition derivable_mx M t v := - forall i j, derivable (fun x => M x i j) t v. - -(* NB: from robot-rocq *) -Lemma derivable_mxP M t v : derivable_mx M t v <-> derivable M t v. +Lemma derivable_mxP M t v : + derivable M t v <-> forall i j, derivable (fun x => M x i j) t v. Proof. -split; rewrite /derivable_mx /derivable. -- move=> H. - apply/cvg_ex => /=. - pose l := \matrix_(i < m, j < n) sval (cid ((cvg_ex _).1 (H i j))). - exists l. +split=> [|Mvt]. +- move=> /cvg_ex[/= l Mvtl] i j; apply/cvg_ex; exists (l i j). apply/cvgrPdist_le => /= e e0. + move/cvgrPdist_le : Mvtl => /(_ _ e0)[/= r r0] rMvte. near=> x. - rewrite /Num.Def.normr/= mx_normrE. - apply: (bigmax_le _ (ltW e0)) => /= i _. - rewrite !mxE/=. - move: i. - near: x. - apply: filter_forall => /= i. - exact: ((@cvgrPdist_le _ _ _ _ (dnbhs_filter 0) _ _).1 - (svalP (cid ((cvg_ex _).1 (H i.1 i.2)))) _ e0). -- move=> /cvg_ex[/= l Hl] i j. - apply/cvg_ex; exists (l i j). + apply: le_trans (rMvte x _ _). + + rewrite [leRHS]/Num.Def.normr/= mx_normrE. + apply: le_trans; last exact: le_bigmax. + by rewrite !mxE. + + rewrite /ball_/= sub0r normrN. + by near: x; exact: dnbhs0_lt. + + near: x; exact: nbhs_dnbhs_neq. +- apply/cvg_ex => /=. + exists (\matrix_(i < m, j < n) sval (cid ((cvg_ex _).1 (Mvt i j)))). apply/cvgrPdist_le => /= e e0. - move/cvgrPdist_le : Hl => /(_ _ e0)[/= r r0] H. near=> x. - apply: le_trans; last first. - apply: (H x). - rewrite /ball_/=. - rewrite sub0r normrN. - near: x. - exact: dnbhs0_lt. - near: x. - exact: nbhs_dnbhs_neq. - rewrite [leRHS]/Num.Def.normr/= mx_normrE. - apply: le_trans; last exact: le_bigmax. - by rewrite /= !mxE. + rewrite /Num.Def.normr/= mx_normrE (bigmax_le _ (ltW e0))//= => i _. + rewrite !mxE/=. + move: i; near: x; apply: filter_forall => /= i. + exact: ((cvgrPdist_le _ _).1 (svalP (cid ((cvg_ex _).1 (Mvt i.1 i.2))))). Unshelve. all: by end_near. Qed. End pointwise_derivable. @@ -2175,42 +2161,36 @@ Section pointwise_derive. Local Open Scope classical_set_scope. Context {R : realFieldType} {V W : normedModType R} . -(* NB: from robot-rocq *) Lemma derive_mx {m n : nat} (M : V -> 'M[R]_(m, n)) t v : derivable M t v -> 'D_v M t = \matrix_(i < m, j < n) 'D_v (fun t => M t i j) t. Proof. -move=> /cvg_ex[/= l Hl]; apply/cvg_lim => //=. -apply/cvgrPdist_le => /= e e0. -move/cvgrPdist_le : (Hl) => /(_ (e / 2)). -rewrite divr_gt0// => /(_ isT)[d /= d0 dle]. +move=> /cvg_ex[/= l Mvtl]; apply/cvg_lim => //=; apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : (Mvtl) => /(_ (e / 2)) /[!divr_gt0]// /(_ isT)[d /= d0 dle]. near=> x. -rewrite [in leLHS]/Num.Def.normr/= mx_normrE. -apply/(bigmax_le _ (ltW e0)) => -[/= i j] _. -rewrite [in leLHS]mxE/= [X in _ + X]mxE -[X in X - _](subrK (l i j)). -rewrite -(addrA (_ - _)) (le_trans (ler_normD _ _))// (splitr e) lerD//. +rewrite [leLHS]/Num.Def.normr/= mx_normrE (bigmax_le _ (ltW e0))//= => -[i j] _. +rewrite [in leLHS]mxE/= [X in _ + X]mxE -(subrKA (l i j)). +rewrite (le_trans (ler_normD _ _))// (splitr e) lerD//. - rewrite mxE. suff : (h^-1 *: (M (h *: v + t) i j - M t i j)) @[h --> 0^'] --> l i j. move/cvg_lim => /=; rewrite /derive /= => ->//. by rewrite subrr normr0 divr_ge0// ltW. apply/cvgrPdist_le => /= r r0. - move/cvgrPdist_le : Hl => /(_ r r0)[/= s s0] sr. + move/cvgrPdist_le : Mvtl => /(_ r r0)[/= s s0] sr. near=> y. - have : `|l - y^-1 *: (M (y *: v + t) - M t)| <= r. - rewrite sr//=; last by near: y; exact: nbhs_dnbhs_neq. - by rewrite sub0r normrN; near: y; exact: dnbhs0_lt. - apply: le_trans. - rewrite [in leRHS]/Num.Def.normr/= mx_normrE. - by under eq_bigr do rewrite !mxE; exact: (le_bigmax _ _ (i, j)). + apply: (@le_trans _ _ (`|l - y^-1 *: (M (y *: v + t) - M t)|)). + rewrite [in leRHS]/Num.Def.normr/= mx_normrE. + by under eq_bigr do rewrite !mxE; exact: (le_bigmax _ _ (i, j)). + rewrite sr//=; last by near: y; exact: nbhs_dnbhs_neq. + by rewrite sub0r normrN; near: y; exact: dnbhs0_lt. - rewrite mxE. - have : `|l - x^-1 *: (M (x *: v + t) - M t)| <= e / 2. - apply: dle => //=; last by near: x; exact: nbhs_dnbhs_neq. - by rewrite sub0r normrN; near: x; exact: dnbhs0_lt. - apply: le_trans. - rewrite [in leRHS]/Num.Def.normr/= mx_normrE/=. - under eq_bigr do rewrite !mxE. - apply: le_trans; last exact: le_bigmax. - by rewrite !mxE. + apply: (@le_trans _ _ `|l - x^-1 *: (M (x *: v + t) - M t)|). + rewrite [in leRHS]/Num.Def.normr/= mx_normrE/=. + under eq_bigr do rewrite !mxE. + apply: le_trans; last exact: le_bigmax. + by rewrite !mxE. + apply: dle => //=; last by near: x; exact: nbhs_dnbhs_neq. + by rewrite sub0r normrN; near: x; exact: dnbhs0_lt. Unshelve. all: by end_near. Qed. End pointwise_derive.