From d4abdcb29c02a51266d2deb95ed90b2b4b87ae6d Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:15:45 +0900 Subject: [PATCH 01/30] fix --- classical/unstable.v | 130 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 129 insertions(+), 1 deletion(-) diff --git a/classical/unstable.v b/classical/unstable.v index 9d2432a9c1..7267ce0466 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,7 +1,7 @@ (* 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 matrix. +From mathcomp Require Import vector archimedean interval matrix complex. (**md**************************************************************************) (* # MathComp extra *) @@ -51,6 +51,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. Lemma sub_row_mx {V : zmodType} m n1 n2 (A1 : 'M[V]_(m, n1)) (A2 : 'M[V]_(m, n2)) @@ -677,3 +678,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 d63c33ec17f431a290ba1baa666f33fbe52580e1 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:22:44 +0900 Subject: [PATCH 02/30] 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 c97543833899b5d0829b63beea041f2fc22d223f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 May 2025 21:09:27 +0900 Subject: [PATCH 03/30] holomorphic Co-Authored-By : Reynald Affeldt Co-Authored-By : Cyril Cohen Co-Authored-By : Quentin Vermande --- .travis.yml | 31 +++ CHANGELOG_UNRELEASED.md | 46 ++++ _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, 434 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 2d85fdc0a5..e516071cf3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -192,6 +192,52 @@ - in `functions.v`: + lemmas `zerofctE`, `onefctE` +- in `unstable.v` + + lemmas `scalecE`, `normcr`, `Im_mul`, `mulrnc`, `complexA`, `normc_natmul`, + `nomrc_mulrn`, `gt0_normc`, `gt0_realC`, `ltc0E`, `ltc0P`, `ltcP`, `lecP`, + `realC_gt0`, `Creal_gtE`, `realC_norm`, `eqCr`, `eqCI`, `neqCr0`, + `real_normc_ler`, `im_normc_ler` + + notations `f %:Rfun`, `v %:Rc` + + lemmas `realCZ`, `realC_alg`, `scalecr`, `scalecV` + +- in `function_spaces.v` + + lemmas `cvg_big`, `continuous_big` + +- file `holomorphy.v` + + instance of `normedModType` on `complex` + + definition `ball_Rcomplex` + + lemmas `entourage_RcomplexE`, `normcZ`, `Rcomplex_findim` + + instance of `normedVectType` on `complex` + + definitions `holomorphic`, `Rdifferentiable`, `realC`, `CauchyRiemannEq` + + lemmas `holomorphicP`, `continuous_realC`, `Rdiff1`, `Rdiffi`, `littleoCo`, + `holo_differentiable`, `holo_CauchyRiemann`, `Diff_CR_holo`, + `holomorphic_Rdiff` + +- in `landau.v` + + lemma `littleoE0` + +- in `normed_module.v` + + structure `normedVectType` + + lemmas `dnbhs0_le`, `nbhs0_le`, `dnbrg0_lt`, `nbhs0_lt` + + definition `pseudometric` + + instance of `normedZmodType`, `pointedType` and `pseudoMetricType` + on `pseudometric` + + definitions `oo_norm`, `oo_space`, + + instance of `normedModType` on `oo_space` + + lemmas `oo_closed_ball_compact`, `equivalence_norms`, + `linear_findim_continuous` + +- in `num_topology.v` + + instance of `pseudoMetricType` on `GRing.regular` + +- in `uniform_structure` + + lemma `within_continuous_withinNx` + +- in `tvs.v` + + lemmas `cvg_sum`, `sum_continuous`, `entourage_nbhsE` + + instance of `UniformZmodule.type` on `GRing.regular` + +### Changed - in `functions.v`: + lemmas `linfunP`, `linfun_eqP` 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 1252178b3f..66142b2bc2 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -510,6 +510,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 f8ec6cb9ae..61435e3885 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 a84ea145be83aef1d2ba8a7bdba3d518dd1e060e Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:48:37 +0900 Subject: [PATCH 04/30] 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 66142b2bc2..a3612ddca9 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2590,6 +2590,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 bc655c930397982bee25b387731d04b578cf6160 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 14:50:38 +0900 Subject: [PATCH 05/30] 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 6c34d3f4e82dcf29638e1e48b785c6d35e864257 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 15:01:00 +0900 Subject: [PATCH 06/30] 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 8ed72df10a4afefdbb2a32035d6b8c12550e043e Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 15:04:19 +0900 Subject: [PATCH 07/30] 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 bcc74b693d2272474e7b3928dbd71e557b4734b1 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 16:09:30 +0900 Subject: [PATCH 08/30] 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 075796d8fa7bb91fdc68468cd0ac44372e5680ed Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 16:16:20 +0900 Subject: [PATCH 09/30] 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 d72ea42b95e34f9ce60c1c7c1ecaea2c0a04db8b Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 4 Jun 2026 22:55:34 +0900 Subject: [PATCH 10/30] 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 12373f2d7aa16beb7f88d4ad56c7c33e9d7c2031 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 10:45:12 +0900 Subject: [PATCH 11/30] 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 79b478d47a8c1fc8bb3353a3ec20a452a8a88b61 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 12:11:10 +0900 Subject: [PATCH 12/30] 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 61435e3885..4bde48531d 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 2d3eb4bfbeafbdba650d69f33668b99d7031ce94 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 12:15:38 +0900 Subject: [PATCH 13/30] 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 7267ce0466..e8aa6a5153 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -692,6 +692,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 4bde48531d..87a63c592f 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 5b0c3c1533d28b8ce6f23925cbe5e14d6a387168 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 16:41:46 +0900 Subject: [PATCH 14/30] exists diff --- theories/derive.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index 07a7aa7cab..f710f0f51b 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 a28cbef1c886594485c921e03deca9ec9640cfdd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 16:41:52 +0900 Subject: [PATCH 15/30] 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 0e0c84fce84f00c199503e0912de0dee2542d585 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 16:42:12 +0900 Subject: [PATCH 16/30] 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 a3612ddca9..955229e4c0 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2643,6 +2643,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 e38614a117eb0dc4b349c822254ae5cf46ddec2d Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 5 Jun 2026 21:58:19 +0900 Subject: [PATCH 17/30] 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 0e36f9c9f03ef22fd65af26dfb78afea27d797fd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 11 Jun 2026 10:26:53 +0900 Subject: [PATCH 18/30] 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 69f559350061469346a06b555c5ee58112eb8f03 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 11 Jun 2026 14:42:26 +0900 Subject: [PATCH 19/30] 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 f710f0f51b..751f1e17d3 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 662712de053c3e979309dfb8b6cba68ea5375f7d Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 11 Jun 2026 18:24:30 +0900 Subject: [PATCH 20/30] 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 f969a230309d637224329eaaa86e73309838ff9d Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 11:35:42 +0900 Subject: [PATCH 21/30] 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 2beb11f2ae7740ef0f45617dad9e8d74eefe4993 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 15:56:06 +0900 Subject: [PATCH 22/30] 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 3a6436c37cf8b1d7c7ff70461098af06524452ab Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 16:52:32 +0900 Subject: [PATCH 23/30] 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 e8aa6a5153..4eedb46100 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -679,6 +679,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. @@ -689,10 +698,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. @@ -779,35 +789,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 3f57c52fde1ecf1036759c95c9474079ea077e81 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 12 Jun 2026 17:06:06 +0900 Subject: [PATCH 24/30] wip shiftaddo --- theories/derive.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index 751f1e17d3..cbd00dee4c 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 b52b1c4136d9f151abd7891b8e33571068a79333 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jun 2026 13:57:32 +0900 Subject: [PATCH 25/30] 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 6e993fb01612eac84ff64356cb507ee10be8f5c6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 14:12:09 +0900 Subject: [PATCH 26/30] 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 db9b0cd1446f30b133dae3430395d4288763ab99 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jun 2026 14:12:57 +0900 Subject: [PATCH 27/30] 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 cbd00dee4c..309eb4f4c2 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 00c0f9a8f1ad3317c4af31afddba731c0937fb87 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jun 2026 14:40:12 +0900 Subject: [PATCH 28/30] 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 309eb4f4c2..cda1a47e4a 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 81905498750d5beea0ac92ecfa69700905f603a3 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 17 Jun 2026 08:38:38 +0200 Subject: [PATCH 29/30] [CI] Test https://github.com/rocq-community/coq-nix-toolbox/pull/476 --- .github/workflows/nix-action-9.0-master.yml | 78 +++++++++++++++++++++ .github/workflows/nix-action-9.1-master.yml | 78 +++++++++++++++++++++ .github/workflows/nix-action-master.yml | 78 +++++++++++++++++++++ .nix/config.nix | 2 - .nix/coq-nix-toolbox.nix | 2 +- .travis.yml | 31 -------- config.nix | 6 -- default.nix | 4 +- opam | 41 ----------- 9 files changed, 237 insertions(+), 83 deletions(-) delete mode 100644 .travis.yml delete mode 100644 config.nix delete mode 100644 opam diff --git a/.github/workflows/nix-action-9.0-master.yml b/.github/workflows/nix-action-9.0-master.yml index aba868db3f..6caa1aa79b 100644 --- a/.github/workflows/nix-action-9.0-master.yml +++ b/.github/workflows/nix-action-9.0-master.yml @@ -130,6 +130,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 +195,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 +209,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 +282,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 @@ -688,6 +698,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..3e3aaf9bfb 100644 --- a/.github/workflows/nix-action-9.1-master.yml +++ b/.github/workflows/nix-action-9.1-master.yml @@ -130,6 +130,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 +195,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 +209,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 +282,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 @@ -688,6 +698,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..0b948625f4 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -254,6 +254,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 +319,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 +333,7 @@ jobs: - mathcomp-finmap - mathcomp-bigenough - mathcomp-bigenough + - mathcomp-real-closed - stdlib runs-on: ubuntu-latest steps: @@ -401,6 +407,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 +756,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/config.nix b/.nix/config.nix index dd98a2ae12..aa747f8ba6 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -8,8 +8,6 @@ let mathcomp-analysis-stdlib.job = true; ssprove.override.version = "main"; mathcomp-infotheo.override.version = "master"; - interval.override.version = "master"; - coquelicot.override.version = "master"; }; in { ## DO NOT CHANGE THIS diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index e70ee2f134..22d1f20ff4 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"4a441c50de5618ef066128f9f6f84e6bc13066da" +"ed23062e563f0fbe6c27877bad88426c7f0dc9c9" diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 6df16b626c..0000000000 --- a/.travis.yml +++ /dev/null @@ -1,31 +0,0 @@ -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/config.nix b/config.nix deleted file mode 100644 index d24ae3aa68..0000000000 --- a/config.nix +++ /dev/null @@ -1,6 +0,0 @@ -{ - coq = "9.1"; - mathcomp = "master"; - mathcomp-real-closed = "2.0.3"; - mathcomp-finmap = "2.2.3"; -} 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 diff --git a/opam b/opam deleted file mode 100644 index e9bd5838b0..0000000000 --- a/opam +++ /dev/null @@ -1,41 +0,0 @@ -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" -] From d927ca50e05fdf67e4aad13457f5b7ad678b1e46 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 17 Jun 2026 13:32:03 +0200 Subject: [PATCH 30/30] Classical doesn't depend on real-closed --- _CoqProject | 3 + classical/unstable.v | 138 +----------------------------- theories/Make | 3 + theories/holomorphy.v | 2 +- theories/unstable_analysis.v | 157 +++++++++++++++++++++++++++++++++++ 5 files changed, 165 insertions(+), 138 deletions(-) create mode 100644 theories/unstable_analysis.v diff --git a/_CoqProject b/_CoqProject index 7cb8c5bda7..d9454144e8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -42,6 +42,8 @@ experimental_reals/distr.v reals_stdlib/Rstruct.v reals_stdlib/nsatz_realtype.v +theories/unstable_analysis.v + theories/ereal.v theories/landau.v @@ -150,6 +152,7 @@ theories/charge.v theories/kernel.v theories/pi_irrational.v theories/gauss_integral.v +theories/holomorphy.v theories/all_analysis.v diff --git a/classical/unstable.v b/classical/unstable.v index 4eedb46100..9d2432a9c1 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,7 +1,7 @@ (* 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 matrix complex. +From mathcomp Require Import vector archimedean interval matrix. (**md**************************************************************************) (* # MathComp extra *) @@ -51,7 +51,6 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. -Local Open Scope complex_scope. Local Open Scope ring_scope. Lemma sub_row_mx {V : zmodType} m n1 n2 (A1 : 'M[V]_(m, n1)) (A2 : 'M[V]_(m, n2)) @@ -678,138 +677,3 @@ End Theory. Module Import Exports. HB.reexport. End Exports. End Norm. Export Norm.Exports. - - -Notation "f %:Rfun" := - (f : (Rcomplex _) -> (Rcomplex _)) - (at level 5, format "f %:Rfun") : complex_scope. - -Notation "v %:RC" := (v : (Rcomplex _)) - (at level 5, format "v %:RC") : complex_scope. - - -(* TODO: backport to real-closed *) -Section complex_extras. -Variable R : rcfType. -Local Notation sqrtr := Num.sqrt. -Local Notation C := (Rcomplex R). - -Import Normc. -Import Num.Def. -Import complex. - -(*TODO : rename scale regular and put there*) -Lemma scalecE (w v: C^o) : v *: w = v * w. -Proof. by []. Qed. - -Lemma scalerc (h : R) (c : C) : h *: (c : Rcomplex R) = h%:C * c. -Proof. -case : c => x y. -by rewrite /(real_complex _) /(_ *: _) /( _ * _) /= /= /scalec !mul0r subr0 addr0. -Qed. - -(* FIXME: unused *) -Lemma normcr (x : R) : normc (x%:C) = normr x. -Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. - -Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. -Proof. by simpc. Qed. - -Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). -Proof. -by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx. -Qed. - -Lemma complexA (h : C^o) : h%:A = h. -Proof. by rewrite scalecE mulr1. Qed. - -Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R. -Proof. by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr normr_nat. Qed. - -Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k. -Proof. -by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul. -Qed. - -Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C. -Proof. -case: r => x y /= /andP[] /eqP -> x0. -by rewrite expr0n addr0 sqrtr_sqr gtr0_norm. -Qed. - -Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C. -Proof. by case: r => x y /andP[] /eqP -> _. Qed. - -Lemma ltc0E (k : R): (0 < k%:C) = (0 < k). -Proof. by simpc. Qed. - -Lemma ltc0P (k : R): (0 < k%:C) <-> (0 < k). -Proof. by simpc. Qed. - -Lemma ltcP (k t: R): (t%:C < k%:C) <-> (t < k). -Proof. by simpc. Qed. - -Lemma lecP (k t: R): (t%:C <= k%:C) <-> (t <= k). -Proof. by simpc. Qed. - -(* (*TBA algC *) *) -Lemma realC_gt0 (d : C) : 0 < d -> (0 < Re d :> R). -Proof. by rewrite ltcE => /andP [] //. Qed. - -Lemma Creal_gtE (c d : C) : c < d -> (complex.Re c < complex.Re d). -Proof. by rewrite ltcE => /andP [] //. Qed. - -Lemma realC_norm (b : R) : `|b%:C| = `|b|%:C. -Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed. - -Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). -Proof. exact: (inj_eq (@complexI _)). Qed. - -Lemma eqCI (r s : R) : (r *i == s *i) = (r == s). -Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed. - -Lemma neqCr0 (r : R) : (r%:C != 0) = (r != 0). -Proof. by apply/negP/negP; rewrite ?eqCr. Qed. - -Lemma real_normc_ler (x : C) : - `|Re x| <= normc x. -Proof. -case: x => x y /=. -rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. -rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. -by rewrite lerDl ?sqr_ge0. -Qed. - -Lemma im_normc_ler (x : C) : - `|Im x| <= normc x. -Proof. -case: x => x y /=. -rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. -rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. -by rewrite lerDr ?sqr_ge0. -Qed. - -Lemma realC_alg (a : R) : a *: (1%:RC) = a%:C. -Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed. - -Lemma scalecV (h: R) (v: Rcomplex R): - h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *) -Proof. -by move=> h0 v0; rewrite scalerc invrM // ?unitfE ?eqCr // mulrC scalerc fmorphV. -Qed. - - -(* TODO: clean lemmas about scalec *) -Lemma scalerc_regular (h : R) (c : R[i]): h *: (c : Rcomplex R) = h%:C *: (c : C^o). -Proof. -by rewrite scalecE scalerc. -Qed. - -Lemma scalec1 (h : R) : h *: (1 : C^o) = h%:C. -Proof. -by rewrite scalerc mulr1. -Qed. - - -End complex_extras. - diff --git a/theories/Make b/theories/Make index 17da83d2a3..72add687e1 100644 --- a/theories/Make +++ b/theories/Make @@ -9,6 +9,8 @@ # introduced in Rocq 9.3 -arg -w -arg -rewrite-rw +unstable_analysis.v + ereal.v landau.v @@ -118,3 +120,4 @@ pi_irrational.v gauss_integral.v all_analysis.v showcase/summability.v +holomorphy.v diff --git a/theories/holomorphy.v b/theories/holomorphy.v index d4e59e4ba8..ef0cf407a6 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -4,7 +4,7 @@ From HB Require Import structures. From mathcomp Require Import ssrnat eqtype seq choice fintype bigop order. 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 unstable_analysis boolp reals ereal derive. From mathcomp Require Import classical_sets functions interval_inference. From mathcomp Require Import topology normedtype landau. diff --git a/theories/unstable_analysis.v b/theories/unstable_analysis.v new file mode 100644 index 0000000000..ef68b32b13 --- /dev/null +++ b/theories/unstable_analysis.v @@ -0,0 +1,157 @@ +(* 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 complex. +From mathcomp.classical Require Export unstable. + +(**md**************************************************************************) +(* # MathComp extra *) +(* *) +(* This files contains lemmas that should eventually be backported *) +(* to mathcomp. These lemmas may change before being backported to mathcomp, *) +(* don't use anything in this file outside of Analysis. For this same reason, *) +(* nothing in this file should be mentionned in the changelog. *) +(* Once a result is backported to mathcomp, please move it to mathcomp_extra.v*) +(* and mention it in the changelog. *) +(******************************************************************************) + +Attributes warn(note="The unstable_analysis.v file should only be used inside analysis.", + cats="internal-analysis"). + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Theory. +Local Open Scope complex_scope. +Local Open Scope ring_scope. + +Notation "f %:Rfun" := (f : (Rcomplex _) -> (Rcomplex _)) + (at level 5, format "f %:Rfun") : complex_scope. + +Notation "v %:RC" := (v : (Rcomplex _)) + (at level 5, format "v %:RC") : complex_scope. + +(* TODO: backport to real-closed *) +Section complex_extras. +Variable R : rcfType. +Local Notation sqrtr := Num.sqrt. +Local Notation C := (Rcomplex R). + +Import Normc. +Import Num.Def. +Import complex. + +(*TODO : rename scale regular and put there*) +Lemma scalecE (w v: C^o) : v *: w = v * w. +Proof. by []. Qed. + +Lemma scalerc (h : R) (c : C) : h *: (c : Rcomplex R) = h%:C * c. +Proof. +case : c => x y. +by rewrite /(real_complex _) /(_ *: _) /( _ * _) /= /= /scalec !mul0r subr0 addr0. +Qed. + +(* FIXME: unused *) +Lemma normcr (x : R) : normc (x%:C) = normr x. +Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + +Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. +Proof. by simpc. Qed. + +Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). +Proof. +by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx. +Qed. + +Lemma complexA (h : C^o) : h%:A = h. +Proof. by rewrite scalecE mulr1. Qed. + +Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R. +Proof. by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr normr_nat. Qed. + +Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k. +Proof. +by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul. +Qed. + +Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C. +Proof. +case: r => x y /= /andP[] /eqP -> x0. +by rewrite expr0n addr0 sqrtr_sqr gtr0_norm. +Qed. + +Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C. +Proof. by case: r => x y /andP[] /eqP -> _. Qed. + +Lemma ltc0E (k : R): (0 < k%:C) = (0 < k). +Proof. by simpc. Qed. + +Lemma ltc0P (k : R): (0 < k%:C) <-> (0 < k). +Proof. by simpc. Qed. + +Lemma ltcP (k t: R): (t%:C < k%:C) <-> (t < k). +Proof. by simpc. Qed. + +Lemma lecP (k t: R): (t%:C <= k%:C) <-> (t <= k). +Proof. by simpc. Qed. + +(* (*TBA algC *) *) +Lemma realC_gt0 (d : C) : 0 < d -> (0 < Re d :> R). +Proof. by rewrite ltcE => /andP [] //. Qed. + +Lemma Creal_gtE (c d : C) : c < d -> (complex.Re c < complex.Re d). +Proof. by rewrite ltcE => /andP [] //. Qed. + +Lemma realC_norm (b : R) : `|b%:C| = `|b|%:C. +Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed. + +Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). +Proof. exact: (inj_eq (@complexI _)). Qed. + +Lemma eqCI (r s : R) : (r *i == s *i) = (r == s). +Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed. + +Lemma neqCr0 (r : R) : (r%:C != 0) = (r != 0). +Proof. by apply/negP/negP; rewrite ?eqCr. Qed. + +Lemma real_normc_ler (x : C) : + `|Re x| <= normc x. +Proof. +case: x => x y /=. +rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. +by rewrite lerDl ?sqr_ge0. +Qed. + +Lemma im_normc_ler (x : C) : + `|Im x| <= normc x. +Proof. +case: x => x y /=. +rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. +by rewrite lerDr ?sqr_ge0. +Qed. + +Lemma realC_alg (a : R) : a *: (1%:RC) = a%:C. +Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed. + +Lemma scalecV (h: R) (v: Rcomplex R): + h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *) +Proof. +by move=> h0 v0; rewrite scalerc invrM // ?unitfE ?eqCr // mulrC scalerc fmorphV. +Qed. + +(* TODO: clean lemmas about scalec *) +Lemma scalerc_regular (h : R) (c : R[i]): h *: (c : Rcomplex R) = h%:C *: (c : C^o). +Proof. +by rewrite scalecE scalerc. +Qed. + +Lemma scalec1 (h : R) : h *: (1 : C^o) = h%:C. +Proof. +by rewrite scalerc mulr1. +Qed. + +End complex_extras.