From 995493d1118bc4796a5c62ae029de85a04d2d787 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 May 2025 21:09:27 +0900 Subject: [PATCH 01/10] pseudometric alias --- theories/normedtype_theory/normed_module.v | 99 ++++++++++++++++++++++ 1 file changed, 99 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index edeccb19c2..1fdc463cd1 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1961,3 +1961,102 @@ by rewrite interior_closed_ballE //; exact: ballxx. Qed. End Closed_Ball_normedModType. + +(* equip a normedZmodType with a structure of normed module *) + +Definition pseudometric (K : realType) (M : normedZmodType K) : Type := M. + +HB.instance Definition _ (K : realType) (M : normedZmodType K) := + Choice.on (pseudometric M). +HB.instance Definition _ (K : realType) (M : normedZmodType K) := + Num.NormedZmodule.on (pseudometric M). +HB.instance Definition _ (K : realType) (M : normedZmodType K) := + isPointed.Build M 0. + +Section isnormedmodule. +Variables (K : realType) (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 -[z](subrK y) -addrA. (le_lt_trans (ler_normD _ _))// addrC ltrD.*) +Admitted. + +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. + +HB.factory Record Lmodule_isNormed (R : realType) M + of GRing.Lmodule R M := { + norm : M -> R; + ler_normD : forall x y, norm (x + y) <= norm x + norm y ; +(* normrMn : forall x n, norm (x *+ n) = norm x *+ n ;*) + normrN : forall x, norm (- x) = norm x ; + normrZ : forall (l : R) (x : M), norm (l *: x) = `|l| * norm x ; + normr0_eq0 : forall x : M, norm x = 0 -> x = 0 +}. + +HB.builders Context R M of Lmodule_isNormed R M. + +HB.about Num.Zmodule_isNormed.Build. + +Lemma normrMn x n : norm (x *+ n) = norm x *+ n. +Admitted. (* from normrZ *) + +HB.instance Definition _ := Num.Zmodule_isNormed.Build + R M ler_normD normr0_eq0 normrMn normrN. + +Check M : normedZmodType R. + +Check (@pseudometric R M). + +HB.saturate pseudometric. + +Check (pseudometric M : pseudoMetricType R). + +HB.instance Definition _ := PseudoMetric.copy M (pseudometric M). +HB.instance Definition _ := isPointed.Build M 0. + +Lemma whatever : NormedZmod_PseudoMetric_eq R M. +Proof. +by constructor. +Qed. + +HB.instance Definition _ := whatever. + +Lemma coucou : PseudoMetricNormedZmod_Lmodule_isNormedModule R M. +Proof. +constructor. +exact: normrZ. +Qed. + +HB.instance Definition _ := coucou. + +Check M : normedModType R. + +HB.end. From 6f33a23fd256dcb8194589bfc15170b3398c5e3b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 May 2025 21:30:02 +0900 Subject: [PATCH 02/10] realType -> numFieldType --- theories/normedtype_theory/normed_module.v | 47 ++++++++++++---------- 1 file changed, 25 insertions(+), 22 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 1fdc463cd1..c985b0faa3 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1964,17 +1964,17 @@ End Closed_Ball_normedModType. (* equip a normedZmodType with a structure of normed module *) -Definition pseudometric (K : realType) (M : normedZmodType K) : Type := M. +Definition pseudometric (K : numFieldType) (M : normedZmodType K) : Type := M. -HB.instance Definition _ (K : realType) (M : normedZmodType K) := +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := Choice.on (pseudometric M). -HB.instance Definition _ (K : realType) (M : normedZmodType K) := +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := Num.NormedZmodule.on (pseudometric M). -HB.instance Definition _ (K : realType) (M : normedZmodType K) := +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := isPointed.Build M 0. Section isnormedmodule. -Variables (K : realType) (M' : normedZmodType K). +Variables (K : numFieldType) (M' : normedZmodType K). Notation M := (pseudometric M'). @@ -2000,8 +2000,9 @@ 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 -[z](subrK y) -addrA. (le_lt_trans (ler_normD _ _))// addrC ltrD.*) -Admitted. +rewrite -[x](subrK y) -(addrA (x + _)). +by rewrite (le_lt_trans (ler_normD _ _))// ltrD. +Qed. Local Lemma entourageE : ent = entourage_ ball. Proof. by []. Qed. @@ -2011,7 +2012,7 @@ HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K M End isnormedmodule. -HB.factory Record Lmodule_isNormed (R : realType) M +HB.factory Record Lmodule_isNormed (R : numFieldType) M of GRing.Lmodule R M := { norm : M -> R; ler_normD : forall x y, norm (x + y) <= norm x + norm y ; @@ -2023,10 +2024,14 @@ HB.factory Record Lmodule_isNormed (R : realType) M HB.builders Context R M of Lmodule_isNormed R M. -HB.about Num.Zmodule_isNormed.Build. +(*HB.about Num.Zmodule_isNormed.Build.*) Lemma normrMn x n : norm (x *+ n) = norm x *+ n. -Admitted. (* from normrZ *) +Proof. +have := normrZ n%:R x. +rewrite ger0_norm// mulr_natl => <-. +by rewrite scaler_nat. +Qed. HB.instance Definition _ := Num.Zmodule_isNormed.Build R M ler_normD normr0_eq0 normrMn normrN. @@ -2035,27 +2040,25 @@ Check M : normedZmodType R. Check (@pseudometric R M). -HB.saturate pseudometric. +(*HB.saturate pseudometric.*) Check (pseudometric M : pseudoMetricType R). HB.instance Definition _ := PseudoMetric.copy M (pseudometric M). HB.instance Definition _ := isPointed.Build M 0. -Lemma whatever : NormedZmod_PseudoMetric_eq R M. -Proof. -by constructor. -Qed. +Local Lemma NormedZmod_PseudoMetric_eq_pseudometric + : NormedZmod_PseudoMetric_eq R M. +Proof. by constructor. Qed. -HB.instance Definition _ := whatever. +HB.instance Definition _ := NormedZmod_PseudoMetric_eq_pseudometric. -Lemma coucou : PseudoMetricNormedZmod_Lmodule_isNormedModule R M. -Proof. -constructor. -exact: normrZ. -Qed. +Lemma PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric + : PseudoMetricNormedZmod_Lmodule_isNormedModule R M. +Proof. by constructor; exact: normrZ. Qed. -HB.instance Definition _ := coucou. +HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric. Check M : normedModType R. From a227a79ad2c1a65817fe62442575edec2409d952 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 May 2025 21:34:00 +0900 Subject: [PATCH 03/10] recover saturate --- theories/normedtype_theory/normed_module.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index c985b0faa3..0ffaa69c57 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2040,7 +2040,7 @@ Check M : normedZmodType R. Check (@pseudometric R M). -(*HB.saturate pseudometric.*) +HB.saturate pseudometric. Check (pseudometric M : pseudoMetricType R). From 4ae3947e37d413dcf5909c9974544bf167c269cc Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 4 May 2020 17:54:48 +0200 Subject: [PATCH 04/10] Mathcomp analysis now depends on real-closed - fixed opam - fixed nix co-authored-by: Reynald Affeldt --- .travis.yml | 31 +++++++++++++++++++++++++++++++ opam | 41 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 72 insertions(+) create mode 100644 .travis.yml create mode 100644 opam 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/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" +] From 283466947152d9e6f8da77393cbdfa328e34b2c4 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Sep 2019 13:37:23 +0200 Subject: [PATCH 05/10] holomorphic Co-Authored-By : Reynald Affeldt Co-Authored-By : Cyril Cohen --- _CoqProject | 1 + config.nix | 6 + theories/holomorphy.v | 636 ++++++++++++++++++++++++++++++++++++++++++ theories/landau.v | 5 + 4 files changed, 648 insertions(+) create mode 100644 config.nix create mode 100644 theories/holomorphy.v diff --git a/_CoqProject b/_CoqProject index 4bd2a3f29c..9bd30d25ba 100644 --- a/_CoqProject +++ b/_CoqProject @@ -97,6 +97,7 @@ theories/forms.v theories/derive.v theories/measure.v theories/numfun.v +theories/holomorphy.v theories/lebesgue_integral_theory/simple_functions.v theories/lebesgue_integral_theory/lebesgue_integral_definition.v 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/theories/holomorphy.v b/theories/holomorphy.v new file mode 100644 index 0000000000..48b6b094d7 --- /dev/null +++ b/theories/holomorphy.v @@ -0,0 +1,636 @@ + +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(*Require Import ssrsearch.*) +From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. +From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum ssrfun. +From mathcomp Require Import complex. +From mathcomp Require Import boolp reals ereal derive. +Require Import classical_sets posnum topology normedtype landau. + +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. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(* I need to import ComplexField to use its lemmas on RComplex, +I don't want the canonical lmodtype structure on C, +Therefore this is based on a fork of real-closed *) + +Section complex_extras. +Variable R : rcfType. +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. + +(*Adapting lemma eq_complex from complex.v, which was done in boolean style*) +Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). +Proof. +move=> [a b] [c d]; apply : propositional_extensionality ; split. +by move=> -> ; split. +by case=> //= -> ->. +Qed. + +Lemma Re0 : Re 0 = 0 :> R. +Proof. by []. Qed. + +Lemma Im0 : Im 0 = 0 :> R. +Proof. by []. Qed. + +Lemma ReIm_eq0 (x : C) : (x = 0) = ((Re x = 0) /\ (Im x = 0)). +Proof. by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. Qed. + +Lemma scalei_muli (z : C^o) : 'i * z = 'i *: z. +Proof. by []. Qed. + +Lemma iE : 'i%C = 'i :> C. +Proof. by []. Qed. + +Lemma scalecM : forall (w v : C^o), (v *: w = v * w). +Proof. by []. Qed. + +Lemma normc0 : normc 0 = 0 :> R . +Proof. by rewrite /normc //= expr0n //= add0r sqrtr0. Qed. + +Lemma normcN (x : C) : normc (- x) = normc x. +Proof. by case: x => a b /=; rewrite 2!sqrrN. Qed. + +Lemma normcr (x : R) : normc (x%:C) = normr x. +Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + +Lemma normcR (x : C) : (normc x)%:C = normr x. +Proof. by rewrite /normr /=. Qed. + +Lemma normc_i (x : R) : normc (x*i) = normr x. +Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. + +Lemma normc1 : normc (1 ) = 1 :> R. +Proof. by rewrite /normc/= expr0n addr0 expr1n sqrtr1. Qed. + +Lemma normcN1 : normc (-1%:C) = 1 :> R. +Proof. by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. Qed. + + +Lemma realCD (x y : R) : (x + y)%:C = x%:C + y%:C. +Proof. +(*realC_additive*) +rewrite -!complexr0 eqE_complex //=; by split; last by rewrite addr0. +Qed. + +Lemma realCB (x y : R) : (x - y)%:C = x%:C - y%:C. +Proof. +by rewrite -!complexr0 eqE_complex //=; split; rewrite ?subr0. +Qed. + +Lemma Inv_realC (x : R) : x%:C^-1 = (x^-1)%:C. +Proof. +have [/eqP->|x0] := boolP (x == 0); first by rewrite !invr0. +apply/eqP; rewrite eq_complex /= mul0r oppr0 eqxx andbT expr0n addr0. +by rewrite expr2 invrM ?unitfE // mulrA divrr ?unitfE // div1r. +Qed. + +Lemma CimV : ('i%C)^-1 = (-1 *i) :> C. +Proof. by rewrite complexiE invCi. Qed. + +Lemma invcM (x y : C) : (x * y)^-1 = x^-1 * y^-1. +Proof. +have [/eqP->|x0] := boolP (x == 0); first by rewrite !(invr0,mul0r). +have [/eqP->|y0] := boolP (y == 0); first by rewrite !(invr0,mulr0). +by rewrite invrM // mulrC. +Qed. + +Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. +Proof. by simpc. Qed. + +Lemma normcD (x y : C) : normc (x + y) <= normc x + normc y. +Proof. by rewrite -lecR realCD; apply: lec_normD. Qed. + +Lemma normc_ge0 (x : C) : 0 <= normc x. +Proof. case: x => ? ?; exact: sqrtr_ge0. Qed. + +Lemma normc_gt0 (v : C) : (0 < normc v) = (v != 0). +Proof. +rewrite lt_neqAle normc_ge0 andbT; apply/idP/idP; apply/contra. +by move/eqP ->; rewrite normc0. +by rewrite eq_sym => /eqP/eq0_normc ->. +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 realCM (a b :R) : a%:C * b%:C = (a * b)%:C. +Proof. by rewrite eqE_complex /= !mulr0 mul0r addr0 subr0. Qed. + +Lemma complexA: forall (h : C^o), h%:A = h. +Proof. by move => h; rewrite scalecM mulr1. Qed. + +Lemma lecM (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 normc_natmul (k : nat) : normc k%:R = k%:R :> R. +Proof. +by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr ger0_norm // ler0n. +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. +move=> r0; have rr : r \is Num.real by rewrite realE (ltW r0). +rewrite /normc (complexE r) /=; simpc. +rewrite (ger0_Im (ltW r0)) expr0n addr0 sqrtr_sqr gtr0_norm ?complexr0 //. +by move: r0; rewrite {1}(complexE r) /=; simpc => /andP[/eqP]. +Qed. + +Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C. +Proof. +by move=> r0; rewrite eqE_complex /=; split; last by apply: ger0_Im; apply: ltW. +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. + +Lemma complex_pos (r : {posnum C}) : 0 < (Re r%:num). +Proof. by rewrite -ltc0E -gt0_realC. 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. rewrite ltcE => /andP [] //. Qed. + +Canonical complex_Re_posnum (x : {posnum C}) := PosNum (complex_pos x). + +Lemma realC_pos_gt0 (r : {posnum R}) : 0 < (r%:num)%:C. +Proof. by rewrite ltcR. Qed. + +Canonical realC_posnum (x : {posnum R}) := PosNum (realC_pos_gt0 x). + +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 realCV (*name ?*) (h: R) : h != 0 -> (h^-1)%:C = h%:C^-1. +Proof. +rewrite eqE_complex //=; split; last by rewrite mul0r oppr0. +by rewrite expr0n //= addr0 -exprVn expr2 mulrA mulrV ?unitfE ?mul1r //=. +Qed. + + +Lemma real_normc_ler (x y : R) : + `|x| <= normc (x +i* y). +Proof. +rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=; last by apply: num_real. +by rewrite ler_addl ?sqr_ge0. +Qed. + +Lemma im_normc_ler (x y : R) : + `|y| <= normc (x +i* y). +Proof. +rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=; last by apply: num_real. +by rewrite ler_addr ?sqr_ge0. +Qed. + +End complex_extras. + +Section Rcomplex. + + +Canonical Rcomplex_lmodType (R : rcfType) := + LmodType R (Rcomplex R) (complex_real_lmodMixin R). + +Lemma scalecAl (R : rcfType) (h : R) (x y : Rcomplex R) : h *: (x * y) = h *: x * y. +Proof. +by move: h x y => h [a b] [c d]; simpc; rewrite -!mulrA -mulrBr -mulrDr. +Qed. + + +Canonical Rcomplex_lalgType (R : rcfType) := LalgType R (Rcomplex R) (@scalecAl R). + +Definition Rcomplex_normedZmodMixin (R: realType) := + @Num.NormedMixin R (Rcomplex_zmodType R) _ _ (@normcD R) (@eq0_normc R) + (@normc_mulrn R) (@normcN R). + +Canonical Rcomplex_normedZmodType (R: realType) := + NormedZmodType R (Rcomplex R) (Rcomplex_normedZmodMixin R). + +Definition Rcomplex_pseudoMetricMixin (R: realType) := + (@pseudoMetric_of_normedDomain R (Rcomplex_normedZmodType R)). + + +Canonical Rcomplex_pointedType (R: realType) := + [pointedType of (Rcomplex R) for [pointedType of R[i]^o]]. + +Canonical Rcomplex_filteredType (R: realType) := + [filteredType (Rcomplex R) of (Rcomplex R) for [filteredType R[i]^o of R[i]^o]]. + +Canonical Rcomplex_topologicalType (R: realType) := + [topologicalType of (Rcomplex R) for [topologicalType of R[i]^o]]. + +Program Definition Rcomplex_uniformMixin (R: realType): + Uniform.mixin_of (nbhs (U := Rcomplex R) ) := + (@UniformMixin (Rcomplex R) (nbhs (U := Rcomplex R)) + (entourage_ ((ball_ (@normc R)))) _ _ _ _ _). +Obligation 1. Admitted. +Obligation 2. Admitted. +Obligation 3. Admitted. +Obligation 4. Admitted. +Obligation 5. +move => R; rewrite /nbhs /= /nbhs_ /nbhs_ball_ /filter_from /entourage_ /= /filter_from /=. +apply/funext => x //=. +apply/funext => P /=; rewrite propeqE; split. + move => [r /[dup] /realC_gt0 r0 /gt0_realC rr] H. + rewrite /entourage_ /filter_from /=. + exists (fun xy => (normc ( xy.1 - xy.2) < Re r)). + exists (Re r) => //. + by move=> z /= h; apply: (H z); rewrite /= rr ltcR. +move => [B [] r r0] H /= H'; exists r%:C; first by rewrite ltcR. +move => z h; apply: H' => /=; apply: H => /=. +by rewrite -ltcR /=. +Qed. + +Canonical Rcomplex_uniformType (R: realType) := + UniformType (Rcomplex R) (Rcomplex_uniformMixin R). + +Canonical Rcomplex_pseudoMetricType (R: realType) := + PseudoMetricType (Rcomplex R) (Rcomplex_pseudoMetricMixin R). + + +Lemma Rcomplex_ball_ball_ (R: realType): + @ball _ (Rcomplex_pseudoMetricType R ) = ball_ (fun x => `| x |). +Proof. by []. Qed. + +Definition Rcomplex_pseudoMetricNormedZmodMixin (R: realType):= + PseudoMetricNormedZmodule.Mixin (Rcomplex_ball_ball_ (R: realType)). + +Canonical Rcomplex_pseudoMetricNormedZmodType (R: realType) := + PseudoMetricNormedZmodType R (Rcomplex R) + (Rcomplex_pseudoMetricNormedZmodMixin R). + +Lemma RnormcZ (R: realType) (l : R) : forall (x : Rcomplex R), + normc (l *: x) = `|l| * (normc x). +Proof. +by case=> ? ?; rewrite /normc //= !exprMn -mulrDr sqrtrM ?sqr_ge0 // sqrtr_sqr. +Qed. + +Definition Rcomplex_normedModMixin (R: realType):= + @NormedModMixin R (Rcomplex_pseudoMetricNormedZmodType R) _ (@RnormcZ R). + +Canonical Rcomplex_normedModType (R: realType):= + NormedModType R (Rcomplex R) (Rcomplex_normedModMixin R). + +End Rcomplex. + + +Lemma filter_compE ( T U V : topologicalType) + (f : T -> U) (g : V -> T) + (F : set ( set V)) : + (f @ (g @ F))= (f \o g @ F). +Proof. by []. Qed. + +Lemma within_continuous_withinNx + (R C : numFieldType) (U : normedModType C) (f : U -> R^o) : + {for (0 : U), continuous f} -> + (forall x, f x = 0 -> x = 0) -> f @ nbhs' (0 :U) --> nbhs' (0 : R^o). +Proof. + move => cf f0 A /=. + rewrite !/nbhs /= /nbhs /= /nbhs' /within /= !nearE => H. Admitted. + +Notation "f %:Rfun" := + (f : (Rcomplex_normedModType _) -> (Rcomplex_normedModType _)) + (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: realType). +Notation C := R[i]. +Notation Rcomplex := (Rcomplex R). + +Lemma normcZ (l : R) : forall (x : Rcomplex), + normc (l *: x) = `|l| * (normc x). +Proof. +by case=> ? ?; rewrite /normc //= !exprMn -mulrDr sqrtrM ?sqr_ge0 // sqrtr_sqr. +Qed. + +Lemma realCZ (a : R) : forall (b : Rcomplex), a%:C * b = a *: b. +Proof. by move => [x y]; rewrite /(_ *: _) /=; simpc. Qed. + +Lemma realC_alg (a : R) : a *: (1%:Rc) = a%:C. +Proof. +apply/eqP; rewrite eq_complex; apply/andP. +by split; simpl; apply/eqP; rewrite ?mulr1 ?mulr0. +Qed. + +Lemma scalecr: forall w: C^o, forall r : R, r *: (w: Rcomplex) = r%:C *: w . +Proof. +Proof. by move=> [a b] r; rewrite eqE_complex //=; split; 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 realCV. +Qed. + +Lemma complex0 : 0%:C = 0 :> C. +Proof. rewrite eqE_complex //=. Qed. + + +End algebraic_lemmas. + + +Section complex_topological. +Variable R : realType. +Local Notation C := R[i]. + +Canonical complex_pointedType := + [pointedType of C for pointed_of_zmodule [zmodType of C]]. +Canonical complex_filteredType := + [filteredType C of C for filtered_of_normedZmod [normedZmodType C of C]]. +Canonical complex_topologicalType := + TopologicalType C + (topologyOfEntourageMixin + (uniformityOfBallMixin + (@nbhs_ball_normE _ [normedZmodType C of C]) + (pseudoMetric_of_normedDomain [normedZmodType C of C]))). +Canonical numFieldType_uniformType := UniformType C + (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType C of C]) + (pseudoMetric_of_normedDomain [normedZmodType C of C])). +Canonical numFieldType_pseudoMetricTyp + := @PseudoMetric.Pack [numDomainType of C] C (@PseudoMetric.Class [numDomainType of C] C + (Uniform.class [uniformType of C]) + (@pseudoMetric_of_normedDomain [numDomainType of C] [normedZmodType C of C])). + +Canonical complex_lmodType := + [lmodType R[i] of R[i] for [lmodType R[i] of R[i]^o]]. + +Canonical complex_lalgType := [lalgType C of C for [lalgType C of C^o]]. +Canonical complex_algType := [algType C of C for [algType C of C^o]]. +Canonical complex_comAlgType := [comAlgType C of C]. +Canonical complex_unitAlgType := [unitAlgType C of C]. +Canonical complex_comUnitAlgType := [comUnitAlgType C of C]. +Canonical complex_vectType := [vectType C of C for [vectType C of C^o]]. +Canonical complex_FalgType := [FalgType C of C]. +Canonical complex_fieldExtType := + [fieldExtType C of C for [fieldExtType C of C^o]]. + +Canonical complex_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType C of C for + [pseudoMetricNormedZmodType C of [numFieldType of C^o]]]. +Canonical complex_normedModType := + [normedModType C of C for [normedModType C of C^o]]. + +End complex_topological. + +Section Holomorphe_der. +Variable R : realType. + +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. +Notation Rc := (Rcomplex R). + +Lemma is_cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : + cvg (f @ F) -> cvg ((k \*: f) @ F ). +Proof. by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. Qed. + +Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : + cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). +Proof. by move => cv; apply/esym/cvg_lim => //; apply: cvgZr. Qed. + +Definition holomorphic (f : C^o -> C^o) (c : C) := + cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ (nbhs' (0:C^o))). + +Lemma holomorphicP (f : C^o -> C^o) (c: C^o) : 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). + +(* No Rmodule structure on C if we can avoid, +so the following line shouldn't type check. *) +Fail Definition Rderivable_fromcomplex_false (f : C^o -> C^o) (c v: C^o) := + cvg (fun (h : R^o) => h^-1 *: (f (c +h *: v) - f c)) @ (nbhs' (0:R^o)). + +Definition realC : R^o -> 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); first by []. +by move => z /= nz; apply: (H (realC z)); rewrite /= -realCB realC_norm rRe ltcR. +Qed. + +Lemma Rdiff1 (f : C -> C) c : + lim ( (fun h : C => h^-1 *: ((f (c + h) - f c) ) ) + @ (realC @ (nbhs' 0))) + = 'D_1 (f%:Rfun) c%:Rc :> C. +Proof. +rewrite /derive. +have -> : (fun h : C^o => h^-1 *: ((f (c + h) - f c))) @ (realC @ (nbhs' 0)) = + (fun h : C^o => h^-1 *: ((f (c + h) - f c))) + \o realC @ (nbhs' (0 : R^o)) by []. +suff -> : ( (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC) += (fun h : R^o => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c) ) :> (R -> C) . + by []. +apply: funext => h /=. +by rewrite Inv_realC /= -!scalecr realC_alg [X in f X]addrC. +Qed. + + +Lemma Rdiffi (f : C^o -> C^o) c: + lim ( (fun h : C^o => h^-1 *: ((f (c + h * 'i) - f c))) + @ (realC @ (nbhs' (0 )))) + = 'D_('i) (f%:Rfun) c%:Rc :> C. +Proof. +rewrite /derive. +have -> : + ((fun h : (R[i])^o => h^-1 *: (f (c + h * 'i) - f c)) @ (realC @ nbhs' 0)) + = ((fun h : (R[i])^o => h^-1 *: (f (c + h * 'i) - f c)) \o realC) @ nbhs' 0 by []. +suff -> : (fun h : (R[i])^o => h^-1 * (f (c + h * 'i) - f c)) \o +realC = fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: ('i%:Rc)) - f c). + by []. +apply: funext => h /=. +by rewrite Inv_realC -scalecM -!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 (E : normedModType C) (h e : E -> C) (x : E) : + [o_x (e : E -> C^o) of (h : E -> C^o)] = + [o_x (e : E -> Rc) of (h : E -> Rc)]. +Proof. +suff heP : (h : E -> C^o) =o_x (e : E -> C^o) <-> + (h : E -> Rc) =o_x (e : E -> Rc). + have [ho|hNo] := asboolP ((h : E -> C^o) =o_x (e : E -> C^o)). + by rewrite !littleoE// -!eqoP// -heP. + by rewrite !littleoE0// -!eqoP// -heP. +rewrite !eqoP; split => small _/posnumP[eps]; near=> y. + rewrite -lecR/= !normcR rmorphM/=. + by near: y; apply: small. +rewrite -[_%:num]ger0_norm// -!normcR -rmorphM/= lecR. +by near: y; apply: small; rewrite normc_gt0//. +Grab Existential Variables. all: by end_near. Qed. + +(*extremely long with modified filteredType *) + +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]. +have lDf : linear ('d f c : Rc -> Rc) by move=> t u v; rewrite !scalecr linearP. +pose df : Rc -> Rc := Linear lDf. +have cdf : continuous df by []. +have eqdf : f%:Rfun \o +%R^~ c = cst (f c) + df +o_ (0 : Rc) id + by rewrite holo littleoCo. +by apply/diff_locallyP; rewrite (diff_unique cdf eqdf). +Qed. + +(*The equality between 'i as imaginaryC from ssrnum and 'i is not transparent: + neq0ci is part of ssrnum and uneasy to find *) + +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 @ nbhs' 0) = (quotR \o realC) @ nbhs' 0 by []. +have realC'0: realC @ nbhs' 0 --> nbhs' 0. + apply: within_continuous_withinNx; first by apply: continuous_realC. + by move => /= x /complexI. +have HR0:(quotC \o (realC) @ nbhs' 0) --> l. + by apply: cvg_comp; last by exact: H. +have lem : quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o))) --> l. + apply: cvg_comp; last by exact: H. + rewrite (filter_compE _ realC); apply: cvg_comp; first by exact: realC'0. + apply: within_continuous_withinNx; first by apply: scalel_continuous. + move => x /eqP; rewrite mulIr_eq0 ; last by apply/rregP; apply: neq0Ci. + by move/eqP. +have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o)))) . + by apply/cvg_ex; simpl; exists l. +have ->: lim (quotR @ (realC @ (nbhs' (0 : R^o)))) + = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ (nbhs' (0 : R^o)))). + have: 'i \*:quotC \o ( fun h => h *'i) =1 quotR. + move => h /= ;rewrite /quotC /quotR /=. + rewrite invcM scalerA mulrC -mulrA mulVf ?mulr1 ?neq0Ci //. + by move => /funext <-; rewrite (limin_scaler _ 'i HRcomp). +rewrite scalecM. +suff: lim (quotC @ (realC @ (nbhs' (0 : R^o)))) + = lim (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o)))) by move => -> . +suff -> : lim (quotC @ (realC @ (nbhs' (0 : R^o)))) = l. + by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_map_lim _ lem). +by apply: cvg_map_lim. +Qed. + + +(*TBA normedType- Cyril's suggestion *) +Lemma nbhs'0_le (K : numFieldType) (V : normedModType K) e : + 0 < e -> \forall x \near (nbhs' (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 (K : numFieldType) (V : normedModType K) e : + 0 < e -> \forall x \near (nbhs' (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 nbhs'0_lt (K : numFieldType) (V : normedModType K) e : + 0 < e -> \forall x \near (nbhs' (0 : V)), `|x| < e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +by rewrite -ball_normE /= sub0r normrN. +Qed. + +Lemma nbhs0_lt (K : numFieldType) (V : normedModType K) e : + 0 < e -> \forall x \near (nbhs' (0 : V)), `|x| < e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +by rewrite -ball_normE /= sub0r normrN. +Qed. + +Lemma normc_ge_Im (x : R[i]) : `|complex.Im x|%:C <= `|x|. +Proof. +by case: x => a b; simpc; rewrite -sqrtr_sqr ler_wsqrtr // ler_addr sqr_ge0. +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 scalecM. +pose df := Linear 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 scalecM [in RHS]mulrC. + rewrite [X in 'd _ _ X]zeq addrC linearP linearZ /= -!deriveE //. + rewrite -CR (scalecAl y) -scalecM !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. + by rewrite diff /= lem -littleoCo. +by rewrite (diff_unique cdf holo). +Qed. + +Lemma holomorphic_Rdiff (f : C -> C) (c : C) : + (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c). +Proof. + split => H; first by apply: Diff_CR_holo. + split; first by apply: holo_differentiable. + by apply: holo_CauchyRiemann. +Qed. + +End Holomorphe_der. diff --git a/theories/landau.v b/theories/landau.v index 2a2bd08aa8..5846175d93 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -391,6 +391,11 @@ Lemma littleoE (tag : unit) (F : filter_on T) littleo_def F f h -> the_littleo tag F phF f h = f. Proof. by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed. +Lemma littleoE0 (tag : unit) (F : filter_on T) + (phF : phantom (set (set T)) F) f h : + ~ littleo_def F f h -> the_littleo tag F phF f h = 0. +Proof. by move=> ?; rewrite /the_littleo /insubd insubN//; apply/asboolP. Qed. + Canonical the_littleo_littleo (tag : unit) (F : filter_on T) (phF : phantom (set_system T) F) f h := [littleo of the_littleo tag F phF f h]. From 0e8adbaf464a6a7eb86c7f8dd82a20c4e638c58a Mon Sep 17 00:00:00 2001 From: Marie Date: Mon, 22 Mar 2021 09:59:31 +0100 Subject: [PATCH 06/10] ComplexNumfieldtype --- theories/holomorphy.v | 112 ++++++++++++++++++++++++++++-------------- 1 file changed, 74 insertions(+), 38 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 48b6b094d7..afb8881e18 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -11,6 +11,7 @@ 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. @@ -19,6 +20,41 @@ Unset Printing Implicit Defensive. (* I need to import ComplexField to use its lemmas on RComplex, I don't want the canonical lmodtype structure on C, Therefore this is based on a fork of real-closed *) +Section ComplexNumfieldType. +Variable R : rcfType. +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. + +Local Canonical complex_pointedType := [pointedType of C for [pointedType of C^o]]. +Local Canonical complex_filteredType := + [filteredType C of C for [filteredType C of C^o]]. +Local Canonical complex_topologicalType := + [topologicalType of C for [topologicalType of C^o]]. +Local Canonical complex_uniformType := [uniformType of C for [uniformType of C^o]]. + +Local Canonical complex_pseudoMetricType := + [pseudoMetricType [numDomainType of C] of C for [pseudoMetricType [numDomainType of C] of C^o]]. +(* missing join ? is [numDomainType of C] ok here ? *) + +Local Canonical complex_lmodType := [lmodType C of C for [lmodType C of C^o]]. +Local Canonical complex_lalgType := [lalgType C of C for [lalgType C of C^o]]. +Local Canonical complex_algType := [algType C of C for [algType C of C^o]]. +Local Canonical complex_comAlgType := [comAlgType C of C]. +Local Canonical complex_unitAlgType := [unitAlgType C of C]. +Local Canonical complex_comUnitAlgType := [comUnitAlgType C of C]. +Local Canonical complex_vectType := [vectType C of C for [vectType C of C^o]]. +Local Canonical complex_FalgType := [FalgType C of C]. +Local Canonical complex_fieldExtType := + [fieldExtType C of C for [fieldExtType C of C^o]]. +Local Canonical complex_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType C of C for [pseudoMetricNormedZmodType C of C^o]]. +Local Canonical complex_normedModType := + [normedModType C of C for [normedModType C of C^o]]. + +(* TODO : joins*) + +End ComplexNumfieldType. + Section complex_extras. Variable R : rcfType. @@ -33,8 +69,8 @@ by move=> -> ; split. by case=> //= -> ->. Qed. -Lemma Re0 : Re 0 = 0 :> R. -Proof. by []. Qed. +Lemma Re0 : Re 0 = 0 :> R. +Proof. by []. Qed. Lemma Im0 : Im 0 = 0 :> R. Proof. by []. Qed. @@ -42,13 +78,13 @@ Proof. by []. Qed. Lemma ReIm_eq0 (x : C) : (x = 0) = ((Re x = 0) /\ (Im x = 0)). Proof. by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. Qed. -Lemma scalei_muli (z : C^o) : 'i * z = 'i *: z. +Lemma scalei_muli (z : C) : 'i * z = 'i *: z. Proof. by []. Qed. Lemma iE : 'i%C = 'i :> C. Proof. by []. Qed. -Lemma scalecM : forall (w v : C^o), (v *: w = v * w). +Lemma scalecM : forall (w v : C), (v *: w = v * w). Proof. by []. Qed. Lemma normc0 : normc 0 = 0 :> R . @@ -125,7 +161,7 @@ Qed. Lemma realCM (a b :R) : a%:C * b%:C = (a * b)%:C. Proof. by rewrite eqE_complex /= !mulr0 mul0r addr0 subr0. Qed. -Lemma complexA: forall (h : C^o), h%:A = h. +Lemma complexA: forall (h : C), h%:A = h. Proof. by move => h; rewrite scalecM mulr1. Qed. Lemma lecM (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). @@ -319,12 +355,12 @@ Lemma filter_compE ( T U V : topologicalType) Proof. by []. Qed. Lemma within_continuous_withinNx - (R C : numFieldType) (U : normedModType C) (f : U -> R^o) : + (R C : numFieldType) (U : normedModType C) (f : U -> R) : {for (0 : U), continuous f} -> - (forall x, f x = 0 -> x = 0) -> f @ nbhs' (0 :U) --> nbhs' (0 : R^o). + (forall x, f x = 0 -> x = 0) -> f @ nbhs' (0 :U) --> nbhs' (0 : R). Proof. move => cf f0 A /=. - rewrite !/nbhs /= /nbhs /= /nbhs' /within /= !nearE => H. Admitted. + rewrite !/nbhs /= /nbhs /= /nbhs' /within /= !nearE => []. Admitted. Notation "f %:Rfun" := (f : (Rcomplex_normedModType _) -> (Rcomplex_normedModType _)) @@ -353,7 +389,7 @@ apply/eqP; rewrite eq_complex; apply/andP. by split; simpl; apply/eqP; rewrite ?mulr1 ?mulr0. Qed. -Lemma scalecr: forall w: C^o, forall r : R, r *: (w: Rcomplex) = r%:C *: w . +Lemma scalecr: forall w: C, forall r : R, r *: (w: Rcomplex) = r%:C *: w . Proof. Proof. by move=> [a b] r; rewrite eqE_complex //=; split; simpc. Qed. @@ -370,7 +406,7 @@ Proof. rewrite eqE_complex //=. Qed. End algebraic_lemmas. -Section complex_topological. +(* Section complex_topological. Variable R : realType. Local Notation C := R[i]. @@ -411,7 +447,7 @@ Canonical complex_pseudoMetricNormedZmodType := Canonical complex_normedModType := [normedModType C of C for [normedModType C of C^o]]. -End complex_topological. +End complex_topological. *) Section Holomorphe_der. Variable R : realType. @@ -430,10 +466,10 @@ Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). Proof. by move => cv; apply/esym/cvg_lim => //; apply: cvgZr. Qed. -Definition holomorphic (f : C^o -> C^o) (c : C) := - cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ (nbhs' (0:C^o))). +Definition holomorphic (f : C-> C ) (c : C) := + cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ (nbhs' (0:C))). -Lemma holomorphicP (f : C^o -> C^o) (c: C^o) : holomorphic f c <-> derivable f c 1. +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))) = @@ -445,16 +481,16 @@ Definition Rdifferentiable (f : C -> C) (c : C) := (differentiable f%:Rfun c%:Rc (* No Rmodule structure on C if we can avoid, so the following line shouldn't type check. *) -Fail Definition Rderivable_fromcomplex_false (f : C^o -> C^o) (c v: C^o) := - cvg (fun (h : R^o) => h^-1 *: (f (c +h *: v) - f c)) @ (nbhs' (0:R^o)). +Fail Definition Rderivable_fromcomplex_false (f : C -> C) (c v: C) := + cvg (fun (h : R) => h^-1 *: (f (c +h *: v) - f c)) @ (nbhs' (0:R)). -Definition realC : R^o -> C := (fun r => r%:C). +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); first by []. by move => z /= nz; apply: (H (realC z)); rewrite /= -realCB realC_norm rRe ltcR. -Qed. +Qed. Lemma Rdiff1 (f : C -> C) c : lim ( (fun h : C => h^-1 *: ((f (c + h) - f c) ) ) @@ -462,27 +498,27 @@ Lemma Rdiff1 (f : C -> C) c : = 'D_1 (f%:Rfun) c%:Rc :> C. Proof. rewrite /derive. -have -> : (fun h : C^o => h^-1 *: ((f (c + h) - f c))) @ (realC @ (nbhs' 0)) = - (fun h : C^o => h^-1 *: ((f (c + h) - f c))) - \o realC @ (nbhs' (0 : R^o)) by []. +have -> : (fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ (nbhs' 0)) = + (fun h : C => h^-1 *: ((f (c + h) - f c))) + \o realC @ (nbhs' (0 : R)) by []. suff -> : ( (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC) -= (fun h : R^o => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c) ) :> (R -> C) . - by []. += (fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c) ) :> (R -> C) . + by []. (*TODO : very long*) apply: funext => h /=. by rewrite Inv_realC /= -!scalecr realC_alg [X in f X]addrC. Qed. -Lemma Rdiffi (f : C^o -> C^o) c: - lim ( (fun h : C^o => h^-1 *: ((f (c + h * 'i) - f c))) +Lemma Rdiffi (f : C -> C) c: + lim ( (fun h : C => h^-1 *: ((f (c + h * 'i) - f c))) @ (realC @ (nbhs' (0 )))) = 'D_('i) (f%:Rfun) c%:Rc :> C. Proof. rewrite /derive. have -> : - ((fun h : (R[i])^o => h^-1 *: (f (c + h * 'i) - f c)) @ (realC @ nbhs' 0)) - = ((fun h : (R[i])^o => h^-1 *: (f (c + h * 'i) - f c)) \o realC) @ nbhs' 0 by []. -suff -> : (fun h : (R[i])^o => h^-1 * (f (c + h * 'i) - f c)) \o + ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) @ (realC @ nbhs' 0)) + = ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) \o realC) @ nbhs' 0 by []. +suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC = fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: ('i%:Rc)) - f c). by []. apply: funext => h /=. @@ -492,12 +528,12 @@ Qed. (* should be generalized to equivalent norms *) (* but there is no way to state it for now *) Lemma littleoCo (E : normedModType C) (h e : E -> C) (x : E) : - [o_x (e : E -> C^o) of (h : E -> C^o)] = + [o_x (e : E -> C) of (h : E -> C)] = [o_x (e : E -> Rc) of (h : E -> Rc)]. Proof. -suff heP : (h : E -> C^o) =o_x (e : E -> C^o) <-> +suff heP : (h : E -> C) =o_x (e : E -> C) <-> (h : E -> Rc) =o_x (e : E -> Rc). - have [ho|hNo] := asboolP ((h : E -> C^o) =o_x (e : E -> C^o)). + have [ho|hNo] := asboolP ((h : E -> C) =o_x (e : E -> C)). by rewrite !littleoE// -!eqoP// -heP. by rewrite !littleoE0// -!eqoP// -heP. rewrite !eqoP; split => small _/posnumP[eps]; near=> y. @@ -539,24 +575,24 @@ have realC'0: realC @ nbhs' 0 --> nbhs' 0. by move => /= x /complexI. have HR0:(quotC \o (realC) @ nbhs' 0) --> l. by apply: cvg_comp; last by exact: H. -have lem : quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o))) --> l. +have lem : quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R))) --> l. apply: cvg_comp; last by exact: H. rewrite (filter_compE _ realC); apply: cvg_comp; first by exact: realC'0. apply: within_continuous_withinNx; first by apply: scalel_continuous. move => x /eqP; rewrite mulIr_eq0 ; last by apply/rregP; apply: neq0Ci. by move/eqP. -have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o)))) . +have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R)))) . by apply/cvg_ex; simpl; exists l. -have ->: lim (quotR @ (realC @ (nbhs' (0 : R^o)))) - = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ (nbhs' (0 : R^o)))). +have ->: lim (quotR @ (realC @ (nbhs' (0 : R)))) + = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ (nbhs' (0 : R)))). have: 'i \*:quotC \o ( fun h => h *'i) =1 quotR. move => h /= ;rewrite /quotC /quotR /=. rewrite invcM scalerA mulrC -mulrA mulVf ?mulr1 ?neq0Ci //. by move => /funext <-; rewrite (limin_scaler _ 'i HRcomp). rewrite scalecM. -suff: lim (quotC @ (realC @ (nbhs' (0 : R^o)))) - = lim (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o)))) by move => -> . -suff -> : lim (quotC @ (realC @ (nbhs' (0 : R^o)))) = l. +suff: lim (quotC @ (realC @ (nbhs' (0 : R)))) + = lim (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R)))) by move => -> . +suff -> : lim (quotC @ (realC @ (nbhs' (0 : R)))) = l. by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_map_lim _ lem). by apply: cvg_map_lim. Qed. From 1896f909d7d30ce23eab84b22b2159f72a85ed4f Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 22 May 2025 14:21:36 +0200 Subject: [PATCH 07/10] port to MC2 (wip) --- theories/holomorphy.v | 263 ++++++++++++++---------------------------- 1 file changed, 84 insertions(+), 179 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index afb8881e18..3f07d490d4 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -1,11 +1,12 @@ (* 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 choice fintype bigop order ssralg ssrnum ssrfun. From mathcomp Require Import complex. From mathcomp Require Import boolp reals ereal derive. -Require Import classical_sets posnum topology normedtype landau. +From mathcomp Require Import classical_sets functions interval_inference topology normedtype landau. Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def complex. Local Open Scope ring_scope. @@ -20,47 +21,39 @@ Unset Printing Implicit Defensive. (* I need to import ComplexField to use its lemmas on RComplex, I don't want the canonical lmodtype structure on C, Therefore this is based on a fork of real-closed *) -Section ComplexNumfieldType. -Variable R : rcfType. -Local Notation sqrtr := Num.sqrt. -Local Notation C := R[i]. +HB.instance Definition _ (R : rcfType) := NormedModule.copy R[i] R[i]^o. -Local Canonical complex_pointedType := [pointedType of C for [pointedType of C^o]]. -Local Canonical complex_filteredType := - [filteredType C of C for [filteredType C of C^o]]. -Local Canonical complex_topologicalType := - [topologicalType of C for [topologicalType of C^o]]. -Local Canonical complex_uniformType := [uniformType of C for [uniformType of C^o]]. - -Local Canonical complex_pseudoMetricType := - [pseudoMetricType [numDomainType of C] of C for [pseudoMetricType [numDomainType of C] of C^o]]. -(* missing join ? is [numDomainType of C] ok here ? *) - -Local Canonical complex_lmodType := [lmodType C of C for [lmodType C of C^o]]. -Local Canonical complex_lalgType := [lalgType C of C for [lalgType C of C^o]]. -Local Canonical complex_algType := [algType C of C for [algType C of C^o]]. -Local Canonical complex_comAlgType := [comAlgType C of C]. -Local Canonical complex_unitAlgType := [unitAlgType C of C]. -Local Canonical complex_comUnitAlgType := [comUnitAlgType C of C]. -Local Canonical complex_vectType := [vectType C of C for [vectType C of C^o]]. -Local Canonical complex_FalgType := [FalgType C of C]. -Local Canonical complex_fieldExtType := - [fieldExtType C of C for [fieldExtType C of C^o]]. -Local Canonical complex_pseudoMetricNormedZmodType := - [pseudoMetricNormedZmodType C of C for [pseudoMetricNormedZmodType C of C^o]]. -Local Canonical complex_normedModType := - [normedModType C of C for [normedModType C of C^o]]. +HB.factory Record Normed_And_Lmodule_isNormedModule (K : numFieldType) R of @Num.NormedZmodule K R & GRing.Lmodule K R := { + normrZ : forall (l : K) (x : R), normr (l *: x) = normr l * normr x; +}. + +HB.builders Context K R of Normed_And_Lmodule_isNormedModule K R. +HB.instance Definition _ := PseudoMetric.copy R (@pseudometric K R). +HB.instance Definition _ := Pointed.copy R R^o. -(* TODO : joins*) +Lemma pseudo_metric_ball_norm : ball = ball_ (@normr K R). +Proof. by []. Qed. + +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K R pseudo_metric_ball_norm. + +HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K R normrZ. +HB.end. -End ComplexNumfieldType. +Lemma normcZ (R : rcfType) (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 _ (R : rcfType) := Normed_And_Lmodule_isNormedModule.Build R (Rcomplex R) (@normcZ R). +(* TODO: backport to real-closed *) Section complex_extras. Variable R : rcfType. Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. +Import Normc. + (*Adapting lemma eq_complex from complex.v, which was done in boolean style*) Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). Proof. @@ -245,7 +238,7 @@ Lemma real_normc_ler (x y : R) : `|x| <= normc (x +i* y). Proof. rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. -rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=; last by apply: num_real. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. by rewrite ler_addl ?sqr_ge0. Qed. @@ -253,117 +246,28 @@ Lemma im_normc_ler (x y : R) : `|y| <= normc (x +i* y). Proof. rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. -rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=; last by apply: num_real. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. by rewrite ler_addr ?sqr_ge0. Qed. End complex_extras. -Section Rcomplex. - - -Canonical Rcomplex_lmodType (R : rcfType) := - LmodType R (Rcomplex R) (complex_real_lmodMixin R). - -Lemma scalecAl (R : rcfType) (h : R) (x y : Rcomplex R) : h *: (x * y) = h *: x * y. -Proof. -by move: h x y => h [a b] [c d]; simpc; rewrite -!mulrA -mulrBr -mulrDr. -Qed. - - -Canonical Rcomplex_lalgType (R : rcfType) := LalgType R (Rcomplex R) (@scalecAl R). - -Definition Rcomplex_normedZmodMixin (R: realType) := - @Num.NormedMixin R (Rcomplex_zmodType R) _ _ (@normcD R) (@eq0_normc R) - (@normc_mulrn R) (@normcN R). - -Canonical Rcomplex_normedZmodType (R: realType) := - NormedZmodType R (Rcomplex R) (Rcomplex_normedZmodMixin R). - -Definition Rcomplex_pseudoMetricMixin (R: realType) := - (@pseudoMetric_of_normedDomain R (Rcomplex_normedZmodType R)). - - -Canonical Rcomplex_pointedType (R: realType) := - [pointedType of (Rcomplex R) for [pointedType of R[i]^o]]. - -Canonical Rcomplex_filteredType (R: realType) := - [filteredType (Rcomplex R) of (Rcomplex R) for [filteredType R[i]^o of R[i]^o]]. - -Canonical Rcomplex_topologicalType (R: realType) := - [topologicalType of (Rcomplex R) for [topologicalType of R[i]^o]]. - -Program Definition Rcomplex_uniformMixin (R: realType): - Uniform.mixin_of (nbhs (U := Rcomplex R) ) := - (@UniformMixin (Rcomplex R) (nbhs (U := Rcomplex R)) - (entourage_ ((ball_ (@normc R)))) _ _ _ _ _). -Obligation 1. Admitted. -Obligation 2. Admitted. -Obligation 3. Admitted. -Obligation 4. Admitted. -Obligation 5. -move => R; rewrite /nbhs /= /nbhs_ /nbhs_ball_ /filter_from /entourage_ /= /filter_from /=. -apply/funext => x //=. -apply/funext => P /=; rewrite propeqE; split. - move => [r /[dup] /realC_gt0 r0 /gt0_realC rr] H. - rewrite /entourage_ /filter_from /=. - exists (fun xy => (normc ( xy.1 - xy.2) < Re r)). - exists (Re r) => //. - by move=> z /= h; apply: (H z); rewrite /= rr ltcR. -move => [B [] r r0] H /= H'; exists r%:C; first by rewrite ltcR. -move => z h; apply: H' => /=; apply: H => /=. -by rewrite -ltcR /=. -Qed. - -Canonical Rcomplex_uniformType (R: realType) := - UniformType (Rcomplex R) (Rcomplex_uniformMixin R). - -Canonical Rcomplex_pseudoMetricType (R: realType) := - PseudoMetricType (Rcomplex R) (Rcomplex_pseudoMetricMixin R). - - -Lemma Rcomplex_ball_ball_ (R: realType): - @ball _ (Rcomplex_pseudoMetricType R ) = ball_ (fun x => `| x |). -Proof. by []. Qed. - -Definition Rcomplex_pseudoMetricNormedZmodMixin (R: realType):= - PseudoMetricNormedZmodule.Mixin (Rcomplex_ball_ball_ (R: realType)). - -Canonical Rcomplex_pseudoMetricNormedZmodType (R: realType) := - PseudoMetricNormedZmodType R (Rcomplex R) - (Rcomplex_pseudoMetricNormedZmodMixin R). - -Lemma RnormcZ (R: realType) (l : R) : forall (x : Rcomplex R), - normc (l *: x) = `|l| * (normc x). -Proof. -by case=> ? ?; rewrite /normc //= !exprMn -mulrDr sqrtrM ?sqr_ge0 // sqrtr_sqr. -Qed. - -Definition Rcomplex_normedModMixin (R: realType):= - @NormedModMixin R (Rcomplex_pseudoMetricNormedZmodType R) _ (@RnormcZ R). - -Canonical Rcomplex_normedModType (R: realType):= - NormedModType R (Rcomplex R) (Rcomplex_normedModMixin R). - -End Rcomplex. - - Lemma filter_compE ( T U V : topologicalType) (f : T -> U) (g : V -> T) - (F : set ( set V)) : + (F : set_system V) : (f @ (g @ F))= (f \o g @ F). Proof. by []. Qed. Lemma within_continuous_withinNx (R C : numFieldType) (U : normedModType C) (f : U -> R) : {for (0 : U), continuous f} -> - (forall x, f x = 0 -> x = 0) -> f @ nbhs' (0 :U) --> nbhs' (0 : R). + (forall x, f x = 0 -> x = 0) -> f @ dnbhs (0 :U) --> dnbhs (0 : R). Proof. move => cf f0 A /=. - rewrite !/nbhs /= /nbhs /= /nbhs' /within /= !nearE => []. Admitted. +(*rewrite !/nbhs /= /nbhs /= /within /= !nearE => [].*) Admitted. Notation "f %:Rfun" := - (f : (Rcomplex_normedModType _) -> (Rcomplex_normedModType _)) + (f : (Rcomplex _ : normedModType _) -> (Rcomplex _ : normedModType _)) (at level 5, format "f %:Rfun") : complex_scope. Notation "v %:Rc" := (v : (Rcomplex _)) @@ -374,11 +278,7 @@ Variable (R: realType). Notation C := R[i]. Notation Rcomplex := (Rcomplex R). -Lemma normcZ (l : R) : forall (x : Rcomplex), - normc (l *: x) = `|l| * (normc x). -Proof. -by case=> ? ?; rewrite /normc //= !exprMn -mulrDr sqrtrM ?sqr_ge0 // sqrtr_sqr. -Qed. +Import Normc. Lemma realCZ (a : R) : forall (b : Rcomplex), a%:C * b = a *: b. Proof. by move => [x y]; rewrite /(_ *: _) /=; simpc. Qed. @@ -457,17 +357,17 @@ Local Notation C := R[i]. Notation Rc := (Rcomplex R). Lemma is_cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : + (F : set_system T) (H : Filter F) (f : T -> V) (k : K) : cvg (f @ F) -> cvg ((k \*: f) @ F ). Proof. by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. Qed. Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : + (F : set_system T) (FF : ProperFilter F) (f : T -> V) (k : K) : cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). Proof. by move => cv; apply/esym/cvg_lim => //; apply: cvgZr. Qed. Definition holomorphic (f : C-> C ) (c : C) := - cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ (nbhs' (0:C))). + cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ (dnbhs (0:C))). Lemma holomorphicP (f : C -> C) (c: C) : holomorphic f c <-> derivable f c 1. Proof. @@ -482,7 +382,7 @@ Definition Rdifferentiable (f : C -> C) (c : C) := (differentiable f%:Rfun c%:Rc (* No Rmodule structure on C if we can avoid, so the following line shouldn't type check. *) Fail Definition Rderivable_fromcomplex_false (f : C -> C) (c v: C) := - cvg (fun (h : R) => h^-1 *: (f (c +h *: v) - f c)) @ (nbhs' (0:R)). + cvg (fun (h : R) => h^-1 *: (f (c +h *: v) - f c)) @ (dnbhs (0:R)). Definition realC : R -> C := (fun r => r%:C). @@ -494,36 +394,36 @@ Qed. Lemma Rdiff1 (f : C -> C) c : lim ( (fun h : C => h^-1 *: ((f (c + h) - f c) ) ) - @ (realC @ (nbhs' 0))) + @ (realC @ (dnbhs 0))) = 'D_1 (f%:Rfun) c%:Rc :> C. Proof. rewrite /derive. -have -> : (fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ (nbhs' 0)) = +have -> : (fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ (dnbhs 0)) = (fun h : C => h^-1 *: ((f (c + h) - f c))) - \o realC @ (nbhs' (0 : R)) by []. + \o realC @ (dnbhs (0 : R)) by []. suff -> : ( (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC) -= (fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c) ) :> (R -> C) . - by []. (*TODO : very long*) += (fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c : Rcomplex _) ) :> (R -> C) . + admit. apply: funext => h /=. by rewrite Inv_realC /= -!scalecr realC_alg [X in f X]addrC. -Qed. +Admitted. Lemma Rdiffi (f : C -> C) c: lim ( (fun h : C => h^-1 *: ((f (c + h * 'i) - f c))) - @ (realC @ (nbhs' (0 )))) + @ (realC @ (dnbhs (0 )))) = 'D_('i) (f%:Rfun) c%:Rc :> C. Proof. rewrite /derive. have -> : - ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) @ (realC @ nbhs' 0)) - = ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) \o realC) @ nbhs' 0 by []. + ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) @ (realC @ dnbhs 0)) + = ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) \o realC) @ dnbhs 0 by []. suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o -realC = fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: ('i%:Rc)) - f c). - by []. +realC = fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: ('i%:Rc)) - f c : Rcomplex _). + admit. apply: funext => h /=. by rewrite Inv_realC -scalecM -!scalecr realCZ [X in f X]addrC. -Qed. +Admitted. (* should be generalized to equivalent norms *) (* but there is no way to state it for now *) @@ -536,12 +436,13 @@ suff heP : (h : E -> C) =o_x (e : E -> C) <-> have [ho|hNo] := asboolP ((h : E -> C) =o_x (e : E -> C)). by rewrite !littleoE// -!eqoP// -heP. by rewrite !littleoE0// -!eqoP// -heP. -rewrite !eqoP; split => small _/posnumP[eps]; near=> y. +rewrite !eqoP; split => small/= _ /posnumP[eps]; near=> y. rewrite -lecR/= !normcR rmorphM/=. - by near: y; apply: small. + near: y. + exact: small. rewrite -[_%:num]ger0_norm// -!normcR -rmorphM/= lecR. by near: y; apply: small; rewrite normc_gt0//. -Grab Existential Variables. all: by end_near. Qed. +Unshelve. all: by end_near. Qed. (*extremely long with modified filteredType *) @@ -552,13 +453,16 @@ Lemma holo_differentiable (f : C -> C) (c : C) : holomorphic f c -> Rdifferentiable f c. Proof. move=> /holomorphicP /derivable1_diffP /diff_locallyP => -[cdiff holo]. -have lDf : linear ('d f c : Rc -> Rc) by move=> t u v; rewrite !scalecr linearP. -pose df : Rc -> Rc := Linear lDf. -have cdf : continuous df by []. -have eqdf : f%:Rfun \o +%R^~ c = cst (f c) + df +o_ (0 : Rc) id - by rewrite holo littleoCo. +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). +have cdf : continuous df'. + admit. +have eqdf : f%:Rfun \o +%R^~ c = cst (f c) + df' +o_ (0 : Rc) id. + rewrite holo littleoCo. + admit. by apply/diff_locallyP; rewrite (diff_unique cdf eqdf). -Qed. +Admitted. (*The equality between 'i as imaginaryC from ssrnum and 'i is not transparent: neq0ci is part of ssrnum and uneasy to find *) @@ -569,38 +473,38 @@ 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 @ nbhs' 0) = (quotR \o realC) @ nbhs' 0 by []. -have realC'0: realC @ nbhs' 0 --> nbhs' 0. +have -> : quotR @ (realC @ dnbhs 0) = (quotR \o realC) @ dnbhs 0 by []. +have realC'0: realC @ dnbhs 0 --> dnbhs 0. apply: within_continuous_withinNx; first by apply: continuous_realC. by move => /= x /complexI. -have HR0:(quotC \o (realC) @ nbhs' 0) --> l. +have HR0:(quotC \o (realC) @ dnbhs 0) --> l. by apply: cvg_comp; last by exact: H. -have lem : quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R))) --> l. +have lem : quotC \o *%R^~ 'i%R @ (realC @ (dnbhs (0 : R))) --> l. apply: cvg_comp; last by exact: H. rewrite (filter_compE _ realC); apply: cvg_comp; first by exact: realC'0. apply: within_continuous_withinNx; first by apply: scalel_continuous. move => x /eqP; rewrite mulIr_eq0 ; last by apply/rregP; apply: neq0Ci. by move/eqP. -have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R)))) . +have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ (dnbhs (0 : R)))) . by apply/cvg_ex; simpl; exists l. -have ->: lim (quotR @ (realC @ (nbhs' (0 : R)))) - = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ (nbhs' (0 : R)))). +have ->: lim (quotR @ (realC @ (dnbhs (0 : R)))) + = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ (dnbhs (0 : R)))). have: 'i \*:quotC \o ( fun h => h *'i) =1 quotR. move => h /= ;rewrite /quotC /quotR /=. rewrite invcM scalerA mulrC -mulrA mulVf ?mulr1 ?neq0Ci //. by move => /funext <-; rewrite (limin_scaler _ 'i HRcomp). rewrite scalecM. -suff: lim (quotC @ (realC @ (nbhs' (0 : R)))) - = lim (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R)))) by move => -> . -suff -> : lim (quotC @ (realC @ (nbhs' (0 : R)))) = l. - by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_map_lim _ lem). -by apply: cvg_map_lim. +suff: lim (quotC @ (realC @ (dnbhs (0 : R)))) + = lim (quotC \o *%R^~ 'i%R @ (realC @ (dnbhs (0 : R)))) by move => -> . +suff -> : lim (quotC @ (realC @ (dnbhs (0 : R)))) = l. + by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_lim _ lem). +by apply: cvg_lim. Qed. (*TBA normedType- Cyril's suggestion *) -Lemma nbhs'0_le (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (nbhs' (0 : V)), `|x| <= e. +Lemma dnbhs0_le (K : numFieldType) (V : normedModType K) e : + 0 < e -> \forall x \near (dnbhs (0 : V)), `|x| <= e. Proof. move=> e_gt0; apply/nbhs_ballP; exists e => // x. rewrite -ball_normE /= sub0r normrN => le_nxe _ . @@ -608,22 +512,22 @@ by rewrite ltW. Qed. Lemma nbhs0_le (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (nbhs' (0 : V)), `|x| <= e. + 0 < e -> \forall x \near (dnbhs (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 nbhs'0_lt (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (nbhs' (0 : V)), `|x| < e. +Lemma dnbhs0_lt (K : numFieldType) (V : normedModType K) e : + 0 < e -> \forall x \near (dnbhs (0 : V)), `|x| < e. Proof. move=> e_gt0; apply/nbhs_ballP; exists e => // x. by rewrite -ball_normE /= sub0r normrN. Qed. Lemma nbhs0_lt (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (nbhs' (0 : V)), `|x| < e. + 0 < e -> \forall x \near (dnbhs (0 : V)), `|x| < e. Proof. move=> e_gt0; apply/nbhs_ballP; exists e => // x. by rewrite -ball_normE /= sub0r normrN. @@ -645,7 +549,7 @@ 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 scalecM. -pose df := Linear lDf. +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. @@ -653,13 +557,14 @@ have lem : Df = 'd (f%:Rfun) (c : Rc). (* issue with notation *) have zeq : z = x *: 1 %:Rc + y *: 'i%:Rc. by rewrite [LHS]complexE /= realC_alg scalecr scalecM [in RHS]mulrC. rewrite [X in 'd _ _ X]zeq addrC linearP linearZ /= -!deriveE //. - rewrite -CR (scalecAl y) -scalecM !scalecr /=. + rewrite -CR (scalerAl y) -scalecM !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. - by rewrite diff /= lem -littleoCo. + rewrite diff /= lem. + admit. by rewrite (diff_unique cdf holo). -Qed. +Admitted. Lemma holomorphic_Rdiff (f : C -> C) (c : C) : (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c). From e9fef19fea02716cf54ee67659b219e9aefd0dbe Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 22 May 2025 18:25:21 +0200 Subject: [PATCH 08/10] wip and tried making factory from uniform to normedModType --- theories/holomorphy.v | 31 +++++++++++++- theories/normedtype_theory/normed_module.v | 50 ++++++++++++++++++++++ 2 files changed, 79 insertions(+), 2 deletions(-) diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 3f07d490d4..1d9bc58ea3 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -23,6 +23,25 @@ I don't want the canonical lmodtype structure on C, Therefore this is based on a fork of real-closed *) HB.instance Definition _ (R : rcfType) := NormedModule.copy R[i] R[i]^o. +HB.instance Definition _ (R : rcfType) := Uniform.copy (Rcomplex R) R[i]. +HB.instance Definition _ (R : rcfType) := Pointed.copy (Rcomplex R) R[i]. + +Section Rcomplex_NormedModType. +Variable (R : rcfType). +HB.howto Rcomplex normedModType 11. + +Definition ball : R -> Rcomplex R -> R -> Prop + - ball_center_subproof : forall (x : M) (e : R), 0 < e -> ball x e x + - ball_sym_subproof : forall (x y : M) (e : R), ball x e y -> ball y e x + - ball_triangle_subproof : + forall (x y z : M) (e1 e2 : R), + ball x e1 y -> ball y e2 z -> ball x (e1 + e2)%E z + - entourageE_subproof : entourage = entourage_ ball + +HB.about Uniform_isPseudoMetric.Build. +; NormedZmod_PseudoMetric_eq; + PseudoMetricNormedZmod_Lmodule_isNormedModule + HB.factory Record Normed_And_Lmodule_isNormedModule (K : numFieldType) R of @Num.NormedZmodule K R & GRing.Lmodule K R := { normrZ : forall (l : K) (x : R), normr (l *: x) = normr l * normr x; }. @@ -239,7 +258,7 @@ Lemma real_normc_ler (x y : R) : Proof. rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. -by rewrite ler_addl ?sqr_ge0. +by rewrite lerDl ?sqr_ge0. Qed. Lemma im_normc_ler (x y : R) : @@ -247,7 +266,7 @@ Lemma im_normc_ler (x y : R) : Proof. rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. -by rewrite ler_addr ?sqr_ge0. +by rewrite lerDr ?sqr_ge0. Qed. End complex_extras. @@ -403,6 +422,14 @@ have -> : (fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ (dnbhs 0)) = \o realC @ (dnbhs (0 : R)) by []. suff -> : ( (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC) = (fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c : Rcomplex _) ) :> (R -> C) . +STOP. +rewrite /=. +f_equal => /=. +Set Printing All. +Search lim Logic.eq . +Search (lim _ = lim _). +Set Printing All. +apply: lim_eq. admit. apply: funext => h /=. by rewrite Inv_realC /= -!scalecr realC_alg [X in f X]addrC. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 0ffaa69c57..4c2377f0b1 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2063,3 +2063,53 @@ HB.instance Definition _ := Check M : normedModType R. HB.end. + +HB.factory Record Uniform_Lmodule_isNormed (R : numFieldType) M of Uniform M & GRing.Lmodule R M := { + norm : M -> R; + ler_normD : forall x y, norm (x + y) <= norm x + norm y ; + normrZ : forall (l : R) (x : M), norm (l *: x) = `|l| * norm x ; + normr0_eq0 : forall x : M, norm x = 0 -> x = 0 ; + entourage_norm : forall x : M, nbhs_ball_ (ball_ norm) x = filter.nbhs x; +}. + +HB.builders Context R M of Uniform_Lmodule_isNormed R M. + +Lemma normrMn (x : M) (n : nat) : norm (x *+ n) = norm x *+ n. +Proof. + admit. +Admitted. + + +Lemma normrN (x : M) : norm (- x) = norm x. +Proof. admit. Admitted. + +HB.instance Definition _ := Num.Zmodule_isNormed.Build R M ler_normD normr0_eq0 normrMn normrN. +HB.instance Definition _ := isPointed.Build M 0. + +Definition ball := ball_ (fun x : M => `|x|). + +Lemma ball_center_subproof (x : M) (e : R) : 0 < e -> ball x e x. +Proof. by rewrite /ball /ball_/= subrr normr0. Qed. + +Lemma ball_sym_subproof (x y : M) (e : R) : ball x e y -> ball y e x. +Proof. by rewrite /ball /ball_/= distrC. Qed. + +Lemma ball_triangle_subproof (x y z : M) (e1 e2 : R) : + ball x e1 y -> + ball y e2 z -> + ball x (e1 + e2)%E z. +Proof. +rewrite /ball /ball_/= => ? ?. +rewrite -[x](subrK y) -(addrA (x + _)). +by rewrite (le_lt_trans (ler_normD _ _))// ltrD. +Qed. + +Lemma entourageE_subproof : entourage = entourage_ ball. +Proof. admit. Admitted. + +HB.instance Definition _ := Uniform_isPseudoMetric.Build R M ball_center_subproof ball_sym_subproof ball_triangle_subproof entourageE_subproof. + +HB.about NormedZmod_PseudoMetric_eq.Build. +; PseudoMetricNormedZmod_Lmodule_isNormedModule + +HB.howto M normedModType. From 73f40eb9e0ef003fb9385d962652c182854a3d07 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 3 Jun 2025 18:04:53 +0200 Subject: [PATCH 09/10] wip --- classical/unstable.v | 131 +++- theories/function_spaces.v | 34 + theories/holomorphy.v | 653 +++++-------------- theories/normedtype_theory/normed_module.v | 344 +++++++--- theories/topology_theory/num_topology.v | 4 + theories/topology_theory/uniform_structure.v | 20 + theories/tvs.v | 48 ++ 7 files changed, 650 insertions(+), 584 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 563dcb9891..780bad49b1 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. -From mathcomp Require Import archimedean finset interval mathcomp_extra. +From mathcomp Require Import archimedean finset interval complex mathcomp_extra. (**md**************************************************************************) (* # MathComp extra *) @@ -33,6 +33,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. +Local Open Scope complex_scope. Local Open Scope ring_scope. Section ssralg. @@ -483,3 +484,131 @@ Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R Export -(notations) Morphisms. End ProperNotations. + +(* TODO: backport to real-closed *) +Section complex_extras. +Variable R : rcfType. +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. + +Import Normc. +Import Num.Def. +Import complex. + +Lemma scalecE (w v : C) : v *: w = v * w. +Proof. by []. Qed. + +(* FIXME: unused *) +Lemma normcr (x : R) : normc (x%:C) = normr x. +Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + +Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. +Proof. by simpc. Qed. + +Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). +Proof. +by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx. +Qed. + +Lemma complexA (h : C) : h%:A = h. +Proof. by rewrite scalecE mulr1. Qed. + +Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R. +Proof. by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr normr_nat. Qed. + +Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k. +Proof. +by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul. +Qed. + +Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C. +Proof. +case: r => x y /= /andP[] /eqP -> x0. +by rewrite expr0n addr0 sqrtr_sqr gtr0_norm. +Qed. + +Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C. +Proof. by case: r => x y /andP[] /eqP -> _. Qed. + +Lemma ltc0E (k : R): (0 < k%:C) = (0 < k). +Proof. by simpc. Qed. + +Lemma ltc0P (k : R): (0 < k%:C) <-> (0 < k). +Proof. by simpc. Qed. + +Lemma ltcP (k t: R): (t%:C < k%:C) <-> (t < k). +Proof. by simpc. Qed. + +Lemma lecP (k t: R): (t%:C <= k%:C) <-> (t <= k). +Proof. by simpc. Qed. + +(* (*TBA algC *) *) +Lemma realC_gt0 (d : C) : 0 < d -> (0 < Re d :> R). +Proof. by rewrite ltcE => /andP [] //. Qed. + +Lemma Creal_gtE (c d : C) : c < d -> (complex.Re c < complex.Re d). +Proof. by rewrite ltcE => /andP [] //. Qed. + +Lemma realC_norm (b : R) : `|b%:C| = `|b|%:C. +Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed. + +Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). +Proof. exact: (inj_eq (@complexI _)). Qed. + +Lemma eqCI (r s : R) : (r *i == s *i) = (r == s). +Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed. + +Lemma neqCr0 (r : R) : (r%:C != 0) = (r != 0). +Proof. by apply/negP/negP; rewrite ?eqCr. Qed. + +Lemma real_normc_ler (x : C) : + `|Re x| <= normc x. +Proof. +case: x => x y /=. +rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. +by rewrite lerDl ?sqr_ge0. +Qed. + +Lemma im_normc_ler (x : C) : + `|Im x| <= normc x. +Proof. +case: x => x y /=. +rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. +by rewrite lerDr ?sqr_ge0. +Qed. + +End complex_extras. + +Notation "f %:Rfun" := + (f : (Rcomplex _) -> (Rcomplex _)) + (at level 5, format "f %:Rfun") : complex_scope. + +Notation "v %:Rc" := (v : (Rcomplex _)) + (at level 5, format "v %:Rc") : complex_scope. + +Section algebraic_lemmas. +Variable (R: rcfType). +Notation C := R[i]. +Notation Rcomplex := (Rcomplex R). + +Import Normc. + +Lemma realCZ (a : R) (b : Rcomplex) : a%:C * b = a *: b. +Proof. by case: b => x y; simpc. Qed. + +Lemma realC_alg (a : R) : a *: (1%:Rc) = a%:C. +Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed. + +Lemma scalecr (w: C) (r : R) : r *: (w: Rcomplex) = r%:C *: w . +Proof. by case w => a b; simpc. Qed. + +Lemma scalecV (h: R) (v: Rcomplex): + h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *) +Proof. +by move=> h0 v0; rewrite scalecr invrM // ?unitfE ?eqCr // mulrC scalecr fmorphV. +Qed. + +End algebraic_lemmas. + diff --git a/theories/function_spaces.v b/theories/function_spaces.v index a920e9e63c..8451cadee5 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1557,6 +1557,40 @@ End cartesian_closed. End currying. +Section big_continuous. + +Lemma cvg_big (T : Type) (U : topologicalType) [F : set_system T] [I : Type] + (r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U) + (op : U -> U -> U) (x0 : U): + Filter F -> + continuous (fun x : U * U => op x.1 x.2) -> + (forall i, P i -> Ff i x @[x --> F] --> Fa i) -> + \big[op/x0]_(i <- r | P i) (Ff i x) @[x --> F] --> + \big[op/x0]_(i <- r | P i) Fa i. +Proof. +move=> FF opC0 cvg_f. +elim: r => [|x r IHr]. + rewrite big_nil. + under eq_cvg do rewrite big_nil. + exact: cvg_cst. +rewrite big_cons (eq_cvg _ _ (fun x => big_cons _ _ _ _ _ _)). +case/boolP: (P x) => // Px. +apply: (@cvg_comp _ _ _ (fun x1 => (Ff x x1, \big[op/x0]_(j <- r | P j) Ff j x1)) _ _ (nbhs (Fa x, \big[op/x0]_(j <- r | P j) Fa j)) _ _ (continuous_curry_cvg opC0)). +by apply: cvg_pair => //; apply: cvg_f. +Qed. + +Lemma continuous_big [K T : topologicalType] [I : Type] (r : seq I) + (P : pred I) (F : I -> T -> K) (op : K -> K -> K) (x0 : K) : + continuous (fun x : K * K => op x.1 x.2) -> + (forall i, P i -> continuous (F i)) -> + continuous (fun x => \big[op/x0]_(i <- r | P i) F i x). +Proof. +move=> op_cont f_cont x. +by apply: cvg_big => // i /f_cont; apply. +Qed. + +End big_continuous. + Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y := uncurry (id : continuousType X Y -> (X -> Y)). diff --git a/theories/holomorphy.v b/theories/holomorphy.v index 1d9bc58ea3..abe8cd7144 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -3,10 +3,25 @@ (*Require Import ssrsearch.*) From HB Require Import structures. From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. -From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum ssrfun. -From mathcomp Require Import complex. -From mathcomp Require Import boolp reals ereal derive. -From mathcomp Require Import classical_sets functions interval_inference topology normedtype landau. +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. @@ -18,463 +33,148 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -(* I need to import ComplexField to use its lemmas on RComplex, -I don't want the canonical lmodtype structure on C, -Therefore this is based on a fork of real-closed *) 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) := Uniform.copy (Rcomplex R) R[i]. +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). -HB.howto Rcomplex normedModType 11. -Definition ball : R -> Rcomplex R -> R -> Prop - - ball_center_subproof : forall (x : M) (e : R), 0 < e -> ball x e x - - ball_sym_subproof : forall (x y : M) (e : R), ball x e y -> ball y e x - - ball_triangle_subproof : - forall (x y z : M) (e1 e2 : R), - ball x e1 y -> ball y e2 z -> ball x (e1 + e2)%E z - - entourageE_subproof : entourage = entourage_ ball - -HB.about Uniform_isPseudoMetric.Build. -; NormedZmod_PseudoMetric_eq; - PseudoMetricNormedZmod_Lmodule_isNormedModule - -HB.factory Record Normed_And_Lmodule_isNormedModule (K : numFieldType) R of @Num.NormedZmodule K R & GRing.Lmodule K R := { - normrZ : forall (l : K) (x : R), normr (l *: x) = normr l * normr x; -}. - -HB.builders Context K R of Normed_And_Lmodule_isNormedModule K R. -HB.instance Definition _ := PseudoMetric.copy R (@pseudometric K R). -HB.instance Definition _ := Pointed.copy R R^o. - -Lemma pseudo_metric_ball_norm : ball = ball_ (@normr K R). -Proof. by []. Qed. - -HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K R pseudo_metric_ball_norm. - -HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K R normrZ. -HB.end. - -Lemma normcZ (R : rcfType) (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 _ (R : rcfType) := Normed_And_Lmodule_isNormedModule.Build R (Rcomplex R) (@normcZ R). - -(* TODO: backport to real-closed *) -Section complex_extras. -Variable R : rcfType. -Local Notation sqrtr := Num.sqrt. -Local Notation C := R[i]. - -Import Normc. - -(*Adapting lemma eq_complex from complex.v, which was done in boolean style*) -Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). -Proof. -move=> [a b] [c d]; apply : propositional_extensionality ; split. -by move=> -> ; split. -by case=> //= -> ->. -Qed. - -Lemma Re0 : Re 0 = 0 :> R. -Proof. by []. Qed. - -Lemma Im0 : Im 0 = 0 :> R. -Proof. by []. Qed. - -Lemma ReIm_eq0 (x : C) : (x = 0) = ((Re x = 0) /\ (Im x = 0)). -Proof. by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. Qed. - -Lemma scalei_muli (z : C) : 'i * z = 'i *: z. -Proof. by []. Qed. - -Lemma iE : 'i%C = 'i :> C. -Proof. by []. Qed. - -Lemma scalecM : forall (w v : C), (v *: w = v * w). -Proof. by []. Qed. - -Lemma normc0 : normc 0 = 0 :> R . -Proof. by rewrite /normc //= expr0n //= add0r sqrtr0. Qed. - -Lemma normcN (x : C) : normc (- x) = normc x. -Proof. by case: x => a b /=; rewrite 2!sqrrN. Qed. - -Lemma normcr (x : R) : normc (x%:C) = normr x. -Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. - -Lemma normcR (x : C) : (normc x)%:C = normr x. -Proof. by rewrite /normr /=. Qed. - -Lemma normc_i (x : R) : normc (x*i) = normr x. -Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. - -Lemma normc1 : normc (1 ) = 1 :> R. -Proof. by rewrite /normc/= expr0n addr0 expr1n sqrtr1. Qed. - -Lemma normcN1 : normc (-1%:C) = 1 :> R. -Proof. by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. Qed. - - -Lemma realCD (x y : R) : (x + y)%:C = x%:C + y%:C. -Proof. -(*realC_additive*) -rewrite -!complexr0 eqE_complex //=; by split; last by rewrite addr0. -Qed. - -Lemma realCB (x y : R) : (x - y)%:C = x%:C - y%:C. -Proof. -by rewrite -!complexr0 eqE_complex //=; split; rewrite ?subr0. -Qed. - -Lemma Inv_realC (x : R) : x%:C^-1 = (x^-1)%:C. -Proof. -have [/eqP->|x0] := boolP (x == 0); first by rewrite !invr0. -apply/eqP; rewrite eq_complex /= mul0r oppr0 eqxx andbT expr0n addr0. -by rewrite expr2 invrM ?unitfE // mulrA divrr ?unitfE // div1r. -Qed. - -Lemma CimV : ('i%C)^-1 = (-1 *i) :> C. -Proof. by rewrite complexiE invCi. Qed. - -Lemma invcM (x y : C) : (x * y)^-1 = x^-1 * y^-1. -Proof. -have [/eqP->|x0] := boolP (x == 0); first by rewrite !(invr0,mul0r). -have [/eqP->|y0] := boolP (y == 0); first by rewrite !(invr0,mulr0). -by rewrite invrM // mulrC. -Qed. - -Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. -Proof. by simpc. Qed. - -Lemma normcD (x y : C) : normc (x + y) <= normc x + normc y. -Proof. by rewrite -lecR realCD; apply: lec_normD. Qed. - -Lemma normc_ge0 (x : C) : 0 <= normc x. -Proof. case: x => ? ?; exact: sqrtr_ge0. Qed. - -Lemma normc_gt0 (v : C) : (0 < normc v) = (v != 0). -Proof. -rewrite lt_neqAle normc_ge0 andbT; apply/idP/idP; apply/contra. -by move/eqP ->; rewrite normc0. -by rewrite eq_sym => /eqP/eq0_normc ->. -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 realCM (a b :R) : a%:C * b%:C = (a * b)%:C. -Proof. by rewrite eqE_complex /= !mulr0 mul0r addr0 subr0. Qed. - -Lemma complexA: forall (h : C), h%:A = h. -Proof. by move => h; rewrite scalecM mulr1. Qed. - -Lemma lecM (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 normc_natmul (k : nat) : normc k%:R = k%:R :> R. -Proof. -by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr ger0_norm // ler0n. -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. -move=> r0; have rr : r \is Num.real by rewrite realE (ltW r0). -rewrite /normc (complexE r) /=; simpc. -rewrite (ger0_Im (ltW r0)) expr0n addr0 sqrtr_sqr gtr0_norm ?complexr0 //. -by move: r0; rewrite {1}(complexE r) /=; simpc => /andP[/eqP]. -Qed. - -Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C. -Proof. -by move=> r0; rewrite eqE_complex /=; split; last by apply: ger0_Im; apply: ltW. -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. - -Lemma complex_pos (r : {posnum C}) : 0 < (Re r%:num). -Proof. by rewrite -ltc0E -gt0_realC. 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. rewrite ltcE => /andP [] //. Qed. - -Canonical complex_Re_posnum (x : {posnum C}) := PosNum (complex_pos x). - -Lemma realC_pos_gt0 (r : {posnum R}) : 0 < (r%:num)%:C. -Proof. by rewrite ltcR. Qed. - -Canonical realC_posnum (x : {posnum R}) := PosNum (realC_pos_gt0 x). - -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 realCV (*name ?*) (h: R) : h != 0 -> (h^-1)%:C = h%:C^-1. -Proof. -rewrite eqE_complex //=; split; last by rewrite mul0r oppr0. -by rewrite expr0n //= addr0 -exprVn expr2 mulrA mulrV ?unitfE ?mul1r //=. -Qed. - - -Lemma real_normc_ler (x y : R) : - `|x| <= normc (x +i* y). -Proof. -rewrite /normc /= -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 y : R) : - `|y| <= normc (x +i* y). -Proof. -rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. -rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. -by rewrite lerDr ?sqr_ge0. +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. -End complex_extras. - -Lemma filter_compE ( T U V : topologicalType) - (f : T -> U) (g : V -> T) - (F : set_system V) : - (f @ (g @ F))= (f \o g @ F). -Proof. by []. Qed. - -Lemma within_continuous_withinNx - (R C : numFieldType) (U : normedModType C) (f : U -> R) : - {for (0 : U), continuous f} -> - (forall x, f x = 0 -> x = 0) -> f @ dnbhs (0 :U) --> dnbhs (0 : R). -Proof. - move => cf f0 A /=. -(*rewrite !/nbhs /= /nbhs /= /within /= !nearE => [].*) Admitted. - -Notation "f %:Rfun" := - (f : (Rcomplex _ : normedModType _) -> (Rcomplex _ : normedModType _)) - (at level 5, format "f %:Rfun") : complex_scope. - -Notation "v %:Rc" := (v : (Rcomplex _)) - (at level 5, format "v %:Rc") : complex_scope. +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. -Section algebraic_lemmas. -Variable (R: realType). -Notation C := R[i]. -Notation Rcomplex := (Rcomplex R). - -Import Normc. - -Lemma realCZ (a : R) : forall (b : Rcomplex), a%:C * b = a *: b. -Proof. by move => [x y]; rewrite /(_ *: _) /=; simpc. Qed. - -Lemma realC_alg (a : R) : a *: (1%:Rc) = a%:C. +Lemma normcZ (l : R) (x : Rcomplex R) : `|l *: x| = `|l| * `|x|. Proof. -apply/eqP; rewrite eq_complex; apply/andP. -by split; simpl; apply/eqP; rewrite ?mulr1 ?mulr0. +by case: x => ??; rewrite /normr/= !exprMn -mulrDr sqrtrM ?sqr_ge0// sqrtr_sqr. Qed. -Lemma scalecr: forall w: C, forall r : R, r *: (w: Rcomplex) = r%:C *: w . -Proof. -Proof. by move=> [a b] r; rewrite eqE_complex //=; split; 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 realCV. +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. -Lemma complex0 : 0%:C = 0 :> C. -Proof. rewrite eqE_complex //=. Qed. - +HB.instance Definition _ := + Lmodule_hasFinDim.Build R (Rcomplex R) Rcomplex_findim. -End algebraic_lemmas. - - -(* Section complex_topological. -Variable R : realType. -Local Notation C := R[i]. - -Canonical complex_pointedType := - [pointedType of C for pointed_of_zmodule [zmodType of C]]. -Canonical complex_filteredType := - [filteredType C of C for filtered_of_normedZmod [normedZmodType C of C]]. -Canonical complex_topologicalType := - TopologicalType C - (topologyOfEntourageMixin - (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType C of C]) - (pseudoMetric_of_normedDomain [normedZmodType C of C]))). -Canonical numFieldType_uniformType := UniformType C - (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType C of C]) - (pseudoMetric_of_normedDomain [normedZmodType C of C])). -Canonical numFieldType_pseudoMetricTyp - := @PseudoMetric.Pack [numDomainType of C] C (@PseudoMetric.Class [numDomainType of C] C - (Uniform.class [uniformType of C]) - (@pseudoMetric_of_normedDomain [numDomainType of C] [normedZmodType C of C])). - -Canonical complex_lmodType := - [lmodType R[i] of R[i] for [lmodType R[i] of R[i]^o]]. - -Canonical complex_lalgType := [lalgType C of C for [lalgType C of C^o]]. -Canonical complex_algType := [algType C of C for [algType C of C^o]]. -Canonical complex_comAlgType := [comAlgType C of C]. -Canonical complex_unitAlgType := [unitAlgType C of C]. -Canonical complex_comUnitAlgType := [comUnitAlgType C of C]. -Canonical complex_vectType := [vectType C of C for [vectType C of C^o]]. -Canonical complex_FalgType := [FalgType C of C]. -Canonical complex_fieldExtType := - [fieldExtType C of C for [fieldExtType C of C^o]]. - -Canonical complex_pseudoMetricNormedZmodType := - [pseudoMetricNormedZmodType C of C for - [pseudoMetricNormedZmodType C of [numFieldType of C^o]]]. -Canonical complex_normedModType := - [normedModType C of C for [normedModType C of C^o]]. - -End complex_topological. *) +End Rcomplex_NormedModType. Section Holomorphe_der. Variable R : realType. Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. -Notation Rc := (Rcomplex R). - -Lemma is_cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set_system T) (H : Filter F) (f : T -> V) (k : K) : - cvg (f @ F) -> cvg ((k \*: f) @ F ). -Proof. by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. Qed. - -Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set_system T) (FF : ProperFilter F) (f : T -> V) (k : K) : - cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). -Proof. by move => cv; apply/esym/cvg_lim => //; apply: cvgZr. Qed. +Local Notation Rc := (Rcomplex R). -Definition holomorphic (f : C-> C ) (c : C) := - cvg ((fun h => h^-1 *: (f (c + h) - f c)) @ (dnbhs (0:C))). +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. +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))) = +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. +by apply: funext => h; rewrite complexA [X in f X]addrC. Qed. -Definition Rdifferentiable (f : C -> C) (c : C) := (differentiable f%:Rfun c%:Rc). - -(* No Rmodule structure on C if we can avoid, -so the following line shouldn't type check. *) -Fail Definition Rderivable_fromcomplex_false (f : C -> C) (c v: C) := - cvg (fun (h : R) => h^-1 *: (f (c +h *: v) - f c)) @ (dnbhs (0:R)). +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); first by []. -by move => z /= nz; apply: (H (realC z)); rewrite /= -realCB realC_norm rRe ltcR. +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 @ (dnbhs 0))) - = 'D_1 (f%:Rfun) c%:Rc :> C. + lim ((fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ 0^')) + = 'D_1 (f%:Rfun) c%:Rc. Proof. rewrite /derive. -have -> : (fun h : C => h^-1 *: ((f (c + h) - f c))) @ (realC @ (dnbhs 0)) = - (fun h : C => h^-1 *: ((f (c + h) - f c))) - \o realC @ (dnbhs (0 : R)) by []. -suff -> : ( (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC) -= (fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c : Rcomplex _) ) :> (R -> C) . -STOP. -rewrite /=. -f_equal => /=. -Set Printing All. -Search lim Logic.eq . -Search (lim _ = lim _). -Set Printing All. -apply: lim_eq. - admit. +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 Inv_realC /= -!scalecr realC_alg [X in f X]addrC. -Admitted. - +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 @ (dnbhs (0 )))) - = 'D_('i) (f%:Rfun) c%:Rc :> C. + lim ((fun h : C => h^-1 *: ((f (c + h * 'i) - f c))) @ (realC @ 0^')) + = 'D_('i) (f%:Rfun) c%:Rc. Proof. rewrite /derive. -have -> : - ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) @ (realC @ dnbhs 0)) - = ((fun h : (R[i]) => h^-1 *: (f (c + h * 'i) - f c)) \o realC) @ dnbhs 0 by []. -suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o -realC = fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: ('i%:Rc)) - f c : Rcomplex _). - admit. +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 Inv_realC -scalecM -!scalecr realCZ [X in f X]addrC. -Admitted. +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 (E : normedModType C) (h e : E -> C) (x : E) : - [o_x (e : E -> C) of (h : E -> C)] = - [o_x (e : E -> Rc) of (h : E -> Rc)]. +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 : E -> C) =o_x (e : E -> C) <-> - (h : E -> Rc) =o_x (e : E -> Rc). - have [ho|hNo] := asboolP ((h : E -> C) =o_x (e : E -> C)). +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/= !normcR rmorphM/=. + rewrite -lecR/= rmorphM/=. near: y. - exact: small. -rewrite -[_%:num]ger0_norm// -!normcR -rmorphM/= lecR. -by near: y; apply: small; rewrite normc_gt0//. + 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. -(*extremely long with modified filteredType *) - 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 holo_differentiable (f : C -> C) (c : C) : holomorphic f c -> Rdifferentiable f c. @@ -482,123 +182,90 @@ 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). -have cdf : continuous df'. - admit. +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 holo littleoCo. - admit. -by apply/diff_locallyP; rewrite (diff_unique cdf eqdf). -Admitted. - -(*The equality between 'i as imaginaryC from ssrnum and 'i is not transparent: - neq0ci is part of ssrnum and uneasy to find *) + 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. +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 @ dnbhs 0) = (quotR \o realC) @ dnbhs 0 by []. -have realC'0: realC @ dnbhs 0 --> dnbhs 0. - apply: within_continuous_withinNx; first by apply: continuous_realC. - by move => /= x /complexI. -have HR0:(quotC \o (realC) @ dnbhs 0) --> l. +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 @ (dnbhs (0 : R))) --> l. +have lem : quotC \o *%R^~ 'i%R @ (realC @ (0 : R)^') --> l. apply: cvg_comp; last by exact: H. - rewrite (filter_compE _ realC); apply: cvg_comp; first by exact: realC'0. - apply: within_continuous_withinNx; first by apply: scalel_continuous. - move => x /eqP; rewrite mulIr_eq0 ; last by apply/rregP; apply: neq0Ci. - by move/eqP. -have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ (dnbhs (0 : R)))) . - by apply/cvg_ex; simpl; exists l. -have ->: lim (quotR @ (realC @ (dnbhs (0 : R)))) - = 'i *: lim (quotC \o ( fun h => h *'i) @ (realC @ (dnbhs (0 : R)))). + 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 invcM scalerA mulrC -mulrA mulVf ?mulr1 ?neq0Ci //. - by move => /funext <-; rewrite (limin_scaler _ 'i HRcomp). -rewrite scalecM. -suff: lim (quotC @ (realC @ (dnbhs (0 : R)))) - = lim (quotC \o *%R^~ 'i%R @ (realC @ (dnbhs (0 : R)))) by move => -> . -suff -> : lim (quotC @ (realC @ (dnbhs (0 : R)))) = l. + 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. +by apply: cvg_lim; last exact: HR0. Qed. - -(*TBA normedType- Cyril's suggestion *) -Lemma dnbhs0_le (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (dnbhs (0 : V)), `|x| <= e. +Lemma Diff_CR_holo (f : C -> C) (c : C): + (Rdifferentiable f c) /\ (CauchyRiemannEq f c) -> (holomorphic f c). Proof. -move=> e_gt0; apply/nbhs_ballP; exists e => // x. -rewrite -ball_normE /= sub0r normrN => le_nxe _ . -by rewrite ltW. -Qed. - -Lemma nbhs0_le (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (dnbhs (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 (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (dnbhs (0 : V)), `|x| < e. -Proof. -move=> e_gt0; apply/nbhs_ballP; exists e => // x. -by rewrite -ball_normE /= sub0r normrN. -Qed. - -Lemma nbhs0_lt (K : numFieldType) (V : normedModType K) e : - 0 < e -> \forall x \near (dnbhs (0 : V)), `|x| < e. -Proof. -move=> e_gt0; apply/nbhs_ballP; exists e => // x. -by rewrite -ball_normE /= sub0r normrN. -Qed. - -Lemma normc_ge_Im (x : R[i]) : `|complex.Im x|%:C <= `|x|. -Proof. -by case: x => a b; simpc; rewrite -sqrtr_sqr ler_wsqrtr // ler_addr sqr_ge0. -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. +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 scalecM. -pose df : {linear R[i] -> R[i]} := HB.pack Df (GRing.isLinear.Build _ _ _ _ Df lDf). +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 scalecM [in RHS]mulrC. + 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) -scalecM !scalecr /=. + 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 diff /= lem. - admit. +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). -Admitted. +(* 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 by apply: Diff_CR_holo. - split; first by apply: holo_differentiable. - by apply: holo_CauchyRiemann. +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 4c2377f0b1..77ff6ccc6f 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -20,6 +20,9 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. (* normedModType K == interface type for a normed module *) (* structure over the numDomainType K *) (* The HB class is NormedModule. *) +(* normedVectType K == interface type for a normed vectType *) +(* structure over the numDomainType K *) +(* The HB class is NormedVector. *) (* `|x| == the norm of x (notation from ssrnum.v) *) (* ``` *) (* *) @@ -140,6 +143,10 @@ HB.instance Definition _ := HB.end. +#[short(type="normedVectType")] +HB.structure Definition NormedVector (K : numDomainType) := + {T of NormedModule K T & Vector K T}. + (**md see also `Section standard_topology_pseudoMetricNormedZmod` in `pseudometric_normed_Zmodule.v` *) Section standard_topology_normedMod. @@ -334,6 +341,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. @@ -2012,104 +2049,231 @@ HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K M End isnormedmodule. -HB.factory Record Lmodule_isNormed (R : numFieldType) M - of GRing.Lmodule R M := { - norm : M -> R; - ler_normD : forall x y, norm (x + y) <= norm x + norm y ; -(* normrMn : forall x n, norm (x *+ n) = norm x *+ n ;*) - normrN : forall x, norm (- x) = norm x ; - normrZ : forall (l : R) (x : M), norm (l *: x) = `|l| * norm x ; - normr0_eq0 : forall x : M, norm x = 0 -> x = 0 -}. - -HB.builders Context R M of Lmodule_isNormed R M. - -(*HB.about Num.Zmodule_isNormed.Build.*) - -Lemma normrMn x n : norm (x *+ n) = norm x *+ n. -Proof. -have := normrZ n%:R x. -rewrite ger0_norm// mulr_natl => <-. -by rewrite scaler_nat. -Qed. - -HB.instance Definition _ := Num.Zmodule_isNormed.Build - R M ler_normD normr0_eq0 normrMn normrN. - -Check M : normedZmodType R. - -Check (@pseudometric R M). +Section InfiniteNorm. +Variables (R : numFieldType) (V : vectType R) (B : (\dim (@fullv _ V)).-tuple V). +Let V' := @fullv _ V. +Hypothesis (Bbasis : basis_of V' B). -HB.saturate pseudometric. +(* FIXME: Check naming. *) +Definition oo_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. -Check (pseudometric M : pseudoMetricType R). +Definition oo_space : Type := (fun=> V) Bbasis. -HB.instance Definition _ := PseudoMetric.copy M (pseudometric M). -HB.instance Definition _ := isPointed.Build M 0. +HB.instance Definition _ := Vector.on oo_space. -Local Lemma NormedZmod_PseudoMetric_eq_pseudometric - : NormedZmod_PseudoMetric_eq R M. -Proof. by constructor. Qed. +HB.instance Definition _ := Pointed.copy oo_space V^o. -HB.instance Definition _ := NormedZmod_PseudoMetric_eq_pseudometric. - -Lemma PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric - : PseudoMetricNormedZmod_Lmodule_isNormedModule R M. -Proof. by constructor; exact: normrZ. Qed. - -HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric. - -Check M : normedModType R. - -HB.end. - -HB.factory Record Uniform_Lmodule_isNormed (R : numFieldType) M of Uniform M & GRing.Lmodule R M := { - norm : M -> R; - ler_normD : forall x y, norm (x + y) <= norm x + norm y ; - normrZ : forall (l : R) (x : M), norm (l *: x) = `|l| * norm x ; - normr0_eq0 : forall x : M, norm x = 0 -> x = 0 ; - entourage_norm : forall x : M, nbhs_ball_ (ball_ norm) x = filter.nbhs x; -}. - -HB.builders Context R M of Uniform_Lmodule_isNormed R M. - -Lemma normrMn (x : M) (n : nat) : norm (x *+ n) = norm x *+ n. +Lemma oo_norm_ge0 x : 0 <= oo_norm x. Proof. - admit. -Admitted. - - -Lemma normrN (x : M) : norm (- x) = norm x. -Proof. admit. Admitted. - -HB.instance Definition _ := Num.Zmodule_isNormed.Build R M ler_normD normr0_eq0 normrMn normrN. -HB.instance Definition _ := isPointed.Build M 0. - -Definition ball := ball_ (fun x : M => `|x|). - -Lemma ball_center_subproof (x : M) (e : R) : 0 < e -> ball x e x. -Proof. by rewrite /ball /ball_/= subrr normr0. Qed. - -Lemma ball_sym_subproof (x y : M) (e : R) : ball x e y -> ball y e x. -Proof. by rewrite /ball /ball_/= distrC. Qed. +rewrite /oo_norm. +elim: (index_enum _) => /=; first by rewrite big_nil. +by move=> i l IHl; rewrite big_cons /Order.max/=; case: ifP. +Qed. -Lemma ball_triangle_subproof (x y z : M) (e1 e2 : R) : - ball x e1 y -> - ball y e2 z -> - ball x (e1 + e2)%E z. +Lemma le_coord_oo_norm x i : `|coord B i x| <= oo_norm x. Proof. -rewrite /ball /ball_/= => ? ?. -rewrite -[x](subrK y) -(addrA (x + _)). -by rewrite (le_lt_trans (ler_normD _ _))// ltrD. +rewrite /oo_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. +rewrite inE big_cons /Order.max/= => /orP[/eqP <-|/IHl {}IHl]; case: ifP => [/ltW|]//. +move=> /negP/negP. +have bR: \big[Order.max/0]_(i <- l) `|coord B i x| \is Num.real. + exact: bigmax_real. +move: (real_comparable bR (normr_real (coord B j x))). +by move=> /comparable_leNgt <- /(le_trans IHl). Qed. -Lemma entourageE_subproof : entourage = entourage_ ball. -Proof. admit. Admitted. - -HB.instance Definition _ := Uniform_isPseudoMetric.Build R M ball_center_subproof ball_sym_subproof ball_triangle_subproof entourageE_subproof. - -HB.about NormedZmod_PseudoMetric_eq.Build. -; PseudoMetricNormedZmod_Lmodule_isNormedModule +Lemma ler_oo_normD x y : oo_norm (x + y) <= oo_norm x + oo_norm y. +Proof. +apply: bigmax_le => [|/= i _]. + by apply: addr_ge0; apply: oo_norm_ge0. +rewrite raddfD/=. +by apply/(le_trans (ler_normD _ _))/lerD; apply: le_coord_oo_norm. +Qed. + +Lemma oo_norm0_eq0 x : oo_norm x = 0 -> x = 0. +Proof. +move=> x0. +rewrite (coord_basis Bbasis (memvf x)). +suff: forall i, coord B i x = 0. + move=> {}x0. + under eq_bigr do rewrite x0. + by rewrite -scaler_sumr scale0r. +move=> i; apply/normr0_eq0/le_anti/andP; split; last exact: normr_ge0. +by rewrite -x0; apply: le_coord_oo_norm. +Qed. + +Lemma oo_normZ r x : oo_norm (r *: x) = `|r| * oo_norm x. +Proof. +rewrite /oo_norm. +under eq_bigr do rewrite linearZ normrZ/=. +elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0. +by rewrite !big_cons IHl maxr_pMr. +Qed. + +Lemma oo_normMn x n : oo_norm (x *+ n) = oo_norm x *+ n. +Proof. by rewrite -scaler_nat oo_normZ normr_nat mulr_natl. Qed. + +Lemma oo_normN x : oo_norm (- x) = oo_norm x. +Proof. by rewrite -scaleN1r oo_normZ normrN1 mul1r. Qed. + +HB.instance Definition _ := Num.Zmodule_isNormed.Build R oo_space ler_oo_normD oo_norm0_eq0 oo_normMn oo_normN. + +HB.instance Definition _ := PseudoMetric.copy oo_space (pseudometric oo_space). + +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R oo_space erefl. + +HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R oo_space oo_normZ. + +End InfiniteNorm. + +Section EquivalenceNorms. +Variables (R : realType) (V : vectType R). +Let V' := @fullv _ V. +Let Voo := oo_space (vbasisP (@fullv _ V)). + +(* N.B. Get Trocq to prove the continuity part automatically. *) +Lemma oo_closed_ball_compact : compact (closed_ball (0 : Voo) 1). +Proof. +rewrite closed_ballE/closed_ball_//=. +under eq_set do rewrite sub0r normrN. +rewrite -[forall x, _]/(compact _). +pose f (X : {ptws 'I_(\dim V') -> R^o}) : Voo := \sum_(i < \dim V') (X i) *: (vbasis V')`_i. +have -> : [set x : Voo | `|x| <= 1] = f @` [set X | forall i, `[-1, 1]%classic (X i)]. + apply/seteqP; split=> x/=. + move=> x1; exists (fun i => coord (vbasis V') i x); last first. + exact/esym/(@coord_vbasis _ _ (x : V))/memvf. + move=> i; rewrite in_itv/= -ler_norml. + apply: (le_trans _ x1). + exact: le_coord_oo_norm. + move=> [X] X1 <-. + rewrite /normr/=/oo_norm. + apply: bigmax_le => //= i _. + rewrite coord_sum_free; last exact/basis_free/vbasisP. + rewrite ler_norml. + exact: X1. +apply: (@continuous_compact _ _ f); last first. + apply: (@tychonoff 'I_(\dim V') (fun=> R^o) (fun=> `[-1, 1 : R^o]%classic)). + move=> _. + exact: segment_compact. +apply/continuous_subspaceT/sum_continuous => i _/= x. +exact/continuousZl/proj_continuous. +Qed. + +Lemma equivalence_norms (N : V -> R) : + N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) -> (forall x y, N (x + y) <= N x + N y) -> + (forall r x, N (r *: x) = `|r| * N x) -> + exists M, 0 < M /\ forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. +Proof. +move=> N0 N_ge0 N0_eq0 ND NZ. +set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i. +have N_sum (I : Type) (r : seq I) (F : I -> V): + N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i). + elim: r => [|x r IHr]; first by rewrite !big_nil N0. + by rewrite !big_cons; apply/(le_trans (ND _ _))/lerD. +have leNoo: forall x : Voo, N x <= M0 * `|x|. + move=> x. + rewrite [in leLHS](coord_vbasis (memvf (x : V))). + apply: (le_trans (N_sum _ _ _)). + rewrite mulrDl mul1r mulr_suml -[leLHS]add0r. + apply: lerD => //. + apply: ler_sum => /= i _. + rewrite NZ mulrC; apply: ler_pM => //. + exact: le_coord_oo_norm. +have M00 : 0 < M0. + rewrite -[ltLHS]addr0. + by apply: ltr_leD => //; apply: sumr_ge0. +have NC0 : continuous (N : Voo -> R). + move=> /= x. + rewrite /continuous_at. + apply: cvg_zero; first exact: nbhs_filter. + apply/cvgr0Pnorm_le; first exact: nbhs_filter. + move=> /= e e0. + near=> y. + rewrite -[_ y]/(N y - N x). + apply: (@le_trans _ _ (N (y - x))). + apply/real_ler_normlP. + by apply: realB; apply: ger0_real. + have NB a b : N a <= N b + N (a - b). + by rewrite -[a in N a]addr0 -(subrr b) addrCA ND. + rewrite opprB !lerBlDl; split; last exact: NB. + by rewrite -opprB -scaleN1r NZ normrN1 mul1r NB. + apply: (le_trans (leNoo _)). + rewrite mulrC -ler_pdivlMr// -opprB normrN. + near: y; apply: cvgr_dist_le; first exact: cvg_id. + exact: divr_gt0. +have: compact [set x : Voo | `|x| = 1]. + apply: (subclosed_compact _ oo_closed_ball_compact); last first. + apply/subsetP => x. + rewrite closed_ballE// !inE/=. + by rewrite /closed_ball_/= sub0r normrN => ->. + apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq. + by rewrite /prop_in1 => + _; apply: norm_continuous. +move=> /(@continuous_compact _ _ (N : Voo -> R)) -/(_ _)/wrap[]. + exact: continuous_subspaceT. +move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[]. + move=> /= x. + rewrite /continuous_at. + apply: (@continuous_in_subspaceT _ _ [set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)). + move=> r /set_mem/=[] y y1 <-. + apply: inv_continuous. + apply/negP => /eqP/N0_eq0 y0. + move: y1; rewrite y0 normr0 => /esym. + by move: (@oner_neq0 R) => /eqP. +move=> /compact_bounded[] M1 [] M1R /(_ (1 + M1)). +rewrite -subr_gt0 -addrA subrr addr0 => /(_ ltr01). +rewrite /globally/= => M1N. +exists (maxr M0 (1 + M1)). +split=> [|x]; first by apply: (lt_le_trans M00); rewrite le_max lexx. +split; last first. + apply/(le_trans (leNoo x))/ler_pM => //; first exact/ltW. + by rewrite /maxr; case: ifP => // /ltW. +have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0. +have Nx0: 0 < N x. + rewrite lt0r N_ge0 andbT. + by move: x0; apply: contra => /eqP/N0_eq0/eqP. +have normx0 : 0 < `|x|. + move: (lt_le_trans Nx0 (leNoo x)). + by rewrite pmulr_rgt0. +move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[]. + exists (N x / `|x|); last by rewrite invf_div. + exists (`|x|^-1 *: x); last first. + by rewrite NZ mulrC ger0_norm. + rewrite normrZ mulrC ger0_norm. + by rewrite divrr//; apply: unitf_gt0. + by rewrite invr_ge0; apply: ltW. +rewrite ger0_norm; last exact: divr_ge0. +rewrite ler_pdivrMr// => xle. +apply: (le_trans xle). +rewrite -subr_ge0 -mulrBl pmulr_lge0// subr_ge0. +by rewrite le_max lexx orbT. +Unshelve. all: by end_near. +Qed. + +End EquivalenceNorms. + +Section LinearContinuous. +Variables (R : realType) (V : normedVectType R) (W : normedModType R). + +Lemma linear_findim_continuous (f : {linear V -> W}) : continuous f. +Proof. +set V' := @fullv _ V. +set B := vbasis V' => /= x. +rewrite /continuous_at. +rewrite [x in f x](coord_vbasis (memvf x)) raddf_sum. +rewrite (@eq_cvg _ _ _ _ (fun y => \sum_(i < \dim V') coord B i y *: f B`_i)); last first. + move=> y; rewrite [y in LHS](coord_vbasis (memvf y)) raddf_sum. + by apply: eq_big => // i _; apply: linearZ. +apply: cvg_sum => i _. +rewrite [X in _ --> X]linearZ/= -/B. +apply: cvgZl. +move: x; apply/linear_bounded_continuous/bounded_funP => r/=. +have := @equivalence_norms R V (@normr R V) (@normr0 _ _) (@normr_ge0 _ _) (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _). +move=> [] M [] M0 MP. +exists (M * r) => x. +move: MP => /(_ x)[] Mx Mx' xr. +apply/(le_trans (le_coord_oo_norm _ _ _))/(le_trans Mx). +rewrite -subr_ge0 -mulrBr; apply: mulr_ge0; first exact: ltW. +by rewrite subr_ge0. +Qed. + +End LinearContinuous. -HB.howto M normedModType. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 7a213364c3..1ce675f1d9 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -83,6 +83,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 611643c7da..7e8a9fdbc1 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -284,6 +284,26 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y. by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. Unshelve. all: by end_near. 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), [/\ diff --git a/theories/tvs.v b/theories/tvs.v index fe43593043..045240c712 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -90,6 +90,22 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. +Section TopologicalNmodule_Theory. + +Lemma cvg_sum (T : Type) (U : TopologicalNmodule.type) (F : set_system T) + (I : Type) (r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U) : + Filter F -> (forall i, P i -> Ff i x @[x --> F] --> Fa i) -> + \sum_(i <- r | P i) Ff i x @[x --> F] --> \sum_(i <- r| P i) Fa i. +Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed. + +Lemma sum_continuous (T : topologicalType) (M : TopologicalNmodule.type) + (I : Type) (r : seq I) (P : pred I) (F : I -> T -> M) : + (forall i : I, P i -> continuous (F i)) -> + continuous (fun x1 : T => \sum_(i <- r | P i) F i x1). +Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. + +End TopologicalNmodule_Theory. + HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}. @@ -273,6 +289,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) := @@ -514,6 +551,16 @@ rewrite /ball /ball_/= => xy /= [nx ny]. by rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (splitr e) ltrD. Qed. +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). Proof. (* NB: This lemma is proved once again in normedtype, in a shorter way with much more machinery *) @@ -591,6 +638,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 _ := Uniform_isTvs.Build R R^o standard_locally_convex. From 7e22e2cb82ef6aa9d8f7d3c3cf3843b57d71fde4 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 3 Jun 2025 19:33:23 +0200 Subject: [PATCH 10/10] typo and changelog --- CHANGELOG_UNRELEASED.md | 45 +++++++++++++++++++++++++++++++++++++++++ theories/holomorphy.v | 1 + 2 files changed, 46 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 699bb89453..d709d8ed0e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -52,6 +52,51 @@ - in `lebesgue_integral_differentiation.v`: + lemma `nicely_shrinking_fin_num` +- in `unstable.v` + + lemmas `scalecE`, `normcr`, `Im_mul`, `mulrnc`, `complexA`, `normc_natmul`, + `nomrc_mulrn`, `gt0_normc`, `gt0_realC`, `ltc0E`, `ltc0P`, `ltcP`, `lecP`, + `realC_gt0`, `Creal_gtE`, `realC_norm`, `eqCr`, `eqCI`, `neqCr0`, + `real_normc_ler`, `im_normc_ler` + + notations `f %:Rfun`, `v %:Rc` + + lemmas `realCZ`, `realC_alg`, `scalecr`, `scalecV` + +- in `function_spaces.v` + + lemmas `cvg_big`, `continuous_big` + +- file `holomorphy.v` + + instance of `normedModType` on `complex` + + definition `ball_Rcomplex` + + lemmas `entourage_RcomplexE`, `normcZ`, `Rcomplex_findim` + + instance of `normedVectType` on `complex` + + definitions `holomorphic`, `Rdifferentiable`, `realC`, `CauchyRiemannEq` + + lemmas `holomorphicP`, `continuous_realC`, `Rdiff1`, `Rdiffi`, `littleoCo`, + `holo_differentiable`, `holo_CauchyRiemann`, `Diff_CR_holo`, + `holomorphic_Rdiff` + +- in `landau.v` + + lemma `littleoE0` + +- in `normed_module.v` + + structure `normedVectType` + + lemmas `dnbhs0_le`, `nbhs0_le`, `dnbrg0_lt`, `nbhs0_lt` + + definition `pseudometric` + + instance of `normedZmodType`, `pointedType` and `pseudoMetricType` + on `pseudometric` + + definitions `oo_norm`, `oo_space`, + + instance of `normedModType` on `oo_space` + + lemmas `oo_closed_ball_compact`, `equivalence_norms`, + `linear_findim_continuous` + +- in `num_topology.v` + + instance of `pseudoMetricType` on `GRing.regular` + +- in `uniform_structure` + + lemma `within_continuous_withinNx` + +- in `tvs.v` + + lemmas `cvg_sum`, `sum_continuous`, `entourage_nbhsE` + + instance of `UniformZmodule.type` on `GRing.regular` + ### Changed - in `convex.v`: diff --git a/theories/holomorphy.v b/theories/holomorphy.v index abe8cd7144..e9263dd257 100644 --- a/theories/holomorphy.v +++ b/theories/holomorphy.v @@ -97,6 +97,7 @@ HB.instance Definition _ := Lmodule_hasFinDim.Build R (Rcomplex R) Rcomplex_findim. End Rcomplex_NormedModType. +End Rcomplex_NormedModType. Section Holomorphe_der. Variable R : realType.