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.

..copy R R^o.
..copy R R^o.

Lemma ( : R -> R) :
continuity_pt f x <->
forall : {posnum R}, nbhs x (fun => `|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 ( : R -> R) ( : 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 ( : R -> R) ( : R) :
continuity_pt f x <-> {for x, continuous f}.

Proof.

exact: continuity_pt_cvg. Qed.

Local Open Scope classical_set_scope.

Lemma :
continuity_pt f x <-> f @ x^' --> f x.

Proof.

by rewrite continuity_ptE continuous_withinNx. Qed.

Lemma :
continuity_pt f x <->
forall , 0 < eps -> x^' (fun u => `|f x - f u| < eps).

Proof.

by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP.
Qed.

Lemma ( : R -> Prop) ( : R -> R) ( : R) :
nbhs (f x) P -> continuity_pt f x -> \near , P (f x).

Proof.

by move=> Lf /continuity_pt_cvg; apply. Qed.

End analysis_struct.

Module .
Import normedtype sequences.

Lemma ( : 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.

Lemma ( : 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 .
Import normedtype sequences trigonometry_functions.
Local Open Scope classical_set_scope.

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

Let ( : 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 : 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 : PI = pi.

Proof.

by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed.

End PIE.

Lemma ( : R) : Rtrigo_def.sin x = sin x.

Proof.

by rewrite sin_cos RcosE PIE !RealsE/= addrC cosDpihalf opprK. Qed.

End RtrigoE.

Definition := RtrigoE.RcosE.
Definition := RtrigoE.PIE.
Definition := RtrigoE.RsinE.

Definition := (RealsE, RexpE, RlnE, RcosE, Rtrigo_PIE, RsinE).

Files

Module mathcomp.analysis_stdlib.Rstruct_topology