Files

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.

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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code PseudoMetricSource code.copy R R^o.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code PointedSource code.copy R R^o.

Lemma continuity_pt_nbhsSource code (fSource code : R -> R) xSource code :
  continuity_pt f x <->
  forall epsSource code : {posnum R}, nbhs x (fun uSource 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_cvgSource code (fSource code : R -> R) (xSource 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_ptESource code (fSource code : R -> R) (xSource 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 fSource code xSource code :
  continuity_pt f x <-> f @ x^' --> f x.
Proof.
by rewrite continuity_ptE continuous_withinNx. Qed.

Lemma continuity_pt_dnbhsSource code fSource code xSource code :
  continuity_pt f x <->
  forall epsSource 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_compSource code (PSource code : R -> Prop) (fSource code : R -> R) (xSource code : R) :
  nbhs (f x) P -> continuity_pt f x -> \forall x0Source code \near x, P (f x0).
Proof.
by move=> Lf /continuity_pt_cvg; apply. Qed.

End analysis_struct.

Module RexpESource code.
Import normedtype sequences.

Lemma RexpESource code (xSource 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 114, characters 11-16

Source code := RexpE.RexpE.

Lemma RlnESource code (xSource 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 RtrigoESource code.
Import normedtype sequences trigonometry_functions.
Local Open Scope classical_set_scope.

Lemma RcosESource code (xSource 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 @[xSource 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_specSource code (xSource code : R) := 0 <= x <= 2 /\ cos x = 0.

Let pihalf_uniqueSource code (xSource code ySource 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 PI2ESource 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 PIESource code : PI = pi.
Proof.
by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed.

End PIE.

Lemma RsinESource code (xSource 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 187, 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 188, 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 189, characters 11-16

Source code := RtrigoE.RsinE.

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