From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum.
Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.subring_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
Require Import signed.

(******************************************************************************)
(* This file equips the product of two normedZmodTypes with a canonical       *)
(* normedZmodType structure. It is a short file that has been added here for  *)
(* convenience during the rebase of MathComp-Analysis on top of MathComp 1.1. *)
(* The contents is likely to be moved elsewhere.                              *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory Num.Theory.

Module ProdNormedZmodule.
Section ProdNormedZmodule.
Context {R : numDomainType} {U V : normedZmodType R}.

Definition norm (x : U * V) : R := Num.max `|x.1| `|x.2|.

Lemma normD x y : norm (x + y) <= norm x + norm y.
R: numDomainType
U, V: normedZmodType R
x, y: pair_zmodType U V
norm (x + y) <= norm x + norm y
Proof.
2
rewrite /norm num_le_maxl !(le_trans (ler_norm_add _ _)) ?ler_add//;
by rewrite comparable_le_maxr ?lexx ?orbT// real_comparable.
Qed.

Lemma norm_eq0 x : norm x = 0 -> x = 0.
5
6
x: (U * V)%type
norm x = 0 -> x = 0
Proof.
b
case: x => x1 x2 /eqP; rewrite eq_le num_le_maxl 2!normr_le0 -andbA/=.
5
6
x1: U
x2: V
[&& x1 == 0, x2 == 0 & 0 <= norm (x1, x2)] ->
(x1, x2) = 0
by case/and3P => /eqP -> /eqP ->.
Qed.

Lemma normMn x n : norm (x *+ n) = (norm x) *+ n.
5
6
x: pair_zmodType U V
n: nat
norm (x *+ n) = norm x *+ n
Proof.
19 by rewrite /norm pairMnE -mulr_natl maxr_pmulr ?mulr_natl ?normrMn. Qed.

Lemma normrN x : norm (- x) = norm x.
5
6
1c
norm (- x) = norm x
Proof.
21 by rewrite /norm/= !normrN. Qed.

Definition normedZmodMixin :
  @Num.normed_mixin_of R [zmodType of U * V] (Num.NumDomain.class R) :=
  @Num.NormedMixin _ _ _ norm normD norm_eq0 normMn normrN.

Canonical normedZmodType := NormedZmodType R (U * V) normedZmodMixin.

Lemma prod_normE (x : normedZmodType) : `|x| = Num.max `|x.1| `|x.2|.
5
U, V: Num.NormedZmodule.Exports.normedZmodType R
x: normedZmodType
`|x| = Num.max `|x.1| `|x.2|
Proof.
27 by []. Qed.

End ProdNormedZmodule.

Module Exports.
Canonical normedZmodType.
Ignoring canonical projection to prod by
Num.NormedZmodule.sort in @normedZmodType: redundant
with @normedZmodType
[redundant-canonical-projection,typechecker]
Definition prod_normE := @prod_normE.
End Exports.

End ProdNormedZmodule.
Export ProdNormedZmodule.Exports.