Files

  • mathcomp

    • Module mathcomp.reals.prodnormedzmodule

    From HB Require Import structures.
    From mathcomp Require Import all_ssreflect_compat fingroup ssralg poly ssrnum.
    From mathcomp Require Import all_classical.
    From mathcomp Require Import interval_inference.

    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 SsrOldRewriteGoalsOrder.  
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.

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

    Section Linear1.
    Context (
    RSource code
     : pzRingType) (
    USource code
     : lmodType R) (
    VSource code
     : zmodType) (
    sSource code
     : R -> V -> V).
    HBSource code
    .
    instanceSource code
    DefinitionSource code
    _Source code
    :=Source code
    gen_eqMixinSource code
     {linear U -> V | s}.
    HBSource code
    .
    instanceSource code
    DefinitionSource code
    _Source code
    :=Source code
    gen_choiceMixinSource code
     {linear U -> V | s}.
    End Linear1.
    Section Linear2.
    Context (
    RSource code
     : pzRingType) (
    USource code
     : lmodType R) (
    VSource code
     : zmodType) (
    sSource code
     : GRing.Scale.law R V).
    HBSource code
    .
    instanceSource code
    DefinitionSource code
    _Source code
    :=Source code

      isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0.
    End Linear2.

    Module
    ProdNormedZmoduleSource code
    .
    Section ProdNormedZmodule.
    Context {
    RSource code
     : numDomainType} {
    USource code
    VSource code
     : normedZmodType R}.

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

    Lemma
    normDSource code
    xSource code
    ySource code
     : norm (x + y) <= norm x + norm y.
    Proof.
    rewrite /norm num_ge_max !(le_trans (ler_normD _ _)) ?lerD//;
    by rewrite comparable_le_max ?lexx ?orbT// real_comparable.
    Qed.

    Lemma
    norm_eq0Source code
    xSource code
     : norm x = 0 -> x = 0.
    Proof.
    case: x => x1 x2 /eqP; rewrite eq_le num_ge_max 2!normr_le0 -andbA/=.
    by case/and3P => /eqP -> /eqP ->.
    Qed.

    Lemma
    normMnSource code
    xSource code
    nSource code
     : norm (x *+ n) = (norm x) *+ n.
    Proof.
    by rewrite /norm pairMnE -mulr_natl maxr_pMr ?mulr_natl ?normrMn. Qed.

    Lemma
    normrNSource code
    xSource code
     : norm (- x) = norm x.
    Proof.
    by rewrite /norm/= !normrN. Qed.

    #[export]Source code

    HBSource code
    .
    instanceSource code
    DefinitionSource code
    _Source code
    :=Source code
    NumSource code
    .Zmodule_isNormed.Build R (U * V)%type
      normD norm_eq0 normMn normrN.

    Lemma
    prod_normESource code
     (
    xSource code
     : U * V) : `|x| = Num.max `|x.1| `|x.2|.
    Proof.
    by []. Qed.

    End ProdNormedZmodule.

    Module
    ExportsSource code
    .
    HB.reexport.
    Definition
    prod_normE
    Used by
    • mathcomp.analysis.derive
    • mathcomp.analysis.normedtype_theory.normed_module
    Source code
     := @prod_normE.
    End Exports.

    End ProdNormedZmodule.
    Export ProdNormedZmodule.Exports.
    Generated by rocqnavi

    Source

    Uses
    Used By