Files

  • mathcomp

    • Top source

    Module mathcomp.reals.prodnormedzmodule

    From HB Require Import structures.
    From mathcomp Require Import boot order 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.

    Unset 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 (
    R
    Source code
     : pzRingType) (
    U
    Source code
     : lmodType R) (
    V
    Source code
     : zmodType) (
    s
    Source code
     : R -> V -> V).
    End Linear1.
    Section Linear2.
    Context (
    R
    Source code
     : pzRingType) (
    U
    Source code
     : lmodType R) (
    V
    Source code
     : zmodType) (
    s
    Source code
     : GRing.Scale.law R V).
    End Linear2.

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

    Definition
    norm

    ereal_ball : forall {R : realFieldType}, \bar R -> R -> \bar R -> bool ereal_ball is not universe polymorphic Arguments ereal_ball {R} x%_ereal_scope r%_ring_scope y%_ereal_scope ereal_ball is transparent Expands to: Constant mathcomp.reals.constructive_ereal.ereal_ball Declared in library mathcomp.reals.constructive_ereal, line 4706, characters 11-21

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

    Lemma
    normD
    Source code
    x
    Source code
    y
    Source 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_eq0
    Source code
    x
    Source 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
    normMn
    Source code
    x
    Source code
    n
    Source code
     : norm (x *+ n) = (norm x) *+ n.
    Proof.
    by rewrite /norm pairMnE -mulr_natl maxr_pMr ?mulr_natl ?normrMn. Qed.

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

    #[export]
    Source code

    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    Num
    Source code
    .Zmodule_isNormed.Build R (U * V)%type
      normD norm_eq0 normMn normrN.

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

    End ProdNormedZmodule.

    Module
    Exports
    Source code
    .
    HB.reexport.
    Definition
    prod_normE
    Source code
     := @prod_normE.
    End Exports.

    End ProdNormedZmodule.
    Export ProdNormedZmodule.Exports.
    Generated by rocqnavi