Holomorphy

.nix/config.nix

@@ -57,13 +57,15 @@ in {
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";
+      mathcomp-real-closed.override.version = "master";
       micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.0";
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";
+      mathcomp-real-closed.override.version = "master";
       ssprove.job = false;  # not yet available for 9.1
     };
   };
@@ -85,13 +87,15 @@ in {
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";
+      mathcomp-real-closed.override.version = "master";
       micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.1";
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";
+      mathcomp-real-closed.override.version = "master";
       ssprove.job = false;  # not yet available for 9.1
     };
   };
@@ -106,6 +110,7 @@ in {
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";
+      mathcomp-real-closed.override.version = "master";
       micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
@@ -116,6 +121,7 @@ in {
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";
+      mathcomp-real-closed.override.version = "master";
       ssprove.job = false;
       mathcomp-infotheo.job = false;
     };

.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

@@ -131,6 +131,51 @@
 - in `lebesgue_stieltjes_measure.v`:
   + definition `lebesgue_display`
 
+- 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
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

_CoqProject

@@ -97,6 +97,7 @@ theories/trigo.v
 theories/esum.v
 theories/derive.v
 theories/numfun.v
+theories/holomorphy.v
 
 theories/measure_theory/measurable_structure.v
 theories/measure_theory/measure_function.v

classical/unstable.v

@@ -1,7 +1,7 @@
-(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *) 
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
-From mathcomp Require Import vector archimedean interval.
+From mathcomp Require Import vector archimedean interval complex.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -45,6 +45,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 IntervalNumDomain.
@@ -653,3 +654,138 @@ End Theory.
 Module Import Exports. HB.reexport. End Exports.
 End Norm.
 Export Norm.Exports.
+
+
+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.
+
+
+(* TODO: backport to real-closed *)
+Section complex_extras.
+Variable R : rcfType.
+Local Notation sqrtr := Num.sqrt. 
+Local Notation C := (Rcomplex R).
+
+Import Normc.
+Import Num.Def.
+Import complex.
+
+(*TODO : rename scale regular and put there*)
+Lemma scalecE (w v: C^o) : v *: w = v * w.
+Proof. by []. Qed.
+
+Lemma scalerc (h : R) (c : C) : h *: (c : Rcomplex R) = h%:C * c.
+Proof.
+case : c => x y.
+by rewrite /(real_complex _) /(_ *: _) /( _ * _) /= /= /scalec !mul0r subr0 addr0.
+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^o) : 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.
+
+Lemma realC_alg (a : R) : a *: (1%:RC) = a%:C.
+Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed.
+
+Lemma scalecV (h: R) (v: Rcomplex R):
+  h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *)
+Proof.
+by move=> h0 v0; rewrite scalerc invrM // ?unitfE ?eqCr // mulrC  scalerc fmorphV.
+Qed.
+
+
+(* TODO: clean lemmas about scalec *)
+Lemma scalerc_regular (h : R) (c : R[i]): h *: (c : Rcomplex R) = h%:C *: (c : C^o).
+Proof.
+by rewrite scalecE scalerc.
+Qed.
+
+Lemma scalec1 (h : R) : h *: (1 : C^o) = h%:C.
+Proof.
+by rewrite scalerc mulr1.
+Qed.
+
+
+End complex_extras.
+

config.nix

@@ -0,0 +1,6 @@
+{
+  coq = "9.1";
+  mathcomp = "master";
+  mathcomp-real-closed = "2.0.3";
+  mathcomp-finmap = "2.2.3";
+}

opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "reynald.affeldt@aist.go.jp"
+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/derive.v

@@ -537,6 +537,7 @@ rewrite invrK -ltr_pdivlMr // ger0_norm // ltr_pdivrMr //.
 by rewrite divfK ?lt0r_neq0// [ltRHS]splitr ltrDl.
 Qed.
 
+
 Lemma diff_unique (V W : normedModType R) (f : V -> W)
   (df : {linear V -> W}) x :
   continuous df -> f \o shift x = cst (f x) + df +o_ 0 id ->
@@ -565,6 +566,29 @@ rewrite [in LHS]littleo_center0 (comp_centerK x id).
 by rewrite -[- _ in RHS](comp_centerK x).
 Qed.
 
+Lemma shift_addo (V W : normedModType R) (f l : V -> W) x :
+ (forall t, f t = f x + l (t - x) +o_(t \near x) (t - x))
+  <-> (forall h, f (h + x) = f x + l h +o_(h \near 0) h).
+Proof.
+split=> [fE t|fE t].
+  rewrite fE addrK; congr (_ + _).
+  by rewrite littleo_center0/= addrK; congr the_littleo;
+    apply/funext => ?/=; rewrite addrK.
+rewrite -[in LHS](@subrK _ x t) fE; congr (_ + _).
+by rewrite [in RHS]littleo_center0/=; congr the_littleo;
+   apply/funext => ?/=; rewrite addrK.
+Qed.
+
+Lemma exists_diff (V W : normedModType R) (f : V -> W) x :
+ (exists2 l : {linear V -> W},
+   continuous l & (forall t, f t = f x + l (t - x) +o_(t \near x) (t - x))) ->
+  differentiable f x.
+Proof.
+move=> [l cl hl].
+have fxl : 'd f x = l :> (V -> W) by exact/(diff_unique cl)/funext/shift_addo.
+by apply/diffP => //=; split; rewrite fxl => // t; rewrite norm_lim_id.
+Qed.
+
 Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0.
 Proof. by apply/diff_unique; have [] := dcst a x. Qed.