Skip to content

is_derive_trmx #2060

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
yosakaon wants to merge 2 commits into
base: master
Choose a base branch
from
Open

is_derive_trmx #2060

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
41381c2
is_derive_trmx
yosakaon Jul 29, 2026
3b0b8c5
mv instance to unstable
affeldt-aist Aug 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,13 @@
- in `Rstruct_topology.v`:
+ lemmas `RcosE`, `Rtrigo_PIE`, `RsinE`

- in `matrix_normedtype.v`:
+ lemma `norm_trmx`

- in `derive.v`:
+ lemmas `derivable_trmx`, `derive_trmx`
+ global instance `is_derive_trmx`

### Changed

- in `derive.v`:
Expand Down
18 changes: 18 additions & 0 deletions classical/unstable.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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? *)

@affeldt-aist affeldt-aist Aug 23, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was a bit surprised that we need to insert this have. Maybe there is some automation in interval_inference.v that does not work as expected? @proux01 ?

@proux01 proux01 Aug 24, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Goal is widen_itv 0%:itv <= x (with the order on Itv.t), of course this is convertible to 0 <= x%:num (as shown by rewrite /Order.le/= /Order.PreCancelPartial.le/=) but trigerring hints for auto for ge0 do not match that syntactic pattern https://github.com/math-comp/math-comp/blob/900e37912dbecbd3c04d3c1b320efe721d3f56dd/algebra/interval_inference.v#L770 . So I'd say it's not expected to be simpler, except maybe by rewrite -num_le/=

Qed.

HB.instance Definition _ :=
Monoid.isComLaw.Build {nonneg K} 0%:nng maxr maxA maxC nng_max0r.

End nng_comlaw.
48 changes: 48 additions & 0 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2511,6 +2511,54 @@ 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/=.
Comment on lines +2514 to +2517

@proux01 proux01 Aug 24, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks like essentially two times the same proof, couldn't it be factored? (I would expect ``derivable M -> derivable M^Tto be enough to provederivable M^T -> derivable M` since `derivable M^T -> derivable M^T^T` and `M^T^T = M`)

- 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.
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 ->
Expand Down
2 changes: 0 additions & 2 deletions theories/lebesgue_integral_theory/radon_nikodym.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
23 changes: 16 additions & 7 deletions theories/normedtype_theory/matrix_normedtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,20 @@ 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 _ _ _).

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.

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.
Expand All @@ -180,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|.
Expand All @@ -198,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.
Expand Down
Loading