From 5fa3027a9fb7caabcb4c655758ef54dc9a8b36a0 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 18 Jun 2021 10:52:24 +0900 Subject: [PATCH 1/2] scratch on power series --- theories/power_series.v | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 theories/power_series.v diff --git a/theories/power_series.v b/theories/power_series.v new file mode 100644 index 000000000..6f16ddf23 --- /dev/null +++ b/theories/power_series.v @@ -0,0 +1,41 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. +From mathcomp Require Import matrix interval rat. +Require Import boolp reals ereal. +Require Import classical_sets posnum topology normedtype landau sequences. + +(******************************************************************************) +(* Definitions and lemmas about power series *) +(* *) +(* The purpose of this file is to gather generic definitions and lemmas about *) +(* power series. *) +(* Definitions: *) +(* ??? == notation for power series, *) +(* ??? == radius of convergence *) +(* *) +(******************************************************************************) + +(* Power series *) +(* we want a notation for the following pattern: + series (fun i => f i * x ^+ i) *) + +power_series f := series (fun i => f i * 'X ^ i) +fun_defined_by_power_series f := lim (series (fun i => f i * 'X ^+ i)) + +for a power_series ps, +ps.[(x:R)] := series (fun i => (ps i).[x]) + + +(* possible example usage *) +Definition exp_coeff' := [sequence 1 / n`!%:R]_n. +Definition expR := [power_series exp_coeff']. + +Lemma power_series_has_a_radius_of_convergence : + forall ps : power_series_T, exists rad : R, + (forall x, x < rad -> cvg ps.[x]) /\ + (forall x, x > rad -> ~ cvg ps.[x]). + +Definition radius_of_convergence (ps : power_series_T) : R := + get (power_series_has_a_radius_of_convergence ps). (* = rad *) + +Lemma ratio_test : ... From 37d27a9a37fd25808a630cb3f101ae305b5fbc37 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 18 Jun 2021 13:44:31 +0900 Subject: [PATCH 2/2] type-check definitions for the sake of discussion Co-Authored-By: Takafumi Saikawa --- theories/power_series.v | 96 +++++++++++++++++++++++++++++++---------- 1 file changed, 74 insertions(+), 22 deletions(-) diff --git a/theories/power_series.v b/theories/power_series.v index 6f16ddf23..f2f565940 100644 --- a/theories/power_series.v +++ b/theories/power_series.v @@ -1,41 +1,93 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. -From mathcomp Require Import matrix interval rat. +From mathcomp Require Import matrix interval rat poly. Require Import boolp reals ereal. Require Import classical_sets posnum topology normedtype landau sequences. (******************************************************************************) -(* Definitions and lemmas about power series *) +(* This file is a scratch file with the goal of defining power series (wip). *) (* *) -(* The purpose of this file is to gather generic definitions and lemmas about *) -(* power series. *) (* Definitions: *) (* ??? == notation for power series, *) -(* ??? == radius of convergence *) +(* ??? == radius of convergence *) (* *) (******************************************************************************) -(* Power series *) -(* we want a notation for the following pattern: - series (fun i => f i * x ^+ i) *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. -power_series f := series (fun i => f i * 'X ^ i) -fun_defined_by_power_series f := lim (series (fun i => f i * 'X ^+ i)) +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. -for a power_series ps, -ps.[(x:R)] := series (fun i => (ps i).[x]) +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Reserved Notation "p `.[ x ]" + (at level 2, left associativity, format "p `.[ x ]"). -(* possible example usage *) -Definition exp_coeff' := [sequence 1 / n`!%:R]_n. -Definition expR := [power_series exp_coeff']. +Section formal_power_series. +Variable R : realType. -Lemma power_series_has_a_radius_of_convergence : - forall ps : power_series_T, exists rad : R, - (forall x, x < rad -> cvg ps.[x]) /\ - (forall x, x > rad -> ~ cvg ps.[x]). +(*TODO: Definition formal_power_series := R^nat.*) -Definition radius_of_convergence (ps : power_series_T) : R := - get (power_series_has_a_radius_of_convergence ps). (* = rad *) +Definition fps_add (f g : R^nat) := (f \+ g). -Lemma ratio_test : ... +Definition cauchy_product (a b : R^nat) : R^nat := + [sequence \sum_(0 <= k < n) (a k * b (n - k)%N)]_n. + +End formal_power_series. +(* TODO: this forms a ringType *) + +Section power_series_definition. +Variable R : realType. +Implicit Types f g : R^nat. + +Definition power_series f (x : R) : R^nat := + series (fun i => (f i *: 'X^i).[x]). + +Local Notation "f `.[ x ]" := (power_series f x). + +End power_series_definition. +Notation "p `.[ x ]" := (power_series p x) : ring_scope. + +Section examples. +Variable R : realType. + +Local Definition exp_coeff : R^nat := [sequence 1 / n`!%:R]_n. +Local Definition expR x : R := lim exp_coeff`.[x]. + +Local Definition sin_coeff : R^nat := + [sequence (odd n)%:R * (- 1) ^+ n.-1./2 * n`!%:R^-1]_n. +Local Definition sin x : R := lim sin_coeff`.[x]. + +End examples. + +Section radius. +Variable R : realType. +Implicit Types f g : R^nat. + +Definition power_series_radius (f : R^nat) : set R := fun r => + forall x, (`|x| < r -> cvg [normed f`.[x] ]) /\ + (`|x| > r -> ~ cvg f`.[x]). + +Lemma power_series_radius_exists f : exists r, power_series_radius f r. +Proof. +Admitted. + +Definition radius_of_convergence f : R := get (power_series_radius f). + +Lemma radius_normed_convergenceP f x : + `|x| < radius_of_convergence f -> cvg [normed f`.[x] ]. +Proof. +Abort. + +Lemma power_series_mul_cvg f g x : cvg f`.[x] -> cvg g`.[x] -> + cvg (cauchy_product f g)`.[x] /\ + lim (cauchy_product f g)`.[x] = lim f`.[x] * lim g`.[x]. +Proof. +Abort. + +(* TODO: Lemma ratio_test : ... *) + +End radius.