wip

Author: Tragicus

classical/unstable.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
-From mathcomp Require Import archimedean finset interval mathcomp_extra.
+From mathcomp Require Import archimedean finset interval complex mathcomp_extra.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -33,6 +33,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Theory.
+Local Open Scope complex_scope.
 Local Open Scope ring_scope.
 
 Section ssralg.
@@ -483,3 +484,131 @@ Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R
 
 Export -(notations) Morphisms.
 End ProperNotations.
+
+(* TODO: backport to real-closed *)
+Section complex_extras.
+Variable R : rcfType.
+Local Notation sqrtr := Num.sqrt.
+Local Notation C := R[i].
+
+Import Normc.
+Import Num.Def.
+Import complex.
+
+Lemma scalecE (w  v : C) : v *: w = v * w.
+Proof. by []. Qed.
+
+(* FIXME: unused *)
+Lemma normcr (x : R) : normc (x%:C) = normr x.
+Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed.
+
+Lemma Im_mul (x : R) : x *i = x%:C * 'i%C.
+Proof. by simpc. Qed.
+
+Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k).
+Proof.
+by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx.
+Qed.
+
+Lemma complexA (h : C) : h%:A = h.
+Proof. by rewrite scalecE mulr1. Qed.
+
+Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R.
+Proof. by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr normr_nat. Qed.
+
+Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k.
+Proof.
+by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul.
+Qed.
+
+Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C.
+Proof.
+case: r => x y /= /andP[] /eqP -> x0.
+by rewrite expr0n addr0 sqrtr_sqr gtr0_norm.
+Qed.
+
+Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C.
+Proof. by case: r => x y /andP[] /eqP -> _. Qed.
+
+Lemma ltc0E  (k : R): (0 < k%:C) = (0 < k).
+Proof. by simpc. Qed.
+
+Lemma ltc0P  (k : R): (0 < k%:C) <-> (0 < k).
+Proof. by simpc. Qed.
+
+Lemma ltcP  (k t: R): (t%:C < k%:C) <-> (t < k).
+Proof. by simpc. Qed.
+
+Lemma lecP  (k t: R): (t%:C <= k%:C) <-> (t <= k).
+Proof. by simpc. Qed.
+
+(* (*TBA algC *) *)
+Lemma realC_gt0 (d : C) : 0 < d -> (0 < Re d :> R).
+Proof. by rewrite ltcE => /andP [] //. Qed.
+
+Lemma Creal_gtE (c d : C) : c < d -> (complex.Re c < complex.Re d).
+Proof. by rewrite ltcE => /andP [] //. Qed.
+
+Lemma realC_norm (b : R) : `|b%:C| = `|b|%:C.
+Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed.
+
+Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s).
+Proof. exact: (inj_eq (@complexI _)). Qed.
+
+Lemma eqCI (r s : R) : (r *i == s *i) = (r == s).
+Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed.
+
+Lemma neqCr0 (r : R) : (r%:C != 0) = (r != 0).
+Proof. by apply/negP/negP; rewrite ?eqCr. Qed.
+
+Lemma real_normc_ler (x : C) :
+  `|Re x| <= normc x.
+Proof.
+case: x => x y /=.
+rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
+rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=.
+by rewrite lerDl ?sqr_ge0.
+Qed.
+
+Lemma im_normc_ler (x : C) :
+  `|Im x| <= normc x.
+Proof.
+case: x => x y /=.
+rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
+rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=.
+by rewrite lerDr ?sqr_ge0.
+Qed.
+
+End complex_extras.
+
+Notation  "f %:Rfun" :=
+  (f : (Rcomplex _) -> (Rcomplex _))
+  (at level 5,  format "f %:Rfun")  : complex_scope.
+
+Notation  "v %:Rc" :=   (v : (Rcomplex _))
+                          (at level 5, format "v %:Rc")  : complex_scope.
+
+Section algebraic_lemmas.
+Variable (R: rcfType).
+Notation C := R[i].
+Notation Rcomplex := (Rcomplex R).
+
+Import Normc.
+
+Lemma realCZ (a : R) (b : Rcomplex) : a%:C * b = a *: b.
+Proof. by case: b => x y; simpc. Qed.
+
+Lemma realC_alg (a : R) : a *: (1%:Rc) = a%:C.
+Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed.
+
+Lemma scalecr (w: C) (r : R) : r *: (w: Rcomplex) = r%:C *: w .
+Proof. by case w => a b; simpc. Qed.
+
+Lemma scalecV (h: R) (v: Rcomplex):
+  h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *)
+Proof.
+by move=> h0 v0; rewrite scalecr invrM // ?unitfE ?eqCr // mulrC scalecr fmorphV.
+Qed.
+
+End algebraic_lemmas.
+

theories/function_spaces.v

@@ -1557,6 +1557,40 @@ End cartesian_closed.
 
 End currying.
 
+Section big_continuous.
+
+Lemma cvg_big (T : Type) (U : topologicalType) [F : set_system T] [I : Type]
+    (r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U)
+    (op : U -> U -> U) (x0 : U):
+  Filter F ->
+  continuous (fun x : U * U => op x.1 x.2) ->
+  (forall i, P i -> Ff i x @[x --> F] --> Fa i) ->
+  \big[op/x0]_(i <- r | P i) (Ff i x) @[x --> F] -->
+    \big[op/x0]_(i <- r | P i) Fa i.
+Proof.
+move=> FF opC0 cvg_f.
+elim: r => [|x r IHr].
+  rewrite big_nil.
+  under eq_cvg do rewrite big_nil.
+  exact: cvg_cst.
+rewrite big_cons (eq_cvg _ _ (fun x => big_cons _ _ _ _ _ _)).
+case/boolP: (P x) => // Px.
+apply: (@cvg_comp _ _ _ (fun x1 => (Ff x x1, \big[op/x0]_(j <- r | P j) Ff j x1)) _ _ (nbhs (Fa x, \big[op/x0]_(j <- r | P j) Fa j)) _ _ (continuous_curry_cvg opC0)).
+by apply: cvg_pair => //; apply: cvg_f.
+Qed.
+
+Lemma continuous_big [K T : topologicalType] [I : Type] (r : seq I)
+    (P : pred I) (F : I -> T -> K) (op : K -> K -> K) (x0 : K) :
+  continuous (fun x : K * K => op x.1 x.2) ->
+  (forall i, P i -> continuous (F i)) ->
+  continuous (fun x => \big[op/x0]_(i <- r | P i) F i x).
+Proof.
+move=> op_cont f_cont x.
+by apply: cvg_big => // i /f_cont; apply.
+Qed.
+
+End big_continuous.
+
 Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
   uncurry (id : continuousType X Y -> (X -> Y)).