Files

  • mathcomp

    • Top source

    Module mathcomp.analysis_stdlib.Rstruct_topology

    # Compatibility with the real numbers of Stdlib Extension to Rstruct.v (lemmas about continuity)

    From Stdlib Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
    From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
    From Stdlib Require Import Rtrigo1 Reals.
    From HB Require Import structures.
    From mathcomp Require Import boot order ssralg ssrnum archimedean.
    From mathcomp Require Import interval arithmetic_tactic.
    From mathcomp Require Import boolp classical_sets reals interval_inference.
    From mathcomp Require Export Rstruct.
    From mathcomp Require Import topology.
    From mathcomp Require normedtype sequences.
    From mathcomp Require exp.
    From mathcomp Require trigonometry_functions.

    Unset SsrOldRewriteGoalsOrder.
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.
    Import Order.TTheory GRing.Theory Num.Theory.

    Local Open Scope R_scope.
    Local Open Scope ring_scope.

    Section analysis_struct.

    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    PseudoMetric
    Source code
    .copy R R^o.
    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    Pointed
    Source code
    .copy R R^o.

    Lemma
    continuity_pt_nbhs
    Source code
     (
    f
    Source code
     : R -> R)
    x
    Source code
     :
      continuity_pt f x <->
      forall
    eps
    Source code
     : {posnum R}, nbhs x (fun
    u
    Source code
     => `|f u - f x| < eps%:num).
    Proof.
    split=> [fcont e|fcont _/RltP/posnumP[e]]; last first.
      have [_/posnumP[d] xd_fxe] := fcont e.
      exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num].
      by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC.
    have /RltP egt0 := [gt0 of e%:num].
    have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0.
    exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney].
      by rewrite subrr normr0.
    apply/RltP/dx_fxe; split; first by split=> //; apply/eqP.
    by have /RltP := xyd; rewrite distrC.
    Qed.

    Lemma
    continuity_pt_cvg
    Source code
     (
    f
    Source code
     : R -> R) (
    x
    Source code
     : R) :
      continuity_pt f x <-> {for x, continuous f}.
    Proof.
    eapply iff_trans; first exact: continuity_pt_nbhs.
    apply iff_sym.
    have FF : Filter (f @ x)%classic.
      by typeclasses eauto.
      (*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*)
    case: (@fcvg_ballP _ _ (f @ x)%classic FF (f x)) => {FF}H1 H2.
    (* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *)
    split => [{H2} - /H1 {}H1 eps|{H1} H].
    - have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num.
      exists x0%:num => //= Hx0' /Hx0 /=.
      by rewrite /= distrC; apply.
    - apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0].
      exists x0%:num => //= y /Hx0 /= {}Hx0.
      by rewrite /ball /= distrC.
    Qed.

    Lemma
    continuity_ptE
    Source code
     (
    f
    Source code
     : R -> R) (
    x
    Source code
     : R) :
      continuity_pt f x <-> {for x, continuous f}.
    Proof.
    exact: continuity_pt_cvg. Qed.

    Local Open Scope classical_set_scope.

    Lemma
    continuity_pt_cvg'
    Source code
    f
    Source code
    x
    Source code
     :
      continuity_pt f x <-> f @ x^' --> f x.
    Proof.
    by rewrite continuity_ptE continuous_withinNx. Qed.

    Lemma
    continuity_pt_dnbhs
    Source code
    f
    Source code
    x
    Source code
     :
      continuity_pt f x <->
      forall
    eps
    Source code
    , 0 < eps -> x^' (fun u => `|f x - f u| < eps).
    Proof.
    by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP.
    Qed.

    Lemma
    nbhs_pt_comp
    Source code
     (
    P
    Source code
     : R -> Prop) (
    f
    Source code
     : R -> R) (
    x
    Source code
     : R) :
      nbhs (f x) P -> continuity_pt f x -> \near
    x
    Source code
    , P (f x).
    Proof.
    by move=> Lf /continuity_pt_cvg; apply. Qed.

    End analysis_struct.

    Module
    RexpE
    Source code
    .
    Import normedtype sequences.

    Lemma
    RexpE
    Source code
     (
    x
    Source code
     : R) : Rtrigo_def.exp x = expR x.
    Proof.
    apply/esym; rewrite /exp /exist_exp; case: Alembert_C3 => y.
    rewrite /Pser /infinite_sum /= => exp_ub.
    rewrite /expR /exp_coeff /series/=; apply: (@cvg_lim R^o) => //.
    rewrite -cvg_shiftS /=; apply/cvgrPdist_lt => /= e /RltP /exp_ub[N Nexp_ub].
    near=> n.
    have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge.
    move: Nexp_ub => /(_ _ nN) /[!RdistE] /RltP /=.
    rewrite distrC sum_f_R0E; congr (`| _ - _ | < e).
    by apply: eq_bigr=> k _; rewrite RinvE RpowE mulrC factE INRE.
    Unshelve. all: by end_near. Qed.

    End RexpE.

    Definition
    RexpE

    RexpE : forall x : R, exp x = expR x RexpE is not universe polymorphic Arguments RexpE x%_R_scope RexpE is transparent Expands to: Constant mathcomp.analysis_stdlib.Rstruct_topology.RexpE Declared in library mathcomp.analysis_stdlib.Rstruct_topology, line 115, characters 11-16

    Source code
     := RexpE.RexpE.

    Lemma
    RlnE
    Source code
     (
    x
    Source code
     : R) : Rpower.ln x = exp.ln x.
    Proof.
    rewrite /Rpower.ln /Rln.
    have [xle0|xgt0] := leP x 0.
      by case: Rlt_dec => //= /[dup] /RltP + ?; rewrite exp.ln0// ltNge xle0.
    case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//].
    by case: ln_exists => y ->; rewrite RexpE exp.expRK.
    Qed.

    Module
    RtrigoE
    Source code
    .
    Import normedtype sequences trigonometry_functions.
    Local Open Scope classical_set_scope.

    Lemma
    RcosE
    Source code
     (
    x
    Source code
     : R) : Rtrigo_def.cos x = cos x.
    Proof.
    rewrite /Rtrigo_def.cos.
    case: exist_cos => y.
    rewrite /cos_in /cos_n /infinite_sum/=.
    set G : nat -> R^o := (G in sum_f_R0 G).
    move=> cos_ub.
    have /(@cvg_lim R^o) <- // : series G x @[
    x
    Source code
     --> \oo] --> y.
      rewrite -cvg_shiftS/=; apply/cvgrPdist_lt => /= e /RltP /cos_ub[N Ncos_ub].
      near=> n.
      have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge.
      move: Ncos_ub => /(_ _ nN) /[!RdistE] /RltP /=.
      by rewrite /G distrC sum_f_R0E.
    apply: (@cvg_lim R^o) => //.
    suff -> : G = cos_coeff' x by exact: cvg_cos_coeff'.
    apply/funext=> n; rewrite /G cos_coeff'E cos_coeffE.
    rewrite odd_double/= mul1r plusE addn0 addnn Rsqr_def !RealsE.
    by rewrite -expr2 -exprM mul2n doubleK.
    Unshelve. all: by end_near. Qed.

    Section PIE.

    Let
    pihalf_spec
    Source code
     (
    x
    Source code
     : R) := 0 <= x <= 2 /\ cos x = 0.

    Let
    pihalf_unique
    Source code
     (
    x
    Source code
    y
    Source code
     : R) : pihalf_spec x -> pihalf_spec y -> x = y.
    Proof.
    case=> /andP[] x0 x2 cosx0 [] /andP[] y0 y2 cosy0.
    apply: cos_inj.
    - rewrite in_itv/=; apply/andP; split => //.
      by rewrite (le_trans x2)// pi_ge2.
    - rewrite in_itv/=; apply/andP; split => //.
      by rewrite (le_trans y2)// pi_ge2.
    by rewrite cosx0 cosy0.
    Qed.

    Let
    PI2E
    Source code
     : PI2 = pi / 2.
    Proof.
    rewrite /PI2; case: PI_2_aux => x /= [] [] /RleP x78 /RleP x74.
    move/Ropp_eq_compat; rewrite Ropp_involutive Ropp_0 RealsE => cosx0.
    rewrite pihalfE.
    have x_pihalf : pihalf_spec x.
      split; [|by rewrite -RcosE].
      rewrite (le_trans _ x78)/= ?RealsE/=; [lra|].
      by rewrite (le_trans x74)// ?RealsE/=; lra.
    apply/esym/get_unique => //= y y_pihalf.
    exact: pihalf_unique.
    Qed.

    Lemma
    PIE
    Source code
     : PI = pi.
    Proof.
    by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed.

    End PIE.

    Lemma
    RsinE
    Source code
     (
    x
    Source code
     : R) : Rtrigo_def.sin x = sin x.
    Proof.
    by rewrite sin_cos RcosE PIE !RealsE/= addrC cosDpihalf opprK. Qed.

    End RtrigoE.

    Definition
    RcosE

    RcosE : forall x : R, Rtrigo_def.cos x = cos x RcosE is not universe polymorphic Arguments RcosE x%_R_scope RcosE is transparent Expands to: Constant mathcomp.analysis_stdlib.Rstruct_topology.RcosE Declared in library mathcomp.analysis_stdlib.Rstruct_topology, line 188, characters 11-16

    Source code
     := RtrigoE.RcosE.
    Definition
    Rtrigo_PIE

    Rtrigo_PIE : PI = pi Rtrigo_PIE is not universe polymorphic Rtrigo_PIE is transparent Expands to: Constant mathcomp.analysis_stdlib.Rstruct_topology.Rtrigo_PIE Declared in library mathcomp.analysis_stdlib.Rstruct_topology, line 189, characters 11-21

    Source code
     := RtrigoE.PIE.
    Definition
    RsinE

    RsinE : forall x : R, Rtrigo_def.sin x = sin x RsinE is not universe polymorphic Arguments RsinE x%_R_scope RsinE is transparent Expands to: Constant mathcomp.analysis_stdlib.Rstruct_topology.RsinE Declared in library mathcomp.analysis_stdlib.Rstruct_topology, line 190, characters 11-16

    Source code
     := RtrigoE.RsinE.

    Definition
    RealsE

    RealsE : (forall x y : R, (x + y)%R = (x + y)%R) * (forall x y : R, (x - y)%R = (x - y)%R) * (forall x y : R, (x * y)%R = (x * y)%R) * (forall x : R, (- x)%R = (- x)%R) * (forall x : R, (/ x)%R = x^-1%R) * (forall x y : R, (x / y)%R = (x / y)%R) * (forall n : nat, INR n = n%:R%R) * (0%R = 0%R) * (1%R = 1%R) * (forall p : positive, Pos.to_nat p = nat_of_pos p) * (forall p : positive, IZR (Z.pos p) = INR (nat_of_pos p)) * (forall x : R, sqrt x = Num.ExtraDef.sqrtr x) * (forall (x : R) (n : nat), (x ^ n)%R = (x ^+ n)%R) * (forall x y : R, Rmax x y = Num.max x y) * (forall x y : R, Rmin x y = Num.min x y) * (forall x : R, Rabs x = `|x|%R) * (forall x y : R, Rdist x y = `|x - y|%R) * (forall (f : nat -> R) (n : nat), sum_f_R0 f n = (\sum_(0 <= k < n.+1) f k)%R) * (forall n : nat, Factorial.fact n = n`!) RealsE is not universe polymorphic RealsE is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.RealsE Declared in library mathcomp.reals_stdlib.Rstruct, line 551, characters 11-17

    Source code
     := (RealsE, RexpE, RlnE, RcosE, Rtrigo_PIE, RsinE).
    Generated by rocqnavi