From e96f7949325aea150d8ed569e63290410ab226ad Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:15:45 +0900 Subject: [PATCH 01/29] fix --- classical/unstable.v | 132 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 130 insertions(+), 2 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index cf8b4ce04a..107babe42d 100644 --- a/classical/unstable.v +++ b/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,130 @@ End Theory. Module Import Exports. HB.reexport. End Exports. End Norm. Export Norm.Exports. + +(* 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. + +Lemma scalecE (w v: C^o) : 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^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. + +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. From 72c1c3074039c690b3ca91000bb25e8435985b81 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:22:44 +0900 Subject: [PATCH 02/29] fix --- theories/normedtype_theory/tvs.v | 36 +++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 41126a781d..35062f5eb7 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -20,7 +20,6 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* PreTopologicalNmodule == HB class, join of Topological and Nmodule *) (* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) (* continuous addition *) -(* PreTopologicalZmodule == HB class, join of Topological and Zmodule *) (* topologicalZmodType == topological abelian group *) (* TopologicalZmodule == HB class, join of TopologicalNmodule and *) (* Zmodule with a continuous opposite operator *) @@ -344,6 +343,27 @@ exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). Qed. +Lemma entourage_nbhsE : @entourage M = filter_from (nbhs 0) (fun X => [set x | x.2 - x.1 \in X]). +Proof. +have map_uniform (T U : uniformType) (S : set (U * U)%type) (f : T * T -> U) : unif_continuous f -> entourage S -> exists ST : set (T * T)%type, entourage ST /\ {in ST, forall x, forall y, (f (x.1, y), f (x.2, y)) \in S}. + move=> fu /fu [[]]/= ST1 ST2 [] ? ? /subsetP STf. + exists ST1; split=> // x xST1 y. + have /STf: (x, (y, y)) \in ST1 `*` ST2. + rewrite in_setX xST1/= unfold_in/=. + apply/asboolT. + exact: entourage_refl. + rewrite in_setE/= => -[] [] [] a1 a2 [] b1 b2 /= abS [] <- {2}<- <-/=. + exact: asboolT. +rewrite eqEsubset; split; apply/subsetP => U; rewrite !inE /filter_from/=. + move=> /(map_uniform _ _ _ _ sub_unif_continuous)/= [] V [] Ve VU. + exists (xsection V 0); first exact: nbhs_entourage. + apply/subsetP => [] [] x y; rewrite inE/= mem_xsection => /VU/(_ (-x))/=. + by rewrite opprK -addrA addNr add0r addr0. +move=> [] V /nbhsP[] U' /(map_uniform _ _ _ _ add_unif_continuous)/= [] W [] We WU' /subsetP U'V /subsetP VU. +apply/(filterS _ We)/subsetP => -[] a b /WU'/=/(_ (-a)); rewrite subrr => abU'. +by apply/VU; rewrite inE/=; apply: U'V; rewrite mem_xsection. +Qed. + End UniformZmoduleTheory. HB.structure Definition PreUniformLmodule (K : numDomainType) := @@ -708,6 +728,19 @@ Qed. Let standard_locally_convex_set : exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B. +(*======= +Local Lemma standard_sub_unif_continuous : unif_continuous (fun x : R^o * R^o => x.1 - x.2). +Proof. +move=> /= U; rewrite /nbhs/= -!entourage_ballE => -[]/= e e0 /subsetP eU. +exists (e / 2) => /=; first exact: divr_gt0. +apply/subsetP => -[] [] a1 a2 [] b1 b2/=; rewrite inE/= => -[]/=. +rewrite /ball/= => abe1 abe2. +apply: eU => /=; rewrite inE/= /ball/= opprD addrACA -opprD. +by rewrite (le_lt_trans (ler_normB _ _))// (splitr e) ltrD. +Qed. + +Local Lemma standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2). +>>>>>>> 50b14da8 (holomorphic):theories/tvs.v*) Proof. exists [set B | exists x r, B = ball x r]. by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set. @@ -718,6 +751,7 @@ Qed. HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. +(*HB.instance Definition _ := PreUniformNmodule_isUniformZmodule.Build R^o standard_sub_unif_continuous.*) HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous. HB.instance Definition _ := From 3bb751ae2ff2769e2c6309aedb3c04af8983cbaa Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 May 2025 21:09:27 +0900 Subject: [PATCH 03/29] holomorphic Co-Authored-By : Reynald Affeldt Co-Authored-By : Cyril Cohen Co-Authored-By : Quentin Vermande --- .travis.yml | 31 +++ CHANGELOG_UNRELEASED.md | 45 +++ _CoqProject | 1 + config.nix | 6 + opam | 41 +++ theories/holomorphy.v | 272 +++++++++++++++++++ theories/normedtype_theory/normed_module.v | 30 ++ theories/topology_theory/num_topology.v | 4 + theories/topology_theory/uniform_structure.v | 3 + 9 files changed, 433 insertions(+) create mode 100644 .travis.yml create mode 100644 config.nix create mode 100644 opam create mode 100644 theories/holomorphy.v diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 0000000000..6df16b626c --- /dev/null +++ b/.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 ." diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0023dbb5e0..beeaa11c6c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`: diff --git a/_CoqProject b/_CoqProject index f0b745c7f6..7cb8c5bda7 100644 --- a/_CoqProject +++ b/_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 diff --git a/config.nix b/config.nix new file mode 100644 index 0000000000..87c4d6070e --- /dev/null +++ b/config.nix @@ -0,0 +1,6 @@ +{ + coq = "8.11"; + mathcomp = "mathcomp-1.12.0"; + mathcomp-real-closed = "mkerjean/master"; + mathcomp-finmap = "1.5.1"; +} diff --git a/opam b/opam new file mode 100644 index 0000000000..e9bd5838b0 --- /dev/null +++ b/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" +] diff --git a/theories/holomorphy.v b/theories/holomorphy.v new file mode 100644 index 0000000000..e9263dd257 --- /dev/null +++ b/theories/holomorphy.v @@ -0,0 +1,272 @@ + +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(*Require Import ssrsearch.*) +From HB Require Import structures. +From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. +From mathcomp Require Import ssrnat eqtype seq choice fintype bigop order. +From mathcomp Require Import ssralg ssrnum ssrfun matrix complex. +From mathcomp Require Import unstable boolp reals ereal derive. +From mathcomp Require Import classical_sets functions interval_inference. +From mathcomp Require Import topology normedtype landau. + +(**md**************************************************************************) +(* # Holomorphic functions *) +(* *) +(* This file develops the theory of holomorphic functions. We endow complex *) +(* (denoted C below) and Rcomplex with structures of normedModType. We prove *) +(* that the holomorphic functions are the R-differentiable functions from C *) +(* to C satisfying the Cauchy-Riemann equation. *) +(* *) +(* holomorphic f == f is holomorphic, i.e. C-derivable *) +(* Rdifferentiable f == f is differentiable on Rcomplex *) +(* CauchyRiemannEq f c == The Cauchy-Riemman equation for f at point c *) +(* *) +(******************************************************************************) + +Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def complex. +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. +Local Open Scope complex_scope. +Import numFieldNormedType.Exports. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +HB.instance Definition _ (R : rcfType) := NormedModule.copy R[i] R[i]^o. +HB.instance Definition _ (R : rcfType) := UniformZmodule.copy R[i] R[i]^o. + +HB.instance Definition _ (R : rcfType) := UniformZmodule.copy (Rcomplex R) R[i]. +HB.instance Definition _ (R : rcfType) := Pointed.copy (Rcomplex R) R[i]. + +Module Rcomplex_NormedModType. +Section Rcomplex_NormedModType. +Variable (R : rcfType). + +Definition ball_Rcomplex : Rcomplex R -> R -> Rcomplex R -> Prop := + ball_ Num.norm. + +Lemma entourage_RcomplexE : entourage = entourage_ ball_Rcomplex. +Proof. +rewrite entourage_nbhsE/= eqEsubset. +split; apply/subsetP => U; rewrite inE => -[]. + move=> V []/= e; rewrite ltcE => /andP[]/eqP/= ei0 e0. + have ->: e = (Re e)%:C by case: e ei0 {e0} => r i/= ->. + move=> /subsetP eV /subsetP VU. + rewrite inE; exists (Re e) => //. + apply/subsetP => -[] a b; rewrite inE/= /ball/= => abe. + by apply: VU; rewrite inE/=; apply: eV; rewrite inE/= add0r opprB ltcR. +move=> e/= e0 /subsetP eU. +rewrite inE; exists (ball_Rcomplex 0 e). + exists e%:C; first by rewrite /= ltcR. + by apply/subsetP => x; rewrite !inE/= ltcR. +apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe. +by apply: eU; rewrite inE. +Qed. + +HB.instance Definition _ := Uniform_isPseudoMetric.Build R (Rcomplex R) + ball_norm_center ball_norm_symmetric ball_norm_triangle entourage_RcomplexE. +HB.instance Definition _ := + NormedZmod_PseudoMetric_eq.Build R (Rcomplex R) erefl. + +Lemma normcZ (l : R) (x : Rcomplex R) : `|l *: x| = `|l| * `|x|. +Proof. +by case: x => ??; rewrite /normr/= !exprMn -mulrDr sqrtrM ?sqr_ge0// sqrtr_sqr. +Qed. + +HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. + +Lemma Rcomplex_findim : Vector.axiom 2 (Rcomplex R). +Proof. +exists (fun x => \row_(i < 2) [:: Re x; Im x]`_i). + move=> r x y; apply/rowP; move=> i /=; rewrite !mxE. + case: i => i /=; rewrite ltnS leq_eqVlt => /orP[/eqP ->/=|]. + by rewrite raddfD/= linearZ. + by rewrite ltnS leqn0 => /eqP -> /=; rewrite raddfD/= linearZ. +apply: (@Bijective _ _ _ (fun x : 'rV_2 => x ord0 ord0 +i* x ord0 ord_max)). + by case=> x y; rewrite !mxE. +move=> x; apply/rowP => i; rewrite mxE/=. +case: i => i /[dup] + ilt; rewrite ltnS leq_eqVlt => /orP[/eqP /= i1|]. + by rewrite {1}i1/=; congr (x ord0); apply: val_inj. +rewrite ltnS leqn0 => /eqP i0/=. +by rewrite {1}i0/=; congr (x ord0); apply: val_inj. +Qed. + +HB.instance Definition _ := + Lmodule_hasFinDim.Build R (Rcomplex R) Rcomplex_findim. + +End Rcomplex_NormedModType. +End Rcomplex_NormedModType. + +Section Holomorphe_der. +Variable R : realType. + +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. +Local Notation Rc := (Rcomplex R). + +Definition holomorphic (f : C -> C) (c : C) := + cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ 0^'). + +Lemma holomorphicP (f : C -> C) (c : C) : holomorphic f c <-> derivable f c 1. +Proof. +rewrite /holomorphic /derivable. +suff ->: (fun h : C => h^-1 *: ((f (c + h) - f c))) = + ((fun h : C => h^-1 *: ((f \o shift c) (h *: 1) - f c))) by []. +by apply: funext => h; rewrite complexA [X in f X]addrC. +Qed. + +Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:Rc. + +Definition realC : R -> C := (fun r => r%:C). + +Lemma continuous_realC: continuous realC. +Proof. +move=> x A /= [] r /[dup] /realC_gt0 Rer0 /gt0_realC rRe H; exists (Re r) => //. +by move=> z /= nz; apply: (H z%:C); rewrite /= -raddfB realC_norm rRe ltcR. +Qed. + +Lemma Rdiff1 (f : C -> C) c : + lim ((fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ 0^')) + = 'D_1 (f%:Rfun) c%:Rc. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : C => h^-1 *: ((f (c + h) - f c))) + \o realC @ 0^')). +suff ->: (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC + = fun h : R => h^-1 *: ((f \o shift c) (h *: (1%:Rc)) - f c)%:Rc. + by []. +apply: funext => h /=. +by rewrite -fmorphV /= -!scalecr realC_alg [X in f X]addrC. +Qed. + +Lemma Rdiffi (f : C -> C) c: + lim ((fun h : C => h^-1 *: ((f (c + h * 'i) - f c))) @ (realC @ 0^')) + = 'D_('i) (f%:Rfun) c%:Rc. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) + \o realC @ 0^')). +suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC + = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:Rc)) - f c)%:Rc. + by []. +apply: funext => h /=. +by rewrite -fmorphV -scalecE -!scalecr realCZ [X in f X]addrC. +Qed. + +(* should be generalized to equivalent norms *) +(* but there is no way to state it for now *) +Lemma littleoCo (h e : C -> C) (x : C) : + [o_x (e : C -> C) of (h : C -> C)] = + [o_x (e : Rc -> Rc) of (h : Rc -> Rc)]. +Proof. +suff heP : (h : C -> C) =o_x (e : C -> C) <-> + (h : Rc -> Rc) =o_x (e : Rc -> Rc). + have [ho|hNo] := asboolP ((h : C -> C) =o_x (e : C -> C)). + by rewrite !littleoE// -!eqoP// -heP. + by rewrite !littleoE0// -!eqoP// -heP. +rewrite !eqoP; split => small/= _ /posnumP[eps]; near=> y. + rewrite -lecR/= rmorphM/=. + near: y. + by apply: small; rewrite ltcR. +rewrite -[_%:num]ger0_norm// -rmorphM/= lecR. +by near: y; apply: small; rewrite (@normr_gt0 _ (Rcomplex R))//. +Unshelve. all: by end_near. Qed. + +Definition CauchyRiemannEq (f : C -> C) c := + 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. + +Lemma holo_differentiable (f : C -> C) (c : C) : + holomorphic f c -> Rdifferentiable f c. +Proof. +move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. +pose df : Rc -> Rc := 'd f c. +have lDf : linear df by move=> t u v; rewrite /df !scalecr linearP. +pose df' : {linear Rc -> Rc} := + HB.pack df (GRing.isLinear.Build _ _ _ _ df lDf). +apply/diff_locallyP; split; first exact: linear_findim_continuous. +have eqdf : f%:Rfun \o +%R^~ c = cst (f c) + df' +o_ (0 : Rc) id. + rewrite [LHS]holo /df'/=/df/=. + congr (_ + _). + exact: littleoCo. +rewrite (@diff_unique R (Rcomplex R) (Rcomplex R) _ df' _ _ eqdf). + exact: eqdf. +exact: linear_findim_continuous. +(* TODO: fix Qed performance issue (which is due to the proof of `eqdf`). + 3.684s *) +Qed. + +Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. +Proof. +move=> /cvg_ex; rewrite //= /CauchyRiemannEq. rewrite -Rdiff1 -Rdiffi. +set quotC : C -> C := fun h : R[i] => h^-1 *: (f (c + h) - f c). +set quotR : C -> C:= fun h => h^-1 *: (f (c + h * 'i) - f c) . +move => /= [l H]. +have -> : quotR @ (realC @ 0^') = (quotR \o realC) @ 0^' by []. +have realC'0: realC @ 0^' --> 0^'. + rewrite -[0 in X in _ --> X]/(realC 0). + apply: within_continuous_withinNx; first by apply: continuous_realC. + by move => /= x /complexI. +have HR0:(quotC \o (realC) @ 0^') --> l. + by apply: cvg_comp; last by exact: H. +have lem : quotC \o *%R^~ 'i%R @ (realC @ (0 : R)^') --> l. + apply: cvg_comp; last by exact: H. + apply: (@cvg_comp _ _ _ realC ( *%R^~ 'i)); first by exact: realC'0. + rewrite -[0 in X in _ `=>` X](mul0r 'i%C). + apply: within_continuous_withinNx; first exact: scalel_continuous. + move=> x /eqP; rewrite mul0r mulIr_eq0; last by apply/rregP; apply: neq0Ci. + exact: eqP. +have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) . + by apply/cvg_ex; simpl; exists l. +have ->: lim (quotR @ (realC @ ((0 : R)^'))) + = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ ((0 : R)^'))). + have: 'i \*:quotC \o ( fun h => h *'i) =1 quotR. + move=> h /=; rewrite /quotC /quotR /=. + rewrite invfM scalerA mulrC -mulrA mulVf ?mulr1 ?neq0Ci //. + by move=> /funext <-; rewrite limZr. +rewrite scalecE. +suff ->: lim (quotC @ (realC @ ((0 : R)^'))) + = lim (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) by []. +suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = l. + by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_lim _ lem). +by apply: cvg_lim; last exact: HR0. +Qed. + +Lemma Diff_CR_holo (f : C -> C) (c : C): + (Rdifferentiable f c) /\ (CauchyRiemannEq f c) -> (holomorphic f c). +Proof. +move=> [] /= /[dup] H /diff_locallyP => [[derc diff]] CR. +apply/holomorphicP/derivable1_diffP/diff_locallyP. +pose Df := (fun h : C => h *: ('D_1 f%:Rfun c : C)). +have lDf : linear Df by move=> t u v /=; rewrite /Df scalerDl scalerA scalecE. +pose df : {linear R[i] -> R[i]} := + HB.pack Df (GRing.isLinear.Build _ _ _ _ Df lDf). +have cdf : continuous df by apply: scalel_continuous. +have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *) + apply: funext => z; rewrite /Df. + set x := Re z; set y := Im z. + have zeq : z = x *: 1 %:Rc + y *: 'i%:Rc. + by rewrite [LHS]complexE /= realC_alg scalecr scalecE [in RHS]mulrC. + rewrite [X in 'd _ _ X]zeq addrC linearP linearZ /= -!deriveE //. + rewrite -CR (scalerAl y) -scalecE !scalecr /=. + rewrite -(scalerDl (('D_1 f%:Rfun (c : Rc)) : C) _ (real_complex R x)). + by rewrite addrC -!scalecr -realC_alg -zeq. +have holo: f \o shift c = cst (f c) + df +o_ ( 0 : C) id. + rewrite [LHS]diff /= lem. + congr (_ + _). + exact/esym/littleoCo. +by rewrite (diff_unique cdf holo). +(* TODO: fix Qed performance issue (which is due to the proof of `holo`). + 6.519s *) +Qed. + +Lemma holomorphic_Rdiff (f : C -> C) (c : C) : + (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c). +Proof. +split=> H; first exact: Diff_CR_holo. +split; first exact: holo_differentiable. +exact: holo_CauchyRiemann. +Qed. + +End Holomorphe_der. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 31c99d1a4f..ebfcbc9a09 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -508,6 +508,36 @@ Proof. by move=> k; apply: (cvg_comp2 cvg_id (cvg_cst _) (scale_continuous _ _ (_, _))). Qed. +Lemma dnbhs0_le e : + 0 < e -> \forall x \near (0 : V)^', `|x| <= e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +rewrite -ball_normE /= sub0r normrN => le_nxe _ . +by rewrite ltW. +Qed. + +Lemma nbhs0_le e : + 0 < e -> \forall x \near (0 : V)^', `|x| <= e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +rewrite -ball_normE /= sub0r normrN => le_nxe _ . +by rewrite ltW. +Qed. + +Lemma dnbhs0_lt e : + 0 < e -> \forall x \near (0 : V)^', `|x| < e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +by rewrite -ball_normE /= sub0r normrN. +Qed. + +Lemma nbhs0_lt e : + 0 < e -> \forall x \near (0 : V)^', `|x| < e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +by rewrite -ball_normE /= sub0r normrN. +Qed. + End NormedModule_numFieldType. Arguments cvg_at_rightE {K V} f x. Arguments cvg_at_leftE {K V} f x. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index fc7caea215..e1d281316b 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -82,6 +82,10 @@ HB.instance Definition _ (R : numFieldType) := Uniform_isPseudoMetric.Build R R^o ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. +HB.instance Definition _ (R : numFieldType) := + Uniform_isPseudoMetric.Build R R^o + ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. + Lemma real_order_nbhsE (R : realFieldType) (x : R^o) : nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]). Proof. diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index 44e5ce8742..d42004181c 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -286,6 +286,9 @@ by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. Unshelve. all: by end_near. Qed. Lemma continuous_injective_withinNx +(*======= +Lemma within_continuous_withinNx +>>>>>>> 50b14da8 (holomorphic) *) (T U : topologicalType) (f : T -> U) (x : T) : {for x, continuous f} -> (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'. From e5aea67906af918fa8aa5ab3c23410f934fb8d2b Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:48:37 +0900 Subject: [PATCH 04/29] add isnormedmodule section --- theories/normedtype_theory/normed_module.v | 50 ++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index ebfcbc9a09..7f34a7d70b 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2598,6 +2598,56 @@ Proof. by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed. End open_set_disjoint_real_intervals. +(* equip a normedZmodType with a structure of normed module *) + +Definition pseudometric (K : numFieldType) (M : normedZmodType K) : Type := M. + +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := + Choice.on (pseudometric M). +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := + Num.NormedZmodule.on (pseudometric M). +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := + isPointed.Build M 0. + +Section isnormedmodule. +Variables (K : numFieldType) (M' : normedZmodType K). + +Notation M := (pseudometric M'). + +Local Definition ball (x : M) (r : K) : set M := ball_ Num.norm x r. + +Local Definition ent : set_system (M * M) := + entourage_ ball. + +Local Definition nbhs (x : M) : set_system M := + nbhs_ ent x. + +Local Lemma nbhsE : nbhs = nbhs_ ent. Proof. by []. Qed. + +HB.instance Definition _ := hasNbhs.Build M nbhs. + +Local Lemma ball_center x (e : K) : 0 < e -> ball x e x. +Proof. by rewrite /ball/= subrr normr0. Qed. + +Local Lemma ball_sym x y (e : K) : ball x e y -> ball y e x. +Proof. by rewrite /ball /= distrC. Qed. + +Local Lemma ball_triangle x y z e1 e2 : ball x e1 y -> ball y e2 z -> + ball x (e1 + e2) z. +Proof. +rewrite /ball /= => ? ?. +rewrite -[x](subrK y) -(addrA (x + _)). +by rewrite (le_lt_trans (ler_normD _ _))// ltrD. +Qed. + +Local Lemma entourageE : ent = entourage_ ball. +Proof. by []. Qed. + +HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K M + ent nbhsE ball ball_center ball_sym ball_triangle entourageE. + +End isnormedmodule. + Section EquivalenceNorms. Variables (R : realType). From eb11793b81bbd594be910520f636512d105774a6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:50:38 +0900 Subject: [PATCH 05/29] fix doubled instance --- theories/topology_theory/num_topology.v | 4 ---- 1 file changed, 4 deletions(-) diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index e1d281316b..fc7caea215 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -82,10 +82,6 @@ HB.instance Definition _ (R : numFieldType) := Uniform_isPseudoMetric.Build R R^o ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. -HB.instance Definition _ (R : numFieldType) := - Uniform_isPseudoMetric.Build R R^o - ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. - Lemma real_order_nbhsE (R : realFieldType) (x : R^o) : nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]). Proof. From 3d0e6b64736774eff260f556243dfc40ee4ea20c Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 15:01:00 +0900 Subject: [PATCH 06/29] fix --- theories/normedtype_theory/tvs.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 35062f5eb7..83107615a8 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -728,7 +728,7 @@ Qed. Let standard_locally_convex_set : exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B. -(*======= + Local Lemma standard_sub_unif_continuous : unif_continuous (fun x : R^o * R^o => x.1 - x.2). Proof. move=> /= U; rewrite /nbhs/= -!entourage_ballE => -[]/= e e0 /subsetP eU. @@ -740,7 +740,6 @@ by rewrite (le_lt_trans (ler_normB _ _))// (splitr e) ltrD. Qed. Local Lemma standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2). ->>>>>>> 50b14da8 (holomorphic):theories/tvs.v*) Proof. exists [set B | exists x r, B = ball x r]. by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set. @@ -751,7 +750,7 @@ Qed. HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. -(*HB.instance Definition _ := PreUniformNmodule_isUniformZmodule.Build R^o standard_sub_unif_continuous.*) +HB.instance Definition _ := PreUniformNmodule_isUniformZmodule.Build R^o standard_sub_unif_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous. HB.instance Definition _ := From 26ecfc6800b03028c071edd8cdc274b8e62371c1 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 15:04:19 +0900 Subject: [PATCH 07/29] fix --- theories/normedtype_theory/tvs.v | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 83107615a8..978bf936cd 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -728,6 +728,12 @@ Qed. Let standard_locally_convex_set : exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B. +exists [set B | exists x r, B = ball x r]. + by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set. +split; first by move=> B [x] [r] ->; exact: ball_open. +move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. +by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. +Qed. Local Lemma standard_sub_unif_continuous : unif_continuous (fun x : R^o * R^o => x.1 - x.2). Proof. @@ -739,15 +745,6 @@ apply: eU => /=; rewrite inE/= /ball/= opprD addrACA -opprD. by rewrite (le_lt_trans (ler_normB _ _))// (splitr e) ltrD. Qed. -Local Lemma standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2). -Proof. -exists [set B | exists x r, B = ball x r]. - by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set. -split; first by move=> B [x] [r] ->; exact: ball_open. -move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. -by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. -Qed. - HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. HB.instance Definition _ := PreUniformNmodule_isUniformZmodule.Build R^o standard_sub_unif_continuous. From 5a81b81e4dffb5fc823773392b9a9484b0334951 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 16:09:30 +0900 Subject: [PATCH 08/29] fix wip --- theories/holomorphy.v | 36 +++++++++++++++++++++++++++++++++--- 1 file changed, 33 insertions(+), 3 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index e9263dd257..11106c95bb 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -1,4 +1,4 @@ - + (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) (*Require Import ssrsearch.*) From HB Require Import structures. @@ -39,12 +39,42 @@ HB.instance Definition _ (R : rcfType) := UniformZmodule.copy R[i] R[i]^o. HB.instance Definition _ (R : rcfType) := UniformZmodule.copy (Rcomplex R) R[i]. HB.instance Definition _ (R : rcfType) := Pointed.copy (Rcomplex R) R[i]. +Fail HB.instance Definition _ (R : rcfType) := Num.SemiNormedZmodule.copy (Rcomplex R) R. + Module Rcomplex_NormedModType. Section Rcomplex_NormedModType. Variable (R : rcfType). +Import Normc. +Import Num. + +(* Lemmas to be used generally when norm is redefined *) + +#[local] Lemma ler_normcD : forall (x y : Rcomplex R), normc (x + y) <= normc x + normc y. +Proof. +Admitted. +#[local] Lemma normrcMn : forall (x : Rcomplex R) n, normc (x *+ n) = normc x *+ n. +Proof. +Admitted. + +#[local] Lemma normrcN : forall (x : Rcomplex R), normc (- x) = normc x. +Proof. +Admitted. + +HB.instance Definition _ := @Num.Zmodule_isSemiNormed.Build R (Rcomplex R) (@normc R) ler_normcD normrcMn normrcN. + + +#[local] Lemma normrc0_eq0 : forall x : Rcomplex R, normc x = 0 -> x = 0. +Proof. +Admitted. + +HB.instance Definition _ := @Num.SemiNormedZmodule_isPositiveDefinite.Build R (Rcomplex R) normrc0_eq0. + +Check (Rcomplex R : Num.SemiNormedZmodule.type R). +Check (Rcomplex R : Num.NormedZmodule.type R). +Check (Rcomplex R : zmodType). -Definition ball_Rcomplex : Rcomplex R -> R -> Rcomplex R -> Prop := - ball_ Num.norm. +Definition ball_Rcomplex : (Rcomplex R) -> R -> set (Rcomplex R) := + ball_ (@normc R). Lemma entourage_RcomplexE : entourage = entourage_ ball_Rcomplex. Proof. From 1a568b3a30f8cd72a3e8c548c555905d692c83c7 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 16:16:20 +0900 Subject: [PATCH 09/29] wip --- theories/holomorphy.v | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 11106c95bb..aa381fc8d4 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -69,21 +69,18 @@ Admitted. HB.instance Definition _ := @Num.SemiNormedZmodule_isPositiveDefinite.Build R (Rcomplex R) normrc0_eq0. -Check (Rcomplex R : Num.SemiNormedZmodule.type R). -Check (Rcomplex R : Num.NormedZmodule.type R). -Check (Rcomplex R : zmodType). - Definition ball_Rcomplex : (Rcomplex R) -> R -> set (Rcomplex R) := ball_ (@normc R). +(* beware that Re and complex.Re don't look similar *) Lemma entourage_RcomplexE : entourage = entourage_ ball_Rcomplex. Proof. rewrite entourage_nbhsE/= eqEsubset. split; apply/subsetP => U; rewrite inE => -[]. move=> V []/= e; rewrite ltcE => /andP[]/eqP/= ei0 e0. - have ->: e = (Re e)%:C by case: e ei0 {e0} => r i/= ->. + have ->: e = (Re e). case: e ei0 {e0} => r i/= ->. admit. move=> /subsetP eV /subsetP VU. - rewrite inE; exists (Re e) => //. + rewrite inE; exists (complex.Re e) => //. apply/subsetP => -[] a b; rewrite inE/= /ball/= => abe. by apply: VU; rewrite inE/=; apply: eV; rewrite inE/= add0r opprB ltcR. move=> e/= e0 /subsetP eU. From 10fc5163f93d0469a2d2dedea9edf3e8fb42c5f9 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 22:55:34 +0900 Subject: [PATCH 10/29] wip --- theories/holomorphy.v | 65 +++++++++++++++++++++++-------------------- 1 file changed, 35 insertions(+), 30 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index aa381fc8d4..906c2c95bb 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -39,13 +39,33 @@ HB.instance Definition _ (R : rcfType) := UniformZmodule.copy R[i] R[i]^o. HB.instance Definition _ (R : rcfType) := UniformZmodule.copy (Rcomplex R) R[i]. HB.instance Definition _ (R : rcfType) := Pointed.copy (Rcomplex R) R[i]. -Fail HB.instance Definition _ (R : rcfType) := Num.SemiNormedZmodule.copy (Rcomplex R) R. - Module Rcomplex_NormedModType. Section Rcomplex_NormedModType. Variable (R : rcfType). Import Normc. -Import Num. + +Definition ball_Rcomplex : (Rcomplex R) -> R -> set (Rcomplex R) := + ball_ (@normc R). + +(* beware that Re and complex.Re don't look similar *) +Lemma entourage_RcomplexE : entourage = entourage_ ball_Rcomplex. +Proof. +rewrite entourage_nbhsE/= eqEsubset. +split; apply/subsetP => U; rewrite inE => -[]. + move=> V []/= e; rewrite ltcE => /andP[]/eqP/= ei0 e0. + have ->: e = (Re e)%:C by case: e ei0 {e0} => r i/= ->. + move=> /subsetP eV /subsetP VU. + rewrite inE; exists (Re e) => //. + apply/subsetP => -[] a b; rewrite inE/= /ball/= => abe. + by apply: VU; rewrite inE/=; apply: eV; rewrite inE/= add0r opprB ltcR. +move=> e/= e0 /subsetP eU. +rewrite inE; exists (ball_Rcomplex 0 e). + exists e%:C; first by rewrite /= ltcR. + by apply/subsetP => x; rewrite !inE/= ltcR. +apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe. +by apply: eU; rewrite inE. +Qed. + (* Lemmas to be used generally when norm is redefined *) @@ -69,28 +89,6 @@ Admitted. HB.instance Definition _ := @Num.SemiNormedZmodule_isPositiveDefinite.Build R (Rcomplex R) normrc0_eq0. -Definition ball_Rcomplex : (Rcomplex R) -> R -> set (Rcomplex R) := - ball_ (@normc R). - -(* beware that Re and complex.Re don't look similar *) -Lemma entourage_RcomplexE : entourage = entourage_ ball_Rcomplex. -Proof. -rewrite entourage_nbhsE/= eqEsubset. -split; apply/subsetP => U; rewrite inE => -[]. - move=> V []/= e; rewrite ltcE => /andP[]/eqP/= ei0 e0. - have ->: e = (Re e). case: e ei0 {e0} => r i/= ->. admit. - move=> /subsetP eV /subsetP VU. - rewrite inE; exists (complex.Re e) => //. - apply/subsetP => -[] a b; rewrite inE/= /ball/= => abe. - by apply: VU; rewrite inE/=; apply: eV; rewrite inE/= add0r opprB ltcR. -move=> e/= e0 /subsetP eU. -rewrite inE; exists (ball_Rcomplex 0 e). - exists e%:C; first by rewrite /= ltcR. - by apply/subsetP => x; rewrite !inE/= ltcR. -apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe. -by apply: eU; rewrite inE. -Qed. - HB.instance Definition _ := Uniform_isPseudoMetric.Build R (Rcomplex R) ball_norm_center ball_norm_symmetric ball_norm_triangle entourage_RcomplexE. HB.instance Definition _ := @@ -104,6 +102,8 @@ Qed. HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. +Check (Rcomplex R : normedModType R). + Lemma Rcomplex_findim : Vector.axiom 2 (Rcomplex R). Proof. exists (fun x => \row_(i < 2) [:: Re x; Im x]`_i). @@ -132,19 +132,24 @@ Variable R : realType. Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. Local Notation Rc := (Rcomplex R). +Fail Check (Rcomplex R : normedModType R). (* why ? *) +Fail HB.instance Definition _ := NormedModule.copy R (Rcomplex R). + + -Definition holomorphic (f : C -> C) (c : C) := +Definition holomorphic (f : C^o -> C^o) (c : C) := cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ 0^'). -Lemma holomorphicP (f : C -> C) (c : C) : holomorphic f c <-> derivable f c 1. + +Lemma holomorphicP (f : C^o -> C^o) (c : C) : holomorphic f c <-> derivable f c 1. Proof. rewrite /holomorphic /derivable. suff ->: (fun h : C => h^-1 *: ((f (c + h) - f c))) = - ((fun h : C => h^-1 *: ((f \o shift c) (h *: 1) - f c))) by []. + ((fun h : C => h^-1 *: ((f \o shift c) (h *: (1 : C^o)) - f c))) by []. by apply: funext => h; rewrite complexA [X in f X]addrC. Qed. - -Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:Rc. + +Definition Rdifferentiable (f : C^o -> C^o) (c : C^o) := differentiable f%:Rfun c%:Rc. Definition realC : R -> C := (fun r => r%:C). From a04d50df1a90ee48a54a112068886b29b48272b1 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 10:45:12 +0900 Subject: [PATCH 11/29] wip --- theories/holomorphy.v | 41 ++++++++++++++++++++--------------------- 1 file changed, 20 insertions(+), 21 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 906c2c95bb..380a028245 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -44,11 +44,11 @@ Section Rcomplex_NormedModType. Variable (R : rcfType). Import Normc. -Definition ball_Rcomplex : (Rcomplex R) -> R -> set (Rcomplex R) := +Definition ball_Rcomplex (R : rcfType) : (Rcomplex R) -> R -> set (Rcomplex R) := ball_ (@normc R). (* beware that Re and complex.Re don't look similar *) -Lemma entourage_RcomplexE : entourage = entourage_ ball_Rcomplex. +Lemma entourage_RcomplexE : entourage = entourage_ (@ball_Rcomplex R). Proof. rewrite entourage_nbhsE/= eqEsubset. split; apply/subsetP => U; rewrite inE => -[]. @@ -72,6 +72,7 @@ Qed. #[local] Lemma ler_normcD : forall (x y : Rcomplex R), normc (x + y) <= normc x + normc y. Proof. Admitted. + #[local] Lemma normrcMn : forall (x : Rcomplex R) n, normc (x *+ n) = normc x *+ n. Proof. Admitted. @@ -82,7 +83,6 @@ Admitted. HB.instance Definition _ := @Num.Zmodule_isSemiNormed.Build R (Rcomplex R) (@normc R) ler_normcD normrcMn normrcN. - #[local] Lemma normrc0_eq0 : forall x : Rcomplex R, normc x = 0 -> x = 0. Proof. Admitted. @@ -99,10 +99,10 @@ Proof. by case: x => ??; rewrite /normr/= !exprMn -mulrDr sqrtrM ?sqr_ge0// sqrtr_sqr. Qed. -HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. +#[export] HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. -Check (Rcomplex R : normedModType R). +Check (Rcomplex R : normedModType R). Lemma Rcomplex_findim : Vector.axiom 2 (Rcomplex R). Proof. @@ -120,36 +120,35 @@ rewrite ltnS leqn0 => /eqP i0/=. by rewrite {1}i0/=; congr (x ord0); apply: val_inj. Qed. -HB.instance Definition _ := +#[export] HB.instance Definition _ := Lmodule_hasFinDim.Build R (Rcomplex R) Rcomplex_findim. End Rcomplex_NormedModType. End Rcomplex_NormedModType. +HB.export Rcomplex_NormedModType. Section Holomorphe_der. -Variable R : realType. +Variable R : rcfType. Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. -Local Notation Rc := (Rcomplex R). -Fail Check (Rcomplex R : normedModType R). (* why ? *) -Fail HB.instance Definition _ := NormedModule.copy R (Rcomplex R). - +Local Notation Rc := (Rcomplex R). +Check (Rcomplex R : normedModType R). (* why ? *) -Definition holomorphic (f : C^o -> C^o) (c : C) := - cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ 0^'). +Definition holomorphic (f : C -> C) (c : C) := + cvg ((fun h => h^-1 * (f (c + h) - f c)) @ 0^'). -Lemma holomorphicP (f : C^o -> C^o) (c : C) : holomorphic f c <-> derivable f c 1. +Lemma holomorphicP (f : C -> C) (c : C) : holomorphic f c = derivable (f : C^o -> C^o) c 1. Proof. rewrite /holomorphic /derivable. -suff ->: (fun h : C => h^-1 *: ((f (c + h) - f c))) = - ((fun h : C => h^-1 *: ((f \o shift c) (h *: (1 : C^o)) - f c))) by []. +suff ->: (fun h : C => h^-1 * ((f (c + h) - f c))) = + ((fun h : C => h^-1 * ((f \o shift c) (h *: (1 : C^o)) - f c))) by []. by apply: funext => h; rewrite complexA [X in f X]addrC. Qed. -Definition Rdifferentiable (f : C^o -> C^o) (c : C^o) := differentiable f%:Rfun c%:Rc. +Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:Rc. Definition realC : R -> C := (fun r => r%:C). @@ -159,8 +158,8 @@ move=> x A /= [] r /[dup] /realC_gt0 Rer0 /gt0_realC rRe H; exists (Re r) => //. by move=> z /= nz; apply: (H z%:C); rewrite /= -raddfB realC_norm rRe ltcR. Qed. -Lemma Rdiff1 (f : C -> C) c : - lim ((fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ 0^')) +Lemma Rdiff1 (f : C -> C) (c : C) : + lim ((fun h : C => h^-1 * ((f (c + h) - f c))) @ (realC @ 0^')) = 'D_1 (f%:Rfun) c%:Rc. Proof. rewrite /derive. @@ -170,7 +169,7 @@ suff ->: (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC = fun h : R => h^-1 *: ((f \o shift c) (h *: (1%:Rc)) - f c)%:Rc. by []. apply: funext => h /=. -by rewrite -fmorphV /= -!scalecr realC_alg [X in f X]addrC. +rewrite -fmorphV /=. rewrite -!scalecr realC_alg [X in f X]addrC. Qed. Lemma Rdiffi (f : C -> C) c: From a804f6453997ae41a328d41a5d097bee82fc7b9b Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 12:11:10 +0900 Subject: [PATCH 12/29] fix --- theories/topology_theory/uniform_structure.v | 24 +++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index d42004181c..d0ca7182b2 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -286,9 +286,7 @@ by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. Unshelve. all: by end_near. Qed. Lemma continuous_injective_withinNx -(*======= -Lemma within_continuous_withinNx ->>>>>>> 50b14da8 (holomorphic) *) +Proof. (T U : topologicalType) (f : T -> U) (x : T) : {for x, continuous f} -> (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'. @@ -300,6 +298,26 @@ by apply/seteqP; split=> y/=; have /contra_neq /(_ yx) := fI y; tauto. Qed. +Lemma within_continuous_withinNx + (T U : topologicalType) (f : T -> U) (x : T) : + {for x, continuous f} -> + (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'. +Proof. +move=> cf fI A. +rewrite /nbhs /= /dnbhs !withinE/= => -[] V Vfx AV. +move: (cf _ Vfx); rewrite /nbhs/= -/(nbhs _ _) => Vx. +exists (f @^-1` V) => //. +apply/seteqP; split=> y/= [] fyAV yx; split=> //. + suff: f y \in A `&` (fun y : U => y != f x). + by rewrite AV inE => -[]. + rewrite inE/=; split=> //. + by move: yx; apply: contra => /eqP /fI /eqP. +suff: f y \in V `&` (fun y : U => y != f x). + by rewrite -AV inE => -[]. +rewrite inE/=; split=> //. +by move: yx; apply: contra => /eqP /fI /eqP. +Qed. + (* This property is primarily useful for metrizability on uniform spaces *) Definition countable_uniformity (T : uniformType) := exists R : set_system (T * T), [/\ From a45af82d8394b134880adaaa07f2342bb0e280ea Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 12:15:38 +0900 Subject: [PATCH 13/29] wip --- classical/unstable.v | 6 ++ theories/holomorphy.v | 60 +++++++++++--------- theories/topology_theory/uniform_structure.v | 1 - 3 files changed, 39 insertions(+), 28 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 107babe42d..b713a21f00 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -668,6 +668,12 @@ Import complex. Lemma scalecE (w v: C^o) : v *: w = v * w. Proof. by []. Qed. +Lemma scalerc (h : R) (c : C) : h%:C * c = h *: (c : Rcomplex R). +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. diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 380a028245..9e89c144c6 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -66,6 +66,8 @@ apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe. by apply: eU; rewrite inE. Qed. +Check scalecr. + (* Lemmas to be used generally when norm is redefined *) @@ -128,19 +130,22 @@ End Rcomplex_NormedModType. HB.export Rcomplex_NormedModType. Section Holomorphe_der. -Variable R : rcfType. +Variable R : realType. Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. Local Notation Rc := (Rcomplex R). -Check (Rcomplex R : normedModType R). (* why ? *) +Check (Rcomplex R : normedModType R). +Check (Rcomplex R : vectType R). +Check (Rcomplex R : normedVectType R). + Definition holomorphic (f : C -> C) (c : C) := - cvg ((fun h => h^-1 * (f (c + h) - f c)) @ 0^'). + cvg ((fun (h : C) => h^-1 * (f (c + h) - f c)) @ 0^'). -Lemma holomorphicP (f : C -> C) (c : C) : holomorphic f c = derivable (f : C^o -> C^o) c 1. +Lemma holomorphicP (f : C -> C) (c : C) : holomorphic f c <-> derivable (f : C^o -> C^o) c 1. Proof. rewrite /holomorphic /derivable. suff ->: (fun h : C => h^-1 * ((f (c + h) - f c))) = @@ -163,38 +168,38 @@ Lemma Rdiff1 (f : C -> C) (c : C) : = 'D_1 (f%:Rfun) c%:Rc. Proof. rewrite /derive. -rewrite -[LHS]/(lim ((fun h : C => h^-1 *: ((f (c + h) - f c))) +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h) - f c))) \o realC @ 0^')). -suff ->: (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC +suff ->: (fun h : C => h^-1 * (f (c + h) - f c)) \o realC = fun h : R => h^-1 *: ((f \o shift c) (h *: (1%:Rc)) - f c)%:Rc. by []. apply: funext => h /=. -rewrite -fmorphV /=. rewrite -!scalecr realC_alg [X in f X]addrC. +by rewrite -fmorphV realC_alg [X in f X]addrC /realC /= scalerc. Qed. -Lemma Rdiffi (f : C -> C) c: - lim ((fun h : C => h^-1 *: ((f (c + h * 'i) - f c))) @ (realC @ 0^')) +Lemma Rdiffi (f : C^o -> C^o) c: + lim ((fun h : C => h^-1 * ((f (c + h * 'i) - f c))) @ (realC @ 0^')) = 'D_('i) (f%:Rfun) c%:Rc. Proof. rewrite /derive. -rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) +rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC @ 0^')). suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:Rc)) - f c)%:Rc. by []. -apply: funext => h /=. -by rewrite -fmorphV -scalecE -!scalecr realCZ [X in f X]addrC. +apply: funext => h /=. +by rewrite -fmorphV realCZ [X in f X]addrC scalerc. Qed. (* should be generalized to equivalent norms *) (* but there is no way to state it for now *) Lemma littleoCo (h e : C -> C) (x : C) : - [o_x (e : C -> C) of (h : C -> C)] = + [o_x (e : C^o -> C^o) of (h : C^o -> C^o)] = [o_x (e : Rc -> Rc) of (h : Rc -> Rc)]. Proof. -suff heP : (h : C -> C) =o_x (e : C -> C) <-> +suff heP : (h : C^o -> C^o) =o_x (e : C^o -> C^o) <-> (h : Rc -> Rc) =o_x (e : Rc -> Rc). - have [ho|hNo] := asboolP ((h : C -> C) =o_x (e : C -> C)). + have [ho|hNo] := asboolP ((h : C^o -> C^o) =o_x (e : C^o -> C^o)). by rewrite !littleoE// -!eqoP// -heP. by rewrite !littleoE0// -!eqoP// -heP. rewrite !eqoP; split => small/= _ /posnumP[eps]; near=> y. @@ -209,30 +214,31 @@ Definition CauchyRiemannEq (f : C -> C) c := 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. Lemma holo_differentiable (f : C -> C) (c : C) : - holomorphic f c -> Rdifferentiable f c. + holomorphic f c -> Rdifferentiable f (c : Rc). Proof. move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. -pose df : Rc -> Rc := 'd f c. -have lDf : linear df by move=> t u v; rewrite /df !scalecr linearP. +pose df : Rc -> Rc := 'd (f%:Rfun)(c%:Rc). +have lDf : linear df by move=> t u v; rewrite /df linearP. pose df' : {linear Rc -> Rc} := - HB.pack df (GRing.isLinear.Build _ _ _ _ df lDf). -apply/diff_locallyP; split; first exact: linear_findim_continuous. -have eqdf : f%:Rfun \o +%R^~ c = cst (f c) + df' +o_ (0 : Rc) id. - rewrite [LHS]holo /df'/=/df/=. - congr (_ + _). - exact: littleoCo. + HB.pack df (GRing.isLinear.Build R Rc _ _ df lDf). +apply/diff_locallyP; split; first by exact: linear_findim_continuous. +have eqdf : f%:Rfun \o +%R^~ c = cst (f c : Rc) + df' +o_ (0 : Rc) id. + rewrite [LHS]holo /=. + congr (_ + _). congr (_ + _). + rewrite /df /df'. Fail reflexivity. admit. + Fail exact: littleoCo. admit. rewrite (@diff_unique R (Rcomplex R) (Rcomplex R) _ df' _ _ eqdf). exact: eqdf. exact: linear_findim_continuous. (* TODO: fix Qed performance issue (which is due to the proof of `eqdf`). 3.684s *) -Qed. +Admitted. Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. Proof. move=> /cvg_ex; rewrite //= /CauchyRiemannEq. rewrite -Rdiff1 -Rdiffi. -set quotC : C -> C := fun h : R[i] => h^-1 *: (f (c + h) - f c). -set quotR : C -> C:= fun h => h^-1 *: (f (c + h * 'i) - f c) . +set quotC : C -> C := fun h : R[i] => h^-1 * (f (c + h) - f c). +set quotR : C -> C:= fun h => h^-1 *: ((f (c + h * 'i) - f c) : C^o) . move => /= [l H]. have -> : quotR @ (realC @ 0^') = (quotR \o realC) @ 0^' by []. have realC'0: realC @ 0^' --> 0^'. diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index d0ca7182b2..c821fac598 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -286,7 +286,6 @@ by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. Unshelve. all: by end_near. Qed. Lemma continuous_injective_withinNx -Proof. (T U : topologicalType) (f : T -> U) (x : T) : {for x, continuous f} -> (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'. From 63a5d212ed203f1a1f7de5d2e434433418a52a91 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 16:41:46 +0900 Subject: [PATCH 14/29] exists diff --- theories/derive.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index e4a340616d..f48d185caf 100644 --- a/theories/derive.v +++ b/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,14 @@ rewrite [in LHS]littleo_center0 (comp_centerK x id). by rewrite -[- _ in RHS](comp_centerK x). Qed. +Lemma exists_diff (V W : normedModType R) (f : V -> W) x: + (exists2 l : {linear V -> W}, continuous l & (forall h, f (x + h) = f(x) + l(h) +o_(h \near 0) h)) + -> differentiable f x. +Proof. +move => [l cl hl]. apply/diffP; split. +Admitted. + + 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. From cdd0953f5b9337668880add7ca54231f0dd1f760 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 16:41:52 +0900 Subject: [PATCH 15/29] wip --- theories/holomorphy.v | 55 +++++++++++++++++++++++++++++-------------- 1 file changed, 37 insertions(+), 18 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 9e89c144c6..79776320fd 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -191,6 +191,7 @@ apply: funext => h /=. by rewrite -fmorphV realCZ [X in f X]addrC scalerc. Qed. + (* should be generalized to equivalent norms *) (* but there is no way to state it for now *) Lemma littleoCo (h e : C -> C) (x : C) : @@ -210,6 +211,7 @@ rewrite -[_%:num]ger0_norm// -rmorphM/= lecR. by near: y; apply: small; rewrite (@normr_gt0 _ (Rcomplex R))//. Unshelve. all: by end_near. Qed. + Definition CauchyRiemannEq (f : C -> C) c := 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. @@ -217,15 +219,29 @@ Lemma holo_differentiable (f : C -> C) (c : C) : holomorphic f c -> Rdifferentiable f (c : Rc). Proof. move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. +have lDf : linear ('d (f%:Rfun) (c%:Rc) : Rc -> Rc) by move=> t u v; rewrite linearP. +pose df : Rc -> Rc := 'd (f%:Rfun)(c%:Rc). +pose df' : {linear Rc -> Rc} := + HB.pack df (GRing.isLinear.Build R Rc _ _ df lDf). + Search (differentiable _ _). +Admitted. +(* +move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. pose df : Rc -> Rc := 'd (f%:Rfun)(c%:Rc). have lDf : linear df by move=> t u v; rewrite /df linearP. pose df' : {linear Rc -> Rc} := HB.pack df (GRing.isLinear.Build R Rc _ _ df lDf). apply/diff_locallyP; split; first by exact: linear_findim_continuous. have eqdf : f%:Rfun \o +%R^~ c = cst (f c : Rc) + df' +o_ (0 : Rc) id. - rewrite [LHS]holo /=. - congr (_ + _). congr (_ + _). - rewrite /df /df'. Fail reflexivity. admit. + rewrite [LHS]holo /df'/=/df/=. + congr (_ + _). + exact: littleoCo. +*) +(* + apply/eqaddoE. + rewrite [LHS]holo. + congr (_ + _). congr (_ + _). + rewrite /df /df' /=. reflexivity. admit. Fail exact: littleoCo. admit. rewrite (@diff_unique R (Rcomplex R) (Rcomplex R) _ df' _ _ eqdf). exact: eqdf. @@ -233,6 +249,7 @@ exact: linear_findim_continuous. (* TODO: fix Qed performance issue (which is due to the proof of `eqdf`). 3.684s *) Admitted. +*) Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. Proof. @@ -251,18 +268,18 @@ have lem : quotC \o *%R^~ 'i%R @ (realC @ (0 : R)^') --> l. apply: cvg_comp; last by exact: H. apply: (@cvg_comp _ _ _ realC ( *%R^~ 'i)); first by exact: realC'0. rewrite -[0 in X in _ `=>` X](mul0r 'i%C). - apply: within_continuous_withinNx; first exact: scalel_continuous. + apply: within_continuous_withinNx; first by apply: mulrr_continuous. move=> x /eqP; rewrite mul0r mulIr_eq0; last by apply/rregP; apply: neq0Ci. exact: eqP. have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) . by apply/cvg_ex; simpl; exists l. have ->: lim (quotR @ (realC @ ((0 : R)^'))) - = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ ((0 : R)^'))). - have: 'i \*:quotC \o ( fun h => h *'i) =1 quotR. - move=> h /=; rewrite /quotC /quotR /=. - rewrite invfM scalerA mulrC -mulrA mulVf ?mulr1 ?neq0Ci //. - by move=> /funext <-; rewrite limZr. -rewrite scalecE. + = 'i * lim (quotC \o ( fun h => h *'i) @ (realC @ ((0 : R)^'))). + have: (fun x => 'i) \* quotC \o ( fun h => h *'i) =1 quotR. + move=> h /=; rewrite /quotC /quotR /=. + rewrite invfM mulrA (mulrC _ ('i)^-1) mulrA divff ?complexiE ?neq0Ci //. + by rewrite mul1r scalecE. + move=> /funext <-. rewrite limM ?lim_cst. by []. by []. exact: cvg_cst. by []. by []. suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = lim (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) by []. suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = l. @@ -271,24 +288,26 @@ by apply: cvg_lim; last exact: HR0. Qed. Lemma Diff_CR_holo (f : C -> C) (c : C): - (Rdifferentiable f c) /\ (CauchyRiemannEq f c) -> (holomorphic f c). + Rdifferentiable f c -> CauchyRiemannEq f c -> holomorphic f c. Proof. -move=> [] /= /[dup] H /diff_locallyP => [[derc diff]] CR. +move=> /= /[dup] H /diff_locallyP => [[derc diff]] CR. apply/holomorphicP/derivable1_diffP/diff_locallyP. -pose Df := (fun h : C => h *: ('D_1 f%:Rfun c : C)). -have lDf : linear Df by move=> t u v /=; rewrite /Df scalerDl scalerA scalecE. +pose Df := (fun h : C => h * ('D_1 f%:Rfun c : C)). +have lDf : linear Df. move=> t u v /=; rewrite /Df mulrDl -scalecE. congr (_ + _). +by rewrite (scalecr u t) !scalecE scalecr mulrA. pose df : {linear R[i] -> R[i]} := HB.pack Df (GRing.isLinear.Build _ _ _ _ Df lDf). -have cdf : continuous df by apply: scalel_continuous. +simpl in df. +have cdf : continuous df by apply: mulrr_continuous. have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *) apply: funext => z; rewrite /Df. set x := Re z; set y := Im z. have zeq : z = x *: 1 %:Rc + y *: 'i%:Rc. - by rewrite [LHS]complexE /= realC_alg scalecr scalecE [in RHS]mulrC. + by rewrite [LHS]complexE /= realC_alg scalecr [in RHS]mulrC. rewrite [X in 'd _ _ X]zeq addrC linearP linearZ /= -!deriveE //. rewrite -CR (scalerAl y) -scalecE !scalecr /=. - rewrite -(scalerDl (('D_1 f%:Rfun (c : Rc)) : C) _ (real_complex R x)). - by rewrite addrC -!scalecr -realC_alg -zeq. + by rewrite zeq scalerDl !scalecr mulr1 !scalecE addrC. +split. admit. (*apply: derc.*) have holo: f \o shift c = cst (f c) + df +o_ ( 0 : C) id. rewrite [LHS]diff /= lem. congr (_ + _). From 9f5a929c394c12031ffa3be0ade36cd841026dbd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 16:42:12 +0900 Subject: [PATCH 16/29] TODO --- theories/normedtype_theory/normed_module.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 7f34a7d70b..9c77c159ba 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2651,6 +2651,8 @@ End isnormedmodule. Section EquivalenceNorms. Variables (R : realType). +(* TODO : generalize to a numFieldType *) + (* FIXME: Specialize to vector space with basis and expose this definition (see https://github.com/math-comp/analysis/issues/1911). It will also be possible to generalize to `numFieldType`. *) From bf943f3815104231fac21722b324c2e7ac144064 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 21:58:19 +0900 Subject: [PATCH 17/29] wip --- theories/holomorphy.v | 100 +++++++++++++++++++++++++++++------------- 1 file changed, 70 insertions(+), 30 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 79776320fd..69e207f186 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -177,6 +177,26 @@ apply: funext => h /=. by rewrite -fmorphV realC_alg [X in f X]addrC /realC /= scalerc. Qed. +Lemma Cdiff1 (f : C -> C) (c : C) : + lim ((fun h : C => h^-1 * ((f (c + h) - f c))) @ 0^') + = 'D_1 (f : C^o -> C^o) c. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h) - f c))) + @ 0^')). +suff ->: (fun h : C => h^-1 * (f (c + h) - f c)) + = (fun h : C => h^-1 *: (( (f : C^o -> C^o) \o shift c) (h *: 1 : C^o) - f c) : C^o). + by []. +apply: funext => h /=. +by rewrite scalecE [X in f X]addrC scaler1. +Qed. + +Lemma RCdiff1 (f : C -> C) (c : C) : + 'D_1 (f%:Rfun) c%:Rc = 'D_1 (f : C^o -> C^o) c. +Proof. +rewrite -Rdiff1 -Cdiff1. +Admitted. + Lemma Rdiffi (f : C^o -> C^o) c: lim ((fun h : C => h^-1 * ((f (c + h * 'i) - f c))) @ (realC @ 0^')) = 'D_('i) (f%:Rfun) c%:Rc. @@ -219,24 +239,20 @@ Lemma holo_differentiable (f : C -> C) (c : C) : holomorphic f c -> Rdifferentiable f (c : Rc). Proof. move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. -have lDf : linear ('d (f%:Rfun) (c%:Rc) : Rc -> Rc) by move=> t u v; rewrite linearP. pose df : Rc -> Rc := 'd (f%:Rfun)(c%:Rc). +have ldf : linear df by move=> t u v; rewrite /df linearP. pose df' : {linear Rc -> Rc} := - HB.pack df (GRing.isLinear.Build R Rc _ _ df lDf). - Search (differentiable _ _). -Admitted. -(* -move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. -pose df : Rc -> Rc := 'd (f%:Rfun)(c%:Rc). -have lDf : linear df by move=> t u v; rewrite /df linearP. -pose df' : {linear Rc -> Rc} := - HB.pack df (GRing.isLinear.Build R Rc _ _ df lDf). + HB.pack df (GRing.isLinear.Build R Rc _ _ df ldf). apply/diff_locallyP; split; first by exact: linear_findim_continuous. have eqdf : f%:Rfun \o +%R^~ c = cst (f c : Rc) + df' +o_ (0 : Rc) id. rewrite [LHS]holo /df'/=/df/=. - congr (_ + _). - exact: littleoCo. -*) + congr (_ + _). congr (_+_). admit. + admit. +rewrite (@diff_unique R (Rcomplex R) (Rcomplex R) _ df' _ _ eqdf). + exact: eqdf. +exact: linear_findim_continuous. +Admitted. + (* apply/eqaddoE. rewrite [LHS]holo. @@ -249,7 +265,8 @@ exact: linear_findim_continuous. (* TODO: fix Qed performance issue (which is due to the proof of `eqdf`). 3.684s *) Admitted. -*) + m*) + Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. Proof. @@ -291,28 +308,51 @@ Lemma Diff_CR_holo (f : C -> C) (c : C): Rdifferentiable f c -> CauchyRiemannEq f c -> holomorphic f c. Proof. move=> /= /[dup] H /diff_locallyP => [[derc diff]] CR. -apply/holomorphicP/derivable1_diffP/diff_locallyP. -pose Df := (fun h : C => h * ('D_1 f%:Rfun c : C)). -have lDf : linear Df. move=> t u v /=; rewrite /Df mulrDl -scalecE. congr (_ + _). -by rewrite (scalecr u t) !scalecE scalecr mulrA. +pose Df := (fun h : C => h * ('D_1 (f: C^o -> C^o) c : C)). +have lDf : linear Df. + move=> t u v /=; rewrite /Df mulrDl -scalecE; congr (_ + _). + by rewrite (scalecr u t) !scalecE scalecr mulrA. pose df : {linear R[i] -> R[i]} := HB.pack Df (GRing.isLinear.Build _ _ _ _ Df lDf). -simpl in df. -have cdf : continuous df by apply: mulrr_continuous. +have cdf : continuous df by apply: mulrr_continuous. have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *) - apply: funext => z; rewrite /Df. - set x := Re z; set y := Im z. - have zeq : z = x *: 1 %:Rc + y *: 'i%:Rc. - by rewrite [LHS]complexE /= realC_alg scalecr [in RHS]mulrC. - rewrite [X in 'd _ _ X]zeq addrC linearP linearZ /= -!deriveE //. + apply: funext => -[x y]. + have zeq : (x +i* y) = x *: 1 %:Rc + y *: 'i%:Rc. + by rewrite [LHS]complexE /= realC_alg scalecr [in RHS]mulrC. + rewrite /Df zeq addrC !linearP linearZ/= -!deriveE //. rewrite -CR (scalerAl y) -scalecE !scalecr /=. - by rewrite zeq scalerDl !scalecr mulr1 !scalecE addrC. -split. admit. (*apply: derc.*) -have holo: f \o shift c = cst (f c) + df +o_ ( 0 : C) id. + rewrite scalerDl mulr1 scalecE. + by rewrite scalecE RCdiff1. +apply/holomorphicP/derivable1_diffP/diff_locallyP. +split. + apply: bounded_linear_continuous; apply/linear_boundedP. + have /linear_bounded_continuous/linear_boundedP [M [Mr F]] := derc. + have Mcreal : M%:C \is Num.real. + have := Mr; rewrite -comparable0r => /orP M0. + by rewrite -comparable0r; case: M0 => M0; apply/orP; [left|right]; rewrite lecR. + exists M%:C; split => //. + move => /= x Mcx /= z. + have xreal : x \is Num.real. + rewrite -comparable0r (@comparabler_trans _ M%:C) //. + by apply/orP; left; rewrite ltW. + have /F /(_ z): M < (Re x) by rewrite -ltcR RRe_real //. + rewrite -lem. + set Cdiff := (X in _ -> `|X| <= _); simpl in Cdiff. + have -> : Cdiff = Df z. admit. + by rewrite -lecR rmorphM /= RRe_real //. +rewrite diff. +congr (_ + _). +congr ( _ + _). + set Cdiff := RHS; simpl in Cdiff. + set Rdiff := LHS; simpl in Cdiff. + admit. +rewrite /the_littleo /= /insubd /littleo0 /odflt /oapp /= /insub. +(*have holo: f \o shift c = cst (f c) + df +o_ ( 0 : C) id. rewrite [LHS]diff /= lem. congr (_ + _). - exact/esym/littleoCo. -by rewrite (diff_unique cdf holo). + exact/esym/littleoCo. +by rewrite (diff_unique cdf holo) *) + (* TODO: fix Qed performance issue (which is due to the proof of `holo`). 6.519s *) Qed. From 61aa05153b0d110f74d87123d223388107bfbbdd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 11 Jun 2026 10:26:53 +0900 Subject: [PATCH 18/29] fix --- theories/holomorphy.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 69e207f186..d61ba649c5 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -288,7 +288,7 @@ have lem : quotC \o *%R^~ 'i%R @ (realC @ (0 : R)^') --> l. apply: within_continuous_withinNx; first by apply: mulrr_continuous. move=> x /eqP; rewrite mul0r mulIr_eq0; last by apply/rregP; apply: neq0Ci. exact: eqP. -have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) . +have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))). by apply/cvg_ex; simpl; exists l. have ->: lim (quotR @ (realC @ ((0 : R)^'))) = 'i * lim (quotC \o ( fun h => h *'i) @ (realC @ ((0 : R)^'))). @@ -309,12 +309,12 @@ Lemma Diff_CR_holo (f : C -> C) (c : C): Proof. move=> /= /[dup] H /diff_locallyP => [[derc diff]] CR. pose Df := (fun h : C => h * ('D_1 (f: C^o -> C^o) c : C)). -have lDf : linear Df. - move=> t u v /=; rewrite /Df mulrDl -scalecE; congr (_ + _). +have lDf : linear Df. + move=> t u v /=; rewrite /Df mulrDl -scalecE; congr (_ + _). by rewrite (scalecr u t) !scalecE scalecr mulrA. pose df : {linear R[i] -> R[i]} := HB.pack Df (GRing.isLinear.Build _ _ _ _ Df lDf). -have cdf : continuous df by apply: mulrr_continuous. +have cdf : continuous df by apply: mulrr_continuous. have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *) apply: funext => -[x y]. have zeq : (x +i* y) = x *: 1 %:Rc + y *: 'i%:Rc. @@ -332,7 +332,7 @@ split. by rewrite -comparable0r; case: M0 => M0; apply/orP; [left|right]; rewrite lecR. exists M%:C; split => //. move => /= x Mcx /= z. - have xreal : x \is Num.real. + have xreal : x \is Num.real. rewrite -comparable0r (@comparabler_trans _ M%:C) //. by apply/orP; left; rewrite ltW. have /F /(_ z): M < (Re x) by rewrite -ltcR RRe_real //. @@ -355,7 +355,7 @@ by rewrite (diff_unique cdf holo) *) (* TODO: fix Qed performance issue (which is due to the proof of `holo`). 6.519s *) -Qed. +Admitted. Lemma holomorphic_Rdiff (f : C -> C) (c : C) : (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c). From a28dfa070dcdaa61d2d23e270758585551cbe313 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 11 Jun 2026 14:42:26 +0900 Subject: [PATCH 19/29] wip --- theories/derive.v | 17 ++++++--- theories/holomorphy.v | 82 +++++++++++++++++++++++++++++++++++++------ 2 files changed, 84 insertions(+), 15 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index f48d185caf..ca2acce49f 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -566,13 +566,22 @@ rewrite [in LHS]littleo_center0 (comp_centerK x id). by rewrite -[- _ in RHS](comp_centerK x). Qed. -Lemma exists_diff (V W : normedModType R) (f : V -> W) x: - (exists2 l : {linear V -> W}, continuous l & (forall h, f (x + h) = f(x) + l(h) +o_(h \near 0) h)) - -> differentiable f x. +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. -move => [l cl hl]. apply/diffP; split. Admitted. +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 lem : 'd f x = l :> (V -> W). + by apply:(@diff_unique V W f l x cl); exact/funext/shift_addo. +by apply/diffP => //=; split; rewrite lem => // 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. diff --git a/theories/holomorphy.v b/theories/holomorphy.v index d61ba649c5..35263192f0 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -1,4 +1,3 @@ - (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) (*Require Import ssrsearch.*) From HB Require Import structures. @@ -66,8 +65,6 @@ apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe. by apply: eU; rewrite inE. Qed. -Check scalecr. - (* Lemmas to be used generally when norm is redefined *) @@ -178,24 +175,87 @@ by rewrite -fmorphV realC_alg [X in f X]addrC /realC /= scalerc. Qed. Lemma Cdiff1 (f : C -> C) (c : C) : - lim ((fun h : C => h^-1 * ((f (c + h) - f c))) @ 0^') + lim ((fun h : C => h^-1 * ((f (h + c) - f c))) @ 0^') = 'D_1 (f : C^o -> C^o) c. Proof. rewrite /derive. -rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h) - f c))) +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (h + c) - f c))) @ 0^')). -suff ->: (fun h : C => h^-1 * (f (c + h) - f c)) +suff ->: (fun h : C => h^-1 * (f (h + c) - f c)) = (fun h : C => h^-1 *: (( (f : C^o -> C^o) \o shift c) (h *: 1 : C^o) - f c) : C^o). by []. apply: funext => h /=. -by rewrite scalecE [X in f X]addrC scaler1. +by rewrite scalecE scaler1. +Qed. + +From mathcomp Require Import ssrAC. + +Lemma mulOo [K : rcfType] [pT : pointedType] (F : filter_on pT) + (h1 h2 f g : pT -> K^o) : [O_F h1 of f] * [o_F h2 of g] =o_F + h1 * h2. +Proof. Admitted. + + +Lemma mulro [K : rcfType] [pT : pointedType] (F : filter_on pT) + (h2 f g : pT -> K^o) : f * [o_F h2 of g] =o_F f * h2. +Proof. Admitted. + +Lemma mulrox [K : rcfType] [pT : pointedType] (F : filter_on pT) + (h2 f g : pT -> K^o) (x : pT) : f x * [o_F h2 of g] x =o_(x \near F) f x * h2 x. +Proof. Admitted. + +Lemma normRcomplex (x : R[i]) : `|x : Rc|%:C = `|x|. +Proof. +by []. Qed. Lemma RCdiff1 (f : C -> C) (c : C) : - 'D_1 (f%:Rfun) c%:Rc = 'D_1 (f : C^o -> C^o) c. + differentiable (f%:Rfun) (c%:Rc) -> + 'D_1 (f : C^o -> C^o) c = 'D_1 (f%:Rfun) c%:Rc. Proof. -rewrite -Rdiff1 -Cdiff1. -Admitted. +move => fdiff. +rewrite -Cdiff1. +apply: (@cvg_lim _ _ _ _ _ (fun h => h^-1 * (f (h + c) - f c))) => //= A. +(*rewrite /nbhs /= /nbhs_ball_ /= /filter_from /=.*) +move => [/= _ /posnumP [r]] /=; rewrite /ball_ /= => H. +near_simpl. +near=> t. +(*exists (r%:Rc) => //=.*) +(*rewrite sub0r normrN => tr t0.*) +apply: H => /=. +rewrite deriveE => //. +rewrite [f _](@diff_locallyx R Rc Rc) => //=. +rewrite (ACl (1*4*2*3)) /= subrr add0r. +have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). + rewrite -[t in LHS]scaler1. + set l : {linear Rc -> Rc} := ('d (f%:Rfun) (c%:Rc)). + rewrite -[t * _](linearZ l). + (* linearZ *) admit. +rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. +rewrite opprD addNKr normrN. +near: t. +case: littleo. +move => h /= H. +near=> t. +rewrite normrM normfV ltr_pdivrMl. +rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. +rewrite -!normRcomplex. +rewrite [r%:num/2]gt0_normc // -rmorphM /= lecR. +near: t. +apply: nbhs_dnbhs. +near_simpl. +apply: H => //. +rewrite -[Normc.normc _]/(`|_|) //. +by rewrite normr_gt0 //. +rewrite mulrC ltr_pM2l //. +rewrite gtr_pMr // invf_lt1 // ?ltr1n //. +rewrite normr_gt0. +near: t. apply: nbhs_dnbhs_neq. +rewrite normr_gt0. +near: t. apply: nbhs_dnbhs_neq. +Unshelve. all: by end_near. +Qed. + Lemma Rdiffi (f : C^o -> C^o) c: lim ((fun h : C => h^-1 * ((f (c + h * 'i) - f c))) @ (realC @ 0^')) @@ -323,7 +383,7 @@ have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *) rewrite -CR (scalerAl y) -scalecE !scalecr /=. rewrite scalerDl mulr1 scalecE. by rewrite scalecE RCdiff1. -apply/holomorphicP/derivable1_diffP/diff_locallyP. +apply/holomorphicP/derivable1_diffP/diff_locallyP. split. apply: bounded_linear_continuous; apply/linear_boundedP. have /linear_bounded_continuous/linear_boundedP [M [Mr F]] := derc. From 304b7d4c471ceeb84ae1c57e8c3dd0c9e4b4dedb Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 11 Jun 2026 18:24:30 +0900 Subject: [PATCH 20/29] RCdiff1 --- theories/holomorphy.v | 66 +++++++++++++++++++++++++++---------------- 1 file changed, 42 insertions(+), 24 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 35263192f0..b32b08cd2b 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -188,6 +188,22 @@ apply: funext => h /=. by rewrite scalecE scaler1. Qed. + +Lemma Rdiffi (f : C^o -> C^o) c: + lim ((fun h : C => h^-1 * ((f (c + h * 'i) - f c))) @ (realC @ 0^')) + = 'D_('i) (f%:Rfun) c%:Rc. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) + \o realC @ 0^')). +suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC + = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:Rc)) - f c)%:Rc. + by []. +apply: funext => h /=. +by rewrite -fmorphV realCZ [X in f X]addrC scalerc. +Qed. + + From mathcomp Require Import ssrAC. Lemma mulOo [K : rcfType] [pT : pointedType] (F : filter_on pT) @@ -209,11 +225,24 @@ Proof. by []. Qed. +(* TODO: clean lemmas about scalec *) +Lemma scaleCr (h : R) (c : R[i]): h *: (c : Rc) = h%:C *: (c : C^o). +Proof. +Admitted. + +Lemma scaleC1 (h : R) : h *: (1 : C^o) = h%:C. +Proof. +Admitted. + + +Definition CauchyRiemannEq (f : C -> C) c := + 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. + Lemma RCdiff1 (f : C -> C) (c : C) : - differentiable (f%:Rfun) (c%:Rc) -> + differentiable (f%:Rfun) (c%:Rc) -> CauchyRiemannEq f c -> 'D_1 (f : C^o -> C^o) c = 'D_1 (f%:Rfun) c%:Rc. Proof. -move => fdiff. +move => fdiff CR. rewrite -Cdiff1. apply: (@cvg_lim _ _ _ _ _ (fun h => h^-1 * (f (h + c) - f c))) => //= A. (*rewrite /nbhs /= /nbhs_ball_ /= /filter_from /=.*) @@ -226,11 +255,17 @@ apply: H => /=. rewrite deriveE => //. rewrite [f _](@diff_locallyx R Rc Rc) => //=. rewrite (ACl (1*4*2*3)) /= subrr add0r. -have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). - rewrite -[t in LHS]scaler1. - set l : {linear Rc -> Rc} := ('d (f%:Rfun) (c%:Rc)). - rewrite -[t * _](linearZ l). - (* linearZ *) admit. +have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). + rewrite (complexE t). + rewrite !linearD. + have -> : (Re t)%:C = Re t *: 1 by rewrite scaleC1. + have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalecr mulrC. + rewrite !linearZ /=. + rewrite -!deriveE //. + rewrite -CR. + rewrite -scalecE. rewrite !scaleCr. rewrite scalerA. + rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)). + by rewrite !scalecE mulr1. rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. rewrite opprD addNKr normrN. near: t. @@ -257,20 +292,6 @@ Unshelve. all: by end_near. Qed. -Lemma Rdiffi (f : C^o -> C^o) c: - lim ((fun h : C => h^-1 * ((f (c + h * 'i) - f c))) @ (realC @ 0^')) - = 'D_('i) (f%:Rfun) c%:Rc. -Proof. -rewrite /derive. -rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) - \o realC @ 0^')). -suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC - = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:Rc)) - f c)%:Rc. - by []. -apply: funext => h /=. -by rewrite -fmorphV realCZ [X in f X]addrC scalerc. -Qed. - (* should be generalized to equivalent norms *) (* but there is no way to state it for now *) @@ -292,9 +313,6 @@ by near: y; apply: small; rewrite (@normr_gt0 _ (Rcomplex R))//. Unshelve. all: by end_near. Qed. -Definition CauchyRiemannEq (f : C -> C) c := - 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. - Lemma holo_differentiable (f : C -> C) (c : C) : holomorphic f c -> Rdifferentiable f (c : Rc). Proof. From 84af9165094989848b8ffdfa854d440c09cb48f8 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 11:35:42 +0900 Subject: [PATCH 21/29] holo Rdiff --- theories/holomorphy.v | 307 ++++++++++++++++++------------------------ 1 file changed, 128 insertions(+), 179 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index b32b08cd2b..3c96cd3a27 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -129,6 +129,7 @@ HB.export Rcomplex_NormedModType. Section Holomorphe_der. Variable R : realType. + Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. Local Notation Rc := (Rcomplex R). @@ -137,7 +138,25 @@ Check (Rcomplex R : vectType R). Check (Rcomplex R : normedVectType R). +From mathcomp Require Import ssrAC. + +Lemma normRcomplex (x : R[i]) : `|x : Rc|%:C = `|x|. +Proof. +by []. +Qed. + +(* TODO: clean lemmas about scalec *) +Lemma scaleCr (h : R) (c : R[i]): h *: (c : Rc) = h%:C *: (c : C^o). +Proof. +by rewrite scalecE scalerc. +Qed. + +Lemma scaleC1 (h : R) : h *: (1 : C^o) = h%:C. +Proof. +Admitted. + +(* TODO : put the h at the left *) Definition holomorphic (f : C -> C) (c : C) := cvg ((fun (h : C) => h^-1 * (f (c + h) - f c)) @ 0^'). @@ -174,6 +193,20 @@ apply: funext => h /=. by rewrite -fmorphV realC_alg [X in f X]addrC /realC /= scalerc. Qed. +Lemma Rdiffv (f : C -> C) (v c : C) : + lim ((fun h : C => h^-1 * ((f (c + h *: (v : C^o)) - f c))) @ (realC @ 0^')) + = 'D_v (f%:Rfun) c%:Rc. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h *: (v : C^o)) - f c))) + \o realC @ 0^')). +suff ->: (fun h : C => h^-1 * (f (c + h *: (v : C^o)) - f c)) \o realC + = fun h : R => h^-1 *: ((f \o shift c) (h *: (v:Rc)) - f c)%:Rc. + by []. +apply: funext => h /=. +by rewrite -fmorphV [X in f X]addrC /realC /= scalerc scaleCr. +Qed. + Lemma Cdiff1 (f : C -> C) (c : C) : lim ((fun h : C => h^-1 * ((f (h + c) - f c))) @ 0^') = 'D_1 (f : C^o -> C^o) c. @@ -204,147 +237,114 @@ by rewrite -fmorphV realCZ [X in f X]addrC scalerc. Qed. -From mathcomp Require Import ssrAC. -Lemma mulOo [K : rcfType] [pT : pointedType] (F : filter_on pT) - (h1 h2 f g : pT -> K^o) : [O_F h1 of f] * [o_F h2 of g] =o_F - h1 * h2. -Proof. Admitted. -Lemma mulro [K : rcfType] [pT : pointedType] (F : filter_on pT) - (h2 f g : pT -> K^o) : f * [o_F h2 of g] =o_F f * h2. -Proof. Admitted. +Definition CauchyRiemannEq (f : C -> C) c := + 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. -Lemma mulrox [K : rcfType] [pT : pointedType] (F : filter_on pT) - (h2 f g : pT -> K^o) (x : pT) : f x * [o_F h2 of g] x =o_(x \near F) f x * h2 x. -Proof. Admitted. -Lemma normRcomplex (x : R[i]) : `|x : Rc|%:C = `|x|. -Proof. -by []. +Lemma is_derive_holo (f : C -> C) (c : C) : + Rdifferentiable f c -> CauchyRiemannEq f c -> + is_derive (c : C^o) 1 (f : C^o -> C^o) ('D_1 (f%:Rfun) c%:Rc). Proof. +move => fdiff CR. +suff lem: (h^-1 * (f (h + c) - f c) @[h --> 0^']) --> 'D_1 (f%:Rfun) (c%:Rc). + split; last first. + by rewrite -Cdiff1; apply: cvg_lim lem; by []. + apply/cvg_ex. eexists. rewrite /=. under eq_fun do rewrite scaler1/=. exact: lem. +move => /= A. + move => [/= _ /posnumP [r]] /=; rewrite /ball_ /= => H. + near_simpl. + near=> t. + apply: H => /=. + rewrite deriveE => //. + rewrite [f _](@diff_locallyx R Rc Rc) => //=. + rewrite (ACl (1*4*2*3)) /= subrr add0r. + have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). + rewrite (complexE t). + rewrite !linearD. + have -> : (Re t)%:C = Re t *: 1 by rewrite scaleC1. + have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalecr mulrC. + rewrite !linearZ -!deriveE // -CR -scalecE /= !scaleCr scalerA. + by rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)) !scalecE mulr1. + rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. + rewrite opprD addNKr normrN. + near: t. + case: littleo. + move => h /= H. + near=> t. + rewrite normrM normfV ltr_pdivrMl; last by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. + rewrite -!normRcomplex. + rewrite [r%:num/2]gt0_normc // -rmorphM /= lecR. + near: t; apply: nbhs_dnbhs; near_simpl. + by apply: H => //; rewrite -[Normc.normc _]/(`|_|) normr_gt0 //. + rewrite mulrC ltr_pM2l //. + by rewrite gtr_pMr // invf_lt1 // ?ltr1n //. + rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. +Unshelve. all: by end_near. Qed. -(* TODO: clean lemmas about scalec *) -Lemma scaleCr (h : R) (c : R[i]): h *: (c : Rc) = h%:C *: (c : C^o). -Proof. -Admitted. +Lemma diff_CR_holo (f : C -> C) (c : C): + Rdifferentiable f c -> CauchyRiemannEq f c -> holomorphic f c. +Proof. +by move=> /is_derive_holo /[apply] ?; exact/holomorphicP. +Qed. -Lemma scaleC1 (h : R) : h *: (1 : C^o) = h%:C. +Lemma is_derive_Rdiff (f : C -> C) (c v : C): + holomorphic f c -> + is_derive (c%:Rc) v (f%:Rfun) ('D_v (f : C^o -> C^o) c). Proof. Admitted. - - -Definition CauchyRiemannEq (f : C -> C) c := - 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. - -Lemma RCdiff1 (f : C -> C) (c : C) : - differentiable (f%:Rfun) (c%:Rc) -> CauchyRiemannEq f c -> - 'D_1 (f : C^o -> C^o) c = 'D_1 (f%:Rfun) c%:Rc. -Proof. -move => fdiff CR. -rewrite -Cdiff1. -apply: (@cvg_lim _ _ _ _ _ (fun h => h^-1 * (f (h + c) - f c))) => //= A. -(*rewrite /nbhs /= /nbhs_ball_ /= /filter_from /=.*) -move => [/= _ /posnumP [r]] /=; rewrite /ball_ /= => H. -near_simpl. -near=> t. -(*exists (r%:Rc) => //=.*) -(*rewrite sub0r normrN => tr t0.*) -apply: H => /=. -rewrite deriveE => //. -rewrite [f _](@diff_locallyx R Rc Rc) => //=. -rewrite (ACl (1*4*2*3)) /= subrr add0r. -have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). - rewrite (complexE t). - rewrite !linearD. - have -> : (Re t)%:C = Re t *: 1 by rewrite scaleC1. - have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalecr mulrC. - rewrite !linearZ /=. - rewrite -!deriveE //. - rewrite -CR. - rewrite -scalecE. rewrite !scaleCr. rewrite scalerA. - rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)). - by rewrite !scalecE mulr1. -rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. -rewrite opprD addNKr normrN. -near: t. -case: littleo. -move => h /= H. -near=> t. -rewrite normrM normfV ltr_pdivrMl. -rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. -rewrite -!normRcomplex. -rewrite [r%:num/2]gt0_normc // -rmorphM /= lecR. -near: t. -apply: nbhs_dnbhs. -near_simpl. -apply: H => //. -rewrite -[Normc.normc _]/(`|_|) //. -by rewrite normr_gt0 //. -rewrite mulrC ltr_pM2l //. -rewrite gtr_pMr // invf_lt1 // ?ltr1n //. -rewrite normr_gt0. -near: t. apply: nbhs_dnbhs_neq. -rewrite normr_gt0. -near: t. apply: nbhs_dnbhs_neq. +(* +move => fdiff. +suff lem: ((h^-1 : R) *: ((f%:Rfun) ( h *:v + (c%:Rc)) - (f%:Rfun) (c%:Rc)) @[h --> 0^']) --> 'D_v (f : C^o -> C^o) (c%:Rc). + split; last first. + rewrite -Rdiffv. apply: cvg_lim. by []. + Search "cvg" "comp". admit. + apply/cvg_ex. eexists. . under eq_fun do rewrite scaler1/=. exact: lem. +move => /= A. + move => [/= _ /posnumP [r]] /=; rewrite /ball_ /= => H. + near_simpl. + near=> t. + apply: H => /=. + rewrite deriveE => //. + rewrite [f _](@diff_locallyx R Rc Rc) => //=. + rewrite (ACl (1*4*2*3)) /= subrr add0r. + have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). + rewrite (complexE t). + rewrite !linearD. + have -> : (Re t)%:C = Re t *: 1 by rewrite scaleC1. + have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalecr mulrC. + rewrite !linearZ -!deriveE // -CR -scalecE /= !scaleCr scalerA. + by rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)) !scalecE mulr1. + rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. + rewrite opprD addNKr normrN. + near: t. + case: littleo. + move => h /= H. + near=> t. + rewrite normrM normfV ltr_pdivrMl; last by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. + rewrite -!normRcomplex. + rewrite [r%:num/2]gt0_normc // -rmorphM /= lecR. + near: t; apply: nbhs_dnbhs; near_simpl. + by apply: H => //; rewrite -[Normc.normc _]/(`|_|) normr_gt0 //. + rewrite mulrC ltr_pM2l //. + by rewrite gtr_pMr // invf_lt1 // ?ltr1n //. + rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. Unshelve. all: by end_near. -Qed. +*) -(* should be generalized to equivalent norms *) -(* but there is no way to state it for now *) -Lemma littleoCo (h e : C -> C) (x : C) : - [o_x (e : C^o -> C^o) of (h : C^o -> C^o)] = - [o_x (e : Rc -> Rc) of (h : Rc -> Rc)]. -Proof. -suff heP : (h : C^o -> C^o) =o_x (e : C^o -> C^o) <-> - (h : Rc -> Rc) =o_x (e : Rc -> Rc). - have [ho|hNo] := asboolP ((h : C^o -> C^o) =o_x (e : C^o -> C^o)). - by rewrite !littleoE// -!eqoP// -heP. - by rewrite !littleoE0// -!eqoP// -heP. -rewrite !eqoP; split => small/= _ /posnumP[eps]; near=> y. - rewrite -lecR/= rmorphM/=. - near: y. - by apply: small; rewrite ltcR. -rewrite -[_%:num]ger0_norm// -rmorphM/= lecR. -by near: y; apply: small; rewrite (@normr_gt0 _ (Rcomplex R))//. -Unshelve. all: by end_near. Qed. - - -Lemma holo_differentiable (f : C -> C) (c : C) : - holomorphic f c -> Rdifferentiable f (c : Rc). +(* exact: linear_findim_continuous. *) + +Lemma holo_differentiable (f : C -> C) (c v : C): + holomorphic f c -> Rdifferentiable f c. Proof. -move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. -pose df : Rc -> Rc := 'd (f%:Rfun)(c%:Rc). -have ldf : linear df by move=> t u v; rewrite /df linearP. -pose df' : {linear Rc -> Rc} := - HB.pack df (GRing.isLinear.Build R Rc _ _ df ldf). -apply/diff_locallyP; split; first by exact: linear_findim_continuous. -have eqdf : f%:Rfun \o +%R^~ c = cst (f c : Rc) + df' +o_ (0 : Rc) id. - rewrite [LHS]holo /df'/=/df/=. - congr (_ + _). congr (_+_). admit. - admit. -rewrite (@diff_unique R (Rcomplex R) (Rcomplex R) _ df' _ _ eqdf). - exact: eqdf. -exact: linear_findim_continuous. Admitted. -(* - apply/eqaddoE. - rewrite [LHS]holo. - congr (_ + _). congr (_ + _). - rewrite /df /df' /=. reflexivity. admit. - Fail exact: littleoCo. admit. -rewrite (@diff_unique R (Rcomplex R) (Rcomplex R) _ df' _ _ eqdf). - exact: eqdf. -exact: linear_findim_continuous. -(* TODO: fix Qed performance issue (which is due to the proof of `eqdf`). - 3.684s *) -Admitted. - m*) - Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. Proof. @@ -382,65 +382,14 @@ suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = l. by apply: cvg_lim; last exact: HR0. Qed. -Lemma Diff_CR_holo (f : C -> C) (c : C): - Rdifferentiable f c -> CauchyRiemannEq f c -> holomorphic f c. -Proof. -move=> /= /[dup] H /diff_locallyP => [[derc diff]] CR. -pose Df := (fun h : C => h * ('D_1 (f: C^o -> C^o) c : C)). -have lDf : linear Df. - move=> t u v /=; rewrite /Df mulrDl -scalecE; congr (_ + _). - by rewrite (scalecr u t) !scalecE scalecr mulrA. -pose df : {linear R[i] -> R[i]} := - HB.pack Df (GRing.isLinear.Build _ _ _ _ Df lDf). -have cdf : continuous df by apply: mulrr_continuous. -have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *) - apply: funext => -[x y]. - have zeq : (x +i* y) = x *: 1 %:Rc + y *: 'i%:Rc. - by rewrite [LHS]complexE /= realC_alg scalecr [in RHS]mulrC. - rewrite /Df zeq addrC !linearP linearZ/= -!deriveE //. - rewrite -CR (scalerAl y) -scalecE !scalecr /=. - rewrite scalerDl mulr1 scalecE. - by rewrite scalecE RCdiff1. -apply/holomorphicP/derivable1_diffP/diff_locallyP. -split. - apply: bounded_linear_continuous; apply/linear_boundedP. - have /linear_bounded_continuous/linear_boundedP [M [Mr F]] := derc. - have Mcreal : M%:C \is Num.real. - have := Mr; rewrite -comparable0r => /orP M0. - by rewrite -comparable0r; case: M0 => M0; apply/orP; [left|right]; rewrite lecR. - exists M%:C; split => //. - move => /= x Mcx /= z. - have xreal : x \is Num.real. - rewrite -comparable0r (@comparabler_trans _ M%:C) //. - by apply/orP; left; rewrite ltW. - have /F /(_ z): M < (Re x) by rewrite -ltcR RRe_real //. - rewrite -lem. - set Cdiff := (X in _ -> `|X| <= _); simpl in Cdiff. - have -> : Cdiff = Df z. admit. - by rewrite -lecR rmorphM /= RRe_real //. -rewrite diff. -congr (_ + _). -congr ( _ + _). - set Cdiff := RHS; simpl in Cdiff. - set Rdiff := LHS; simpl in Cdiff. - admit. -rewrite /the_littleo /= /insubd /littleo0 /odflt /oapp /= /insub. -(*have holo: f \o shift c = cst (f c) + df +o_ ( 0 : C) id. - rewrite [LHS]diff /= lem. - congr (_ + _). - exact/esym/littleoCo. -by rewrite (diff_unique cdf holo) *) - -(* TODO: fix Qed performance issue (which is due to the proof of `holo`). - 6.519s *) -Admitted. Lemma holomorphic_Rdiff (f : C -> C) (c : C) : (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c). Proof. -split=> H; first exact: Diff_CR_holo. -split; first exact: holo_differentiable. -exact: holo_CauchyRiemann. +split; first by move => [Rdiff CR]; exact: diff_CR_holo. +split; first by exact: holo_differentiable. +by exact: holo_CauchyRiemann. Qed. + End Holomorphe_der. From ca443d4d79063869b34b67ab481fd0af57cec7d6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 15:56:06 +0900 Subject: [PATCH 22/29] rdholo rdiff --- theories/holomorphy.v | 69 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 60 insertions(+), 9 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 3c96cd3a27..6aa907d333 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -153,8 +153,8 @@ Qed. Lemma scaleC1 (h : R) : h *: (1 : C^o) = h%:C. Proof. -Admitted. - +by rewrite scaleCr scaler1. +Qed. (* TODO : put the h at the left *) Definition holomorphic (f : C -> C) (c : C) := @@ -291,8 +291,56 @@ Proof. by move=> /is_derive_holo /[apply] ?; exact/holomorphicP. Qed. -Lemma is_derive_Rdiff (f : C -> C) (c v : C): - holomorphic f c -> + +Lemma eqaddoPx {K : numDomainType} {T : Type} {V W : normedModType K} + (F : filter_on T) (f g : T -> V) (e : T -> W) : +(forall x, f x = g x +o_(x \near F) e x) <-> + forall eps : K, 0 < eps -> \near F, `|(f - g) F| <= eps * `|e F|. +Proof. +rewrite -eqaddoP; split=> [fE|->]; last exact/eqaddoEx. +by apply/funext=> x; rewrite fctE. +Qed. + +Lemma holo_differentiable (f : C -> C) (c v : C): + holomorphic f c -> Rdifferentiable f c. +Proof. +move => /holomorphicP/derivable1_diffP fdiff. +rewrite /Rdifferentiable. +pose df (v : Rc) : Rc := 'd (f : C^o -> C^o) (c : C^o) v. +have lindf : linear df. + by move=> /= k x y; rewrite !scaleCr /df /= linearP. +pose Df : {linear Rc -> Rc} := +HB.pack df (@GRing.isLinear.Build _ _ _ _ df lindf). +apply: (exists_diff). +exists Df; first exact: linear_findim_continuous. +rewrite /Df /df /=. +apply/eqaddoPx. +move => r r0. +near=> w. +rewrite /Df /df /=. +have /diff_locallyxP [_ ] := fdiff. +move => /(_ (w - c)). +rewrite !fctE subrK => ->. +rewrite opprD. +rewrite (AC (3*2) ((1*4)*(2*5)*3)) /=. +rewrite !subrr !add0r. +near: w. +case : littleo => /=. +move => h heps. +near=> w. +rewrite -lecR. +rewrite rmorphM /=. +rewrite !normRcomplex. +near: w. +suff: \forall x \near c, `|h (x - c)| <= r%:C * `|x - c|. + exact. +apply/nbhs0P. +near do rewrite addrC addKr. +apply: heps. +by rewrite ltcR. +Unshelve. all: end_near. Qed. + +Lemma is_derive_Rdiff (f : C -> C) (c v : C): is_derive (c%:Rc) v (f%:Rfun) ('D_v (f : C^o -> C^o) c). Proof. Admitted. @@ -339,11 +387,11 @@ Unshelve. all: by end_near. (* exact: linear_findim_continuous. *) - -Lemma holo_differentiable (f : C -> C) (c v : C): - holomorphic f c -> Rdifferentiable f c. -Proof. +(*Lemma thm_qui_manque (K : numFieldType) (V W : normedModType K) (f : V -> W) (c h v: V) (df : W): is_derive c v f df -> + forall h, f ( c + h *: v) = f c + df +o_(v \near c) (v - c). Admitted. +*) + Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. @@ -391,5 +439,8 @@ split; first by exact: holo_differentiable. by exact: holo_CauchyRiemann. Qed. - End Holomorphe_der. + +Search "scale" "C". +Search "scale" "c". +Check scalerc. From a28f43c55d41386c7552a6071bb6552262ec9a76 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 16:52:32 +0900 Subject: [PATCH 23/29] clean --- classical/unstable.v | 54 +++++++-------- theories/holomorphy.v | 151 +++++++++--------------------------------- 2 files changed, 58 insertions(+), 147 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index b713a21f00..48e95f8d8e 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -655,6 +655,15 @@ 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. @@ -665,10 +674,11 @@ 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 * c = h *: (c : Rcomplex R). +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. @@ -755,35 +765,27 @@ 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 realC_alg (a : R) : a *: (1%:RC) = a%:C. +Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed. -Lemma realCZ (a : R) (b : Rcomplex) : a%:C * b = a *: b. -Proof. by case: b => x y; simpc. 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. -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. +(* 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 scalecV (h: R) (v: Rcomplex): - h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *) +Lemma scalec1 (h : R) : h *: (1 : C^o) = h%:C. Proof. -by move=> h0 v0; rewrite scalecr invrM // ?unitfE ?eqCr // mulrC scalecr fmorphV. +by rewrite scalerc mulr1. Qed. -End algebraic_lemmas. + +End complex_extras. + diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 6aa907d333..d9ba8bef71 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -1,6 +1,5 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -(*Require Import ssrsearch.*) -From HB Require Import structures. +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. From mathcomp Require Import ssrnat eqtype seq choice fintype bigop order. From mathcomp Require Import ssralg ssrnum ssrfun matrix complex. @@ -65,7 +64,6 @@ apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe. by apply: eU; rewrite inE. Qed. - (* Lemmas to be used generally when norm is redefined *) #[local] Lemma ler_normcD : forall (x y : Rcomplex R), normc (x + y) <= normc x + normc y. @@ -101,7 +99,6 @@ Qed. #[export] HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. -Check (Rcomplex R : normedModType R). Lemma Rcomplex_findim : Vector.axiom 2 (Rcomplex R). Proof. @@ -126,6 +123,7 @@ End Rcomplex_NormedModType. End Rcomplex_NormedModType. HB.export Rcomplex_NormedModType. + Section Holomorphe_der. Variable R : realType. @@ -145,17 +143,6 @@ Proof. by []. Qed. -(* TODO: clean lemmas about scalec *) -Lemma scaleCr (h : R) (c : R[i]): h *: (c : Rc) = h%:C *: (c : C^o). -Proof. -by rewrite scalecE scalerc. -Qed. - -Lemma scaleC1 (h : R) : h *: (1 : C^o) = h%:C. -Proof. -by rewrite scaleCr scaler1. -Qed. - (* TODO : put the h at the left *) Definition holomorphic (f : C -> C) (c : C) := cvg ((fun (h : C) => h^-1 * (f (c + h) - f c)) @ 0^'). @@ -169,7 +156,8 @@ suff ->: (fun h : C => h^-1 * ((f (c + h) - f c))) = by apply: funext => h; rewrite complexA [X in f X]addrC. Qed. -Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:Rc. + +Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:RC. Definition realC : R -> C := (fun r => r%:C). @@ -181,13 +169,13 @@ Qed. Lemma Rdiff1 (f : C -> C) (c : C) : lim ((fun h : C => h^-1 * ((f (c + h) - f c))) @ (realC @ 0^')) - = 'D_1 (f%:Rfun) c%:Rc. + = 'D_1 (f%:Rfun) c%:RC. Proof. rewrite /derive. rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h) - f c))) \o realC @ 0^')). suff ->: (fun h : C => h^-1 * (f (c + h) - f c)) \o realC - = fun h : R => h^-1 *: ((f \o shift c) (h *: (1%:Rc)) - f c)%:Rc. + = fun h : R => h^-1 *: ((f \o shift c) (h *: (1%:RC)) - f c)%:RC. by []. apply: funext => h /=. by rewrite -fmorphV realC_alg [X in f X]addrC /realC /= scalerc. @@ -195,16 +183,16 @@ Qed. Lemma Rdiffv (f : C -> C) (v c : C) : lim ((fun h : C => h^-1 * ((f (c + h *: (v : C^o)) - f c))) @ (realC @ 0^')) - = 'D_v (f%:Rfun) c%:Rc. + = 'D_v (f%:Rfun) c%:RC. Proof. rewrite /derive. rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h *: (v : C^o)) - f c))) \o realC @ 0^')). suff ->: (fun h : C => h^-1 * (f (c + h *: (v : C^o)) - f c)) \o realC - = fun h : R => h^-1 *: ((f \o shift c) (h *: (v:Rc)) - f c)%:Rc. + = fun h : R => h^-1 *: ((f \o shift c) (h *: (v:Rc)) - f c)%:RC. by []. apply: funext => h /=. -by rewrite -fmorphV [X in f X]addrC /realC /= scalerc scaleCr. +by rewrite -fmorphV [X in f X]addrC /realC /= scalerc scalerc_regular. (*-scaleCE*) Qed. Lemma Cdiff1 (f : C -> C) (c : C) : @@ -224,31 +212,27 @@ Qed. Lemma Rdiffi (f : C^o -> C^o) c: lim ((fun h : C => h^-1 * ((f (c + h * 'i) - f c))) @ (realC @ 0^')) - = 'D_('i) (f%:Rfun) c%:Rc. + = 'D_('i) (f%:Rfun) c%:RC. Proof. rewrite /derive. rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC @ 0^')). suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC - = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:Rc)) - f c)%:Rc. + = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:RC)) - f c)%:RC. by []. apply: funext => h /=. -by rewrite -fmorphV realCZ [X in f X]addrC scalerc. +by rewrite -fmorphV scalerc [X in f X]addrC scalerc. Qed. - - - - Definition CauchyRiemannEq (f : C -> C) c := - 'i * 'D_1 f%:Rfun c%:Rc = 'D_('i) f%:Rfun c%:Rc. + 'i * 'D_1 f%:Rfun c%:RC = 'D_('i) f%:Rfun c%:RC. Lemma is_derive_holo (f : C -> C) (c : C) : Rdifferentiable f c -> CauchyRiemannEq f c -> - is_derive (c : C^o) 1 (f : C^o -> C^o) ('D_1 (f%:Rfun) c%:Rc). Proof. + is_derive (c : C^o) 1 (f : C^o -> C^o) ('D_1 (f%:Rfun) c%:RC). Proof. move => fdiff CR. -suff lem: (h^-1 * (f (h + c) - f c) @[h --> 0^']) --> 'D_1 (f%:Rfun) (c%:Rc). +suff lem: (h^-1 * (f (h + c) - f c) @[h --> 0^']) --> 'D_1 (f%:Rfun) (c%:RC). split; last first. by rewrite -Cdiff1; apply: cvg_lim lem; by []. apply/cvg_ex. eexists. rewrite /=. under eq_fun do rewrite scaler1/=. exact: lem. @@ -260,12 +244,12 @@ move => /= A. rewrite deriveE => //. rewrite [f _](@diff_locallyx R Rc Rc) => //=. rewrite (ACl (1*4*2*3)) /= subrr add0r. - have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). + have -> : 'd (f%:Rfun) (c%:RC) (t : Rc) = t * 'd (f%:Rfun) (c%:RC) (1: Rc). rewrite (complexE t). rewrite !linearD. - have -> : (Re t)%:C = Re t *: 1 by rewrite scaleC1. - have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalecr mulrC. - rewrite !linearZ -!deriveE // -CR -scalecE /= !scaleCr scalerA. + have -> : (Re t)%:C = Re t *: 1 by rewrite scalec1. + have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalerc mulrC. + rewrite !linearZ -!deriveE // -CR /= !scalerc_regular scalerA. by rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)) !scalecE mulr1. rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. rewrite opprD addNKr normrN. @@ -308,91 +292,20 @@ move => /holomorphicP/derivable1_diffP fdiff. rewrite /Rdifferentiable. pose df (v : Rc) : Rc := 'd (f : C^o -> C^o) (c : C^o) v. have lindf : linear df. - by move=> /= k x y; rewrite !scaleCr /df /= linearP. -pose Df : {linear Rc -> Rc} := -HB.pack df (@GRing.isLinear.Build _ _ _ _ df lindf). -apply: (exists_diff). -exists Df; first exact: linear_findim_continuous. -rewrite /Df /df /=. -apply/eqaddoPx. -move => r r0. -near=> w. -rewrite /Df /df /=. + by move=> /= k x y; rewrite !scalerc /df /= linearP. +pose Df : {linear Rc -> Rc} := HB.pack df (@GRing.isLinear.Build _ _ _ _ df lindf). +apply: (exists_diff); exists Df; first exact: linear_findim_continuous. +rewrite /Df /df /=; apply/eqaddoPx => r r0; near=> w. have /diff_locallyxP [_ ] := fdiff. -move => /(_ (w - c)). -rewrite !fctE subrK => ->. -rewrite opprD. -rewrite (AC (3*2) ((1*4)*(2*5)*3)) /=. -rewrite !subrr !add0r. -near: w. -case : littleo => /=. -move => h heps. -near=> w. -rewrite -lecR. -rewrite rmorphM /=. -rewrite !normRcomplex. -near: w. -suff: \forall x \near c, `|h (x - c)| <= r%:C * `|x - c|. - exact. -apply/nbhs0P. -near do rewrite addrC addKr. -apply: heps. +move => /(_ (w - c)); rewrite !fctE subrK => ->. +rewrite opprD (AC (3*2) ((1*4)*(2*5)*3)) /= !subrr !add0r. +near: w; case : littleo => /= h heps; near=> w. +rewrite -lecR rmorphM /= !normRcomplex; near: w. +suff: \forall x \near c, `|h (x - c)| <= r%:C * `|x - c| by exact. +apply/nbhs0P; near do rewrite addrC addKr; apply: heps. by rewrite ltcR. Unshelve. all: end_near. Qed. -Lemma is_derive_Rdiff (f : C -> C) (c v : C): - is_derive (c%:Rc) v (f%:Rfun) ('D_v (f : C^o -> C^o) c). -Proof. -Admitted. -(* -move => fdiff. -suff lem: ((h^-1 : R) *: ((f%:Rfun) ( h *:v + (c%:Rc)) - (f%:Rfun) (c%:Rc)) @[h --> 0^']) --> 'D_v (f : C^o -> C^o) (c%:Rc). - split; last first. - rewrite -Rdiffv. apply: cvg_lim. by []. - Search "cvg" "comp". admit. - apply/cvg_ex. eexists. . under eq_fun do rewrite scaler1/=. exact: lem. -move => /= A. - move => [/= _ /posnumP [r]] /=; rewrite /ball_ /= => H. - near_simpl. - near=> t. - apply: H => /=. - rewrite deriveE => //. - rewrite [f _](@diff_locallyx R Rc Rc) => //=. - rewrite (ACl (1*4*2*3)) /= subrr add0r. - have -> : 'd (f%:Rfun) (c%:Rc) (t : Rc) = t * 'd (f%:Rfun) (c%:Rc) (1: Rc). - rewrite (complexE t). - rewrite !linearD. - have -> : (Re t)%:C = Re t *: 1 by rewrite scaleC1. - have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalecr mulrC. - rewrite !linearZ -!deriveE // -CR -scalecE /= !scaleCr scalerA. - by rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)) !scalecE mulr1. - rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. - rewrite opprD addNKr normrN. - near: t. - case: littleo. - move => h /= H. - near=> t. - rewrite normrM normfV ltr_pdivrMl; last by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. - rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. - rewrite -!normRcomplex. - rewrite [r%:num/2]gt0_normc // -rmorphM /= lecR. - near: t; apply: nbhs_dnbhs; near_simpl. - by apply: H => //; rewrite -[Normc.normc _]/(`|_|) normr_gt0 //. - rewrite mulrC ltr_pM2l //. - by rewrite gtr_pMr // invf_lt1 // ?ltr1n //. - rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. -Unshelve. all: by end_near. -*) - - - -(* exact: linear_findim_continuous. *) -(*Lemma thm_qui_manque (K : numFieldType) (V W : normedModType K) (f : V -> W) (c h v: V) (df : W): is_derive c v f df -> - forall h, f ( c + h *: v) = f c + df +o_(v \near c) (v - c). -Admitted. -*) - - Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. Proof. @@ -440,7 +353,3 @@ by exact: holo_CauchyRiemann. Qed. End Holomorphe_der. - -Search "scale" "C". -Search "scale" "c". -Check scalerc. From 6638b717a10b970132314ddcf8ff3541bc842efc Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 17:06:06 +0900 Subject: [PATCH 24/29] wip shiftaddo --- theories/derive.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index ca2acce49f..6d664187ec 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -570,6 +570,9 @@ 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. + rewrite fE. +rewrite addrK. Admitted. Lemma exists_diff (V W: normedModType R) (f : V -> W) x: From 54c6a34228c05eb66409860c893c2c84b6a2a85e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jun 2026 13:57:32 +0900 Subject: [PATCH 25/29] upd --- theories/holomorphy.v | 49 ++++++++++++++++++++++++++----------------- 1 file changed, 30 insertions(+), 19 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index d9ba8bef71..defb2bf66a 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -1,8 +1,9 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +@(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. +(*From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. From mathcomp Require Import ssrnat eqtype seq choice fintype bigop order. -From mathcomp Require Import ssralg ssrnum ssrfun matrix complex. +From mathcomp Require Import ssralg ssrnum ssrfun matrix complex.*) +From mathcomp Require Import boot order algebra complex. From mathcomp Require Import unstable boolp reals ereal derive. From mathcomp Require Import classical_sets functions interval_inference. From mathcomp Require Import topology normedtype landau. @@ -21,6 +22,8 @@ From mathcomp Require Import topology normedtype landau. (* *) (******************************************************************************) +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) + Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def complex. Local Open Scope ring_scope. Local Open Scope classical_set_scope. @@ -66,7 +69,7 @@ Qed. (* Lemmas to be used generally when norm is redefined *) -#[local] Lemma ler_normcD : forall (x y : Rcomplex R), normc (x + y) <= normc x + normc y. +(*#[local] Lemma ler_normcD : forall (x y : Rcomplex R), normc (x + y) <= normc x + normc y. Proof. Admitted. @@ -78,13 +81,13 @@ Admitted. Proof. Admitted. -HB.instance Definition _ := @Num.Zmodule_isSemiNormed.Build R (Rcomplex R) (@normc R) ler_normcD normrcMn normrcN. +HB.instance Definition _ := @Num.Zmodule_isSemiNormed.Build R (Rcomplex R) (@normc R) ler_normcD normrcMn normrcN.*) -#[local] Lemma normrc0_eq0 : forall x : Rcomplex R, normc x = 0 -> x = 0. +(*#[local] Lemma normrc0_eq0 : forall x : Rcomplex R, normc x = 0 -> x = 0. Proof. Admitted. -HB.instance Definition _ := @Num.SemiNormedZmodule_isPositiveDefinite.Build R (Rcomplex R) normrc0_eq0. +HB.instance Definition _ := @Num.SemiNormedZmodule_isPositiveDefinite.Build R (Rcomplex R) normrc0_eq0.*) HB.instance Definition _ := Uniform_isPseudoMetric.Build R (Rcomplex R) ball_norm_center ball_norm_symmetric ball_norm_triangle entourage_RcomplexE. @@ -246,28 +249,31 @@ move => /= A. rewrite (ACl (1*4*2*3)) /= subrr add0r. have -> : 'd (f%:Rfun) (c%:RC) (t : Rc) = t * 'd (f%:Rfun) (c%:RC) (1: Rc). rewrite (complexE t). - rewrite !linearD. - have -> : (Re t)%:C = Re t *: 1 by rewrite scalec1. - have -> : 'i%C * (Im t)%:C = Im t *: 'i%C by rewrite scalerc mulrC. + rewrite !linearD. + have <- := scalec1 (Re t). + have := scalerc (Im t) 'i%C. + rewrite mulrC => <-. rewrite !linearZ -!deriveE // -CR /= !scalerc_regular scalerA. by rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)) !scalecE mulr1. - rewrite mulrDr mulKf //; last by near:t; exact: nbhs_dnbhs_neq. + rewrite mulrDr mulKf //. + by near:t; exact: nbhs_dnbhs_neq. rewrite opprD addNKr normrN. near: t. case: littleo. move => h /= H. near=> t. - rewrite normrM normfV ltr_pdivrMl; last by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + rewrite normrM normfV ltr_pdivrMl; first by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. rewrite -!normRcomplex. rewrite [r%:num/2]gt0_normc // -rmorphM /= lecR. near: t; apply: nbhs_dnbhs; near_simpl. - by apply: H => //; rewrite -[Normc.normc _]/(`|_|) normr_gt0 //. + apply: H => //. +(* rewrite -[Normc.normc _]/(`|_|). + rewrite normr_gt0.*) admit. rewrite mulrC ltr_pM2l //. - by rewrite gtr_pMr // invf_lt1 // ?ltr1n //. - rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. -Unshelve. all: by end_near. -Qed. + by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + by rewrite gtr_pMr // invf_lt1 // ?ltr1n //. +Unshelve. all: by end_near. Admitted. Lemma diff_CR_holo (f : C -> C) (c : C): Rdifferentiable f c -> CauchyRiemannEq f c -> holomorphic f c. @@ -325,7 +331,7 @@ have lem : quotC \o *%R^~ 'i%R @ (realC @ (0 : R)^') --> l. apply: (@cvg_comp _ _ _ realC ( *%R^~ 'i)); first by exact: realC'0. rewrite -[0 in X in _ `=>` X](mul0r 'i%C). apply: within_continuous_withinNx; first by apply: mulrr_continuous. - move=> x /eqP; rewrite mul0r mulIr_eq0; last by apply/rregP; apply: neq0Ci. + move=> x /eqP; rewrite mul0r mulIr_eq0; first by apply/rregP; apply: neq0Ci. exact: eqP. have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))). by apply/cvg_ex; simpl; exists l. @@ -335,7 +341,12 @@ have ->: lim (quotR @ (realC @ ((0 : R)^'))) move=> h /=; rewrite /quotC /quotR /=. rewrite invfM mulrA (mulrC _ ('i)^-1) mulrA divff ?complexiE ?neq0Ci //. by rewrite mul1r scalecE. - move=> /funext <-. rewrite limM ?lim_cst. by []. by []. exact: cvg_cst. by []. by []. + move=> /funext <-. rewrite limM ?lim_cst. + by []. + exact: cvg_cst. + by []. + by []. + by []. suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = lim (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) by []. suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = l. From b73e7b73962ccf4436d1b4471bb761d61796259f Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 14:12:09 +0900 Subject: [PATCH 26/29] fix --- theories/holomorphy.v | 60 +++++++++++++++++++++---------------------- 1 file changed, 30 insertions(+), 30 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index defb2bf66a..d4e59e4ba8 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -1,5 +1,5 @@ -@(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From HB Require Import structures. +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. (*From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. From mathcomp Require Import ssrnat eqtype seq choice fintype bigop order. From mathcomp Require Import ssralg ssrnum ssrfun matrix complex.*) @@ -100,7 +100,7 @@ by case: x => ??; rewrite /normr/= !exprMn -mulrDr sqrtrM ?sqr_ge0// sqrtr_sqr. Qed. #[export] HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. Lemma Rcomplex_findim : Vector.axiom 2 (Rcomplex R). @@ -133,7 +133,7 @@ Variable R : realType. Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. -Local Notation Rc := (Rcomplex R). +Local Notation Rc := (Rcomplex R). Check (Rcomplex R : normedModType R). Check (Rcomplex R : vectType R). Check (Rcomplex R : normedVectType R). @@ -158,7 +158,7 @@ suff ->: (fun h : C => h^-1 * ((f (c + h) - f c))) = ((fun h : C => h^-1 * ((f \o shift c) (h *: (1 : C^o)) - f c))) by []. by apply: funext => h; rewrite complexA [X in f X]addrC. Qed. - + Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:RC. @@ -168,7 +168,7 @@ Lemma continuous_realC: continuous realC. Proof. move=> x A /= [] r /[dup] /realC_gt0 Rer0 /gt0_realC rRe H; exists (Re r) => //. by move=> z /= nz; apply: (H z%:C); rewrite /= -raddfB realC_norm rRe ltcR. -Qed. +Qed. Lemma Rdiff1 (f : C -> C) (c : C) : lim ((fun h : C => h^-1 * ((f (c + h) - f c))) @ (realC @ 0^')) @@ -203,13 +203,12 @@ Lemma Cdiff1 (f : C -> C) (c : C) : = 'D_1 (f : C^o -> C^o) c. Proof. rewrite /derive. -rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (h + c) - f c))) - @ 0^')). -suff ->: (fun h : C => h^-1 * (f (h + c) - f c)) +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (h + c) - f c))) @ 0^')). +suff ->: (fun h : C => h^-1 * (f (h + c) - f c)) = (fun h : C => h^-1 *: (( (f : C^o -> C^o) \o shift c) (h *: 1 : C^o) - f c) : C^o). by []. apply: funext => h /=. -by rewrite scalecE scaler1. +by rewrite scalecE scaler1. Qed. @@ -223,7 +222,7 @@ rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:RC)) - f c)%:RC. by []. -apply: funext => h /=. +apply: funext => h /=. by rewrite -fmorphV scalerc [X in f X]addrC scalerc. Qed. @@ -236,17 +235,17 @@ Lemma is_derive_holo (f : C -> C) (c : C) : is_derive (c : C^o) 1 (f : C^o -> C^o) ('D_1 (f%:Rfun) c%:RC). Proof. move => fdiff CR. suff lem: (h^-1 * (f (h + c) - f c) @[h --> 0^']) --> 'D_1 (f%:Rfun) (c%:RC). - split; last first. + split; last first. by rewrite -Cdiff1; apply: cvg_lim lem; by []. apply/cvg_ex. eexists. rewrite /=. under eq_fun do rewrite scaler1/=. exact: lem. -move => /= A. +move => /= A. move => [/= _ /posnumP [r]] /=; rewrite /ball_ /= => H. near_simpl. near=> t. apply: H => /=. - rewrite deriveE => //. + rewrite deriveE => //. rewrite [f _](@diff_locallyx R Rc Rc) => //=. - rewrite (ACl (1*4*2*3)) /= subrr add0r. + rewrite (ACl (1*4*2*3)) /= subrr add0r. have -> : 'd (f%:Rfun) (c%:RC) (t : Rc) = t * 'd (f%:Rfun) (c%:RC) (1: Rc). rewrite (complexE t). rewrite !linearD. @@ -257,27 +256,28 @@ move => /= A. by rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)) !scalecE mulr1. rewrite mulrDr mulKf //. by near:t; exact: nbhs_dnbhs_neq. - rewrite opprD addNKr normrN. + rewrite opprD addNKr normrN. near: t. case: littleo. - move => h /= H. - near=> t. - rewrite normrM normfV ltr_pdivrMl; first by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + move => h /= H. + near=> t. + rewrite normrM normfV ltr_pdivrMl. + by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. - rewrite -!normRcomplex. - rewrite [r%:num/2]gt0_normc // -rmorphM /= lecR. + rewrite -!normRcomplex [r%:num/2]gt0_normc // -rmorphM /= lecR. near: t; apply: nbhs_dnbhs; near_simpl. apply: H => //. -(* rewrite -[Normc.normc _]/(`|_|). - rewrite normr_gt0.*) admit. - rewrite mulrC ltr_pM2l //. - by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + rewrite -[Normc.normc _]/(`|_ : Rc|) . + by rewrite normr_gt0. + rewrite mulrC ltr_pM2l //. + by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. by rewrite gtr_pMr // invf_lt1 // ?ltr1n //. -Unshelve. all: by end_near. Admitted. +Unshelve. all: by end_near. +Qed. Lemma diff_CR_holo (f : C -> C) (c : C): Rdifferentiable f c -> CauchyRiemannEq f c -> holomorphic f c. -Proof. +Proof. by move=> /is_derive_holo /[apply] ?; exact/holomorphicP. Qed. @@ -339,9 +339,9 @@ have ->: lim (quotR @ (realC @ ((0 : R)^'))) = 'i * lim (quotC \o ( fun h => h *'i) @ (realC @ ((0 : R)^'))). have: (fun x => 'i) \* quotC \o ( fun h => h *'i) =1 quotR. move=> h /=; rewrite /quotC /quotR /=. - rewrite invfM mulrA (mulrC _ ('i)^-1) mulrA divff ?complexiE ?neq0Ci //. - by rewrite mul1r scalecE. - move=> /funext <-. rewrite limM ?lim_cst. + rewrite invfM mulrA (mulrC _ ('i)^-1) mulrA divff ?complexiE ?neq0Ci //. + by rewrite mul1r scalecE. + move=> /funext <-. rewrite limM ?lim_cst. by []. exact: cvg_cst. by []. From fdaf370561399c7ec8e6c9dfe893baba5f53f3a7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jun 2026 14:12:57 +0900 Subject: [PATCH 27/29] wip --- .nix/config.nix | 6 ++++++ config.nix | 8 ++++---- theories/derive.v | 10 ++++++---- 3 files changed, 16 insertions(+), 8 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 7c48a67da2..dd98a2ae12 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -57,6 +57,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 // { @@ -64,6 +65,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; # not yet available for 9.1 }; }; @@ -85,6 +87,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 // { @@ -92,6 +95,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; # 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; }; diff --git a/config.nix b/config.nix index 87c4d6070e..d24ae3aa68 100644 --- a/config.nix +++ b/config.nix @@ -1,6 +1,6 @@ { - coq = "8.11"; - mathcomp = "mathcomp-1.12.0"; - mathcomp-real-closed = "mkerjean/master"; - mathcomp-finmap = "1.5.1"; + coq = "9.1"; + mathcomp = "master"; + mathcomp-real-closed = "2.0.3"; + mathcomp-finmap = "2.2.3"; } diff --git a/theories/derive.v b/theories/derive.v index 6d664187ec..7ebc32fd91 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -567,12 +567,14 @@ 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 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. - rewrite fE. -rewrite addrK. +split=> [fE t|fE t]. + rewrite fE addrK. + congr (_ + _). + + admit. Admitted. Lemma exists_diff (V W: normedModType R) (f : V -> W) x: From 95f194f9436f55a249c47eab64fffcf17e4e13d3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jun 2026 14:40:12 +0900 Subject: [PATCH 28/29] admit in derive.v --- theories/derive.v | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index 7ebc32fd91..15d1a900bb 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -566,26 +566,27 @@ 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). +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 (_ + _). - - admit. -Admitted. - -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 lem : 'd f x = l :> (V -> W). - by apply:(@diff_unique V W f l x cl); exact/funext/shift_addo. -by apply/diffP => //=; split; rewrite lem => // t; rewrite norm_lim_id. + 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. From 224608d96aa15c2f300e4e3345f14c90159b33a2 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 17 Jun 2026 08:38:38 +0200 Subject: [PATCH 29/29] [CI] Test https://github.com/rocq-community/coq-nix-toolbox/pull/476 --- .github/workflows/nix-action-9.0-master.yml | 226 ++++++++++++++++++++ .github/workflows/nix-action-9.1-master.yml | 226 ++++++++++++++++++++ .github/workflows/nix-action-master.yml | 218 +++++++++++++++++++ .nix/coq-nix-toolbox.nix | 2 +- default.nix | 4 +- 5 files changed, 673 insertions(+), 3 deletions(-) diff --git a/.github/workflows/nix-action-9.0-master.yml b/.github/workflows/nix-action-9.0-master.yml index aba868db3f..6588b6e104 100644 --- a/.github/workflows/nix-action-9.0-master.yml +++ b/.github/workflows/nix-action-9.0-master.yml @@ -58,6 +58,153 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "coq" + coquelicot: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (coquelicot) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-master\" --argstr job \"coquelicot\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "coquelicot" + interval: + needs: + - coq + - coquelicot + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (interval) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-master\" --argstr job \"interval\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "bignums" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coquelicot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "coquelicot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: flocq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "flocq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "interval" mathcomp: needs: - rocq-core @@ -130,6 +277,7 @@ jobs: - rocq-core - mathcomp-reals - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -194,6 +342,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -204,6 +356,7 @@ jobs: - mathcomp-finmap - mathcomp-bigenough - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -276,6 +429,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -624,6 +781,7 @@ jobs: needs: - coq - mathcomp-analysis-stdlib + - interval runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -688,6 +846,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "mathcomp-infotheo" + mathcomp-real-closed: + needs: + - rocq-core + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-real-closed) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-real-closed" mathcomp-reals: needs: - rocq-core diff --git a/.github/workflows/nix-action-9.1-master.yml b/.github/workflows/nix-action-9.1-master.yml index 185797a8ee..86bd2b4764 100644 --- a/.github/workflows/nix-action-9.1-master.yml +++ b/.github/workflows/nix-action-9.1-master.yml @@ -58,6 +58,153 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "coq" + coquelicot: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (coquelicot) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.1-master\" --argstr job \"coquelicot\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "coquelicot" + interval: + needs: + - coq + - coquelicot + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (interval) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.1-master\" --argstr job \"interval\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "bignums" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coquelicot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "coquelicot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: flocq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "flocq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "interval" mathcomp: needs: - rocq-core @@ -130,6 +277,7 @@ jobs: - rocq-core - mathcomp-reals - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -194,6 +342,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -204,6 +356,7 @@ jobs: - mathcomp-finmap - mathcomp-bigenough - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -276,6 +429,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -624,6 +781,7 @@ jobs: needs: - coq - mathcomp-analysis-stdlib + - interval runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -688,6 +846,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "mathcomp-infotheo" + mathcomp-real-closed: + needs: + - rocq-core + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-real-closed) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.1-master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-real-closed" mathcomp-reals: needs: - rocq-core diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml index adb5918eec..bea2999924 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -117,6 +117,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "coq-elpi" + coquelicot: + needs: + - coq + - stdlib + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (coquelicot) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"master\" --argstr job \"coquelicot\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "coquelicot" hierarchy-builder: needs: - rocq-core @@ -181,6 +249,78 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "hierarchy-builder" + interval: + needs: + - coq + - coquelicot + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (interval) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"master\" --argstr job \"interval\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coquelicot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "coquelicot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "interval" mathcomp: needs: - rocq-core @@ -254,6 +394,7 @@ jobs: - rocq-core - mathcomp-reals - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -318,6 +459,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -328,6 +473,7 @@ jobs: - mathcomp-finmap - mathcomp-bigenough - mathcomp-bigenough + - mathcomp-real-closed - stdlib runs-on: ubuntu-latest steps: @@ -401,6 +547,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -746,6 +896,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-finmap" + mathcomp-real-closed: + needs: + - rocq-core + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-real-closed) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-real-closed" mathcomp-reals: needs: - rocq-core diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index e70ee2f134..70de233261 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"4a441c50de5618ef066128f9f6f84e6bc13066da" +"c119770e932f8f931877eddb284008225c9f1cd0" diff --git a/default.nix b/default.nix index ec2742873f..1d43290d34 100644 --- a/default.nix +++ b/default.nix @@ -4,8 +4,8 @@ bundle ? null, job ? null, inNixShell ? null, src ? ./., }@args: let auto = fetchGit { - url = "https://github.com/rocq-community/coq-nix-toolbox.git"; - ref = "master"; + url = "https://github.com/proux01/coq-nix-toolbox.git"; + ref = "fix530989"; rev = import .nix/coq-nix-toolbox.nix; }; in