Holomorphy

.travis.yml

@@ -0,0 +1,31 @@
+language: generic
+os: linux
+
+branches:
+  only:
+  - master
+
+services:
+- docker
+
+env:
+  global:
+  - NJOBS="2"
+  - CONTRIB="analysis"
+  - OPAMYES=yes
+  jobs:
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.10"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.12"
+
+install:
+- docker pull ${DOCKERIMAGE}
+- docker tag  ${DOCKERIMAGE} ci:current
+- docker run  --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current
+- docker exec CI /bin/bash --login -c "opam repo add coq-released https://coq.inria.fr/opam/released"
+- docker exec CI /bin/bash --login -c "opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev"
+# - docker exec CI /bin/bash --login -c "opam pin add -y -n coq-mathcomp-${CONTRIB} ."
+- docker exec CI /bin/bash --login -c "opam install --deps-only ."
+
+script:
+- docker exec CI /bin/bash --login -c "opam install -vvv ."

CHANGELOG_UNRELEASED.md

@@ -52,6 +52,51 @@
 - in `lebesgue_integral_differentiation.v`:
   + lemma `nicely_shrinking_fin_num`
 
+- in `unstable.v`
+  + lemmas `scalecE`, `normcr`, `Im_mul`, `mulrnc`, `complexA`, `normc_natmul`,
+    `nomrc_mulrn`, `gt0_normc`, `gt0_realC`, `ltc0E`, `ltc0P`, `ltcP`, `lecP`,
+    `realC_gt0`, `Creal_gtE`, `realC_norm`, `eqCr`, `eqCI`, `neqCr0`,
+    `real_normc_ler`, `im_normc_ler`
+  + notations `f %:Rfun`, `v %:Rc`
+  + lemmas `realCZ`, `realC_alg`, `scalecr`, `scalecV`
+
+- in `function_spaces.v`
+  + lemmas `cvg_big`, `continuous_big`
+
+- file `holomorphy.v`
+  + instance of `normedModType` on `complex`
+  + definition `ball_Rcomplex`
+  + lemmas `entourage_RcomplexE`, `normcZ`, `Rcomplex_findim`
+  + instance of `normedVectType` on `complex`
+  + definitions `holomorphic`, `Rdifferentiable`, `realC`, `CauchyRiemannEq`
+  + lemmas `holomorphicP`, `continuous_realC`, `Rdiff1`, `Rdiffi`, `littleoCo`,
+    `holo_differentiable`, `holo_CauchyRiemann`, `Diff_CR_holo`,
+    `holomorphic_Rdiff`
+
+- in `landau.v`
+  + lemma `littleoE0`
+
+- in `normed_module.v`
+  + structure `normedVectType`
+  + lemmas `dnbhs0_le`, `nbhs0_le`, `dnbrg0_lt`, `nbhs0_lt`
+  + definition `pseudometric`
+  + instance of `normedZmodType`, `pointedType` and `pseudoMetricType`
+    on `pseudometric`
+  + definitions `oo_norm`, `oo_space`,
+  + instance of `normedModType` on `oo_space`
+  + lemmas `oo_closed_ball_compact`, `equivalence_norms`,
+    `linear_findim_continuous`
+
+- in `num_topology.v`
+  + instance of `pseudoMetricType` on `GRing.regular`
+
+- in `uniform_structure`
+  + lemma `within_continuous_withinNx`
+
+- in `tvs.v`
+  + lemmas `cvg_sum`, `sum_continuous`, `entourage_nbhsE`
+  + instance of `UniformZmodule.type` on `GRing.regular`
+
 ### Changed
 
 - in `convex.v`:

_CoqProject

@@ -97,6 +97,7 @@ theories/forms.v
 theories/derive.v
 theories/measure.v
 theories/numfun.v
+theories/holomorphy.v
 
 theories/lebesgue_integral_theory/simple_functions.v
 theories/lebesgue_integral_theory/lebesgue_integral_definition.v

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.
+

config.nix

@@ -0,0 +1,6 @@
+{
+  coq = "8.11";
+  mathcomp = "mathcomp-1.12.0";
+  mathcomp-real-closed = "mkerjean/master";
+  mathcomp-finmap = "1.5.1";
+}

opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://github.com/math-comp/analysis"
+bug-reports: "https://github.com/math-comp/analysis/issues"
+dev-repo: "git+https://github.com/math-comp/analysis.git"
+license: "CECILL-C"
+authors: [
+  "Reynald Affeldt"
+  "Cyril Cohen"
+  "Assia Mahboubi"
+  "Damien Rouhling"
+  "Pierre-Yves Strub"
+]
+build: [
+  [make "INSTMODE=global" "config"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "coq" { ((>= "8.10" & < "8.13~") | = "dev") }
+  "coq-mathcomp-field"       {(>= "1.11.0" & < "1.12~")}
+  "coq-mathcomp-finmap"      {(>= "1.5.0" & < "1.6~")}
+  "coq-mathcomp-real-closed"          {(>= "1.0.5" & < "1.1~")}
+]
+synopsis: "An analysis library for mathematical components"
+description: """
+This repository contains an experimental library for real analysis for
+the Coq proof-assistant and using the Mathematical Components library.
+
+It is inspired by the Coquelicot library.
+"""
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword: analysis"
+  "keyword: topology"
+  "keyword: real numbers"
+  "logpath: mathcomp.analysis"
+  "date:2020-08-11"
+]

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)).