feat(Analysis\SpecialFunctions\OrdinaryHypergeometric) and (RingTheory\Polynomial\Pochhammer): add the ordinaryHyperGeometricSeries and related theorems #17430
Conversation
…oid poles in the sum later. TODO: find the minimal classes on ascPochhammer to move to an appropriate location.
…/leanprover-community/mathlib4 into edwatine/hypergeometric-function
…y\Polynomial\Pochhammer): add the ordinaryHyperGeometricSeries and some related theorems Add the definition of the ordinary hypergeometric series, and show that its radius is one. Part of this requires an additional theorem about ascPochhammer, which can be found in the ascPochhammer file. Closely follows the exponential series definition. #15966
…lib4 into edwatine/hypergeometric-function
…/leanprover-community/mathlib4 into edwatine/hypergeometric-function
github-actions
bot
added
the
new-contributor
PR summary e7fd3aa420
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.Polynomial.Pochhammer | 946 | 951 | +5 (+0.53%) |
Import changes for all files
| Files | Import difference |
|---|---|
7 filesMathlib.Data.Nat.Choose.Cast Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Taylor Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Binomial Mathlib.Data.Nat.Factorial.Cast |
5 |
Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric |
1386 |
Declarations diff
+ ascPochhammer_eq_zero_iff
+ ascPochhammer_eq_zero_of_nonpos_int
+ ordinaryHypergeometric
+ ordinaryHypergeometricSeries
+ ordinaryHypergeometricSeries_apply_eq
+ ordinaryHypergeometricSeries_apply_eq'
+ ordinaryHypergeometricSeries_apply_zero
+ ordinaryHypergeometricSeries_eq_zero_iff
+ ordinaryHypergeometricSeries_eq_zero_of_nonpos_int
+ ordinaryHypergeometricSeries_radius_eq_one
+ ordinaryHypergeometricSeries_ratio_tendsto_one_atTop
+ ordinaryHypergeometricSeries_succ_norm_div_norm
+ ordinaryHypergeometricSeries_symm
+ ordinaryHypergeometric_eq_tsum
+ ordinaryHypergeometric_op
+ ordinaryHypergeometric_radius_top_of_nonpos_int₁
+ ordinaryHypergeometric_radius_top_of_nonpos_int₂
+ ordinaryHypergeometric_radius_top_of_nonpos_int₃
+ ordinaryHypergeometric_ratio_tendsto_nhds_atTop
+ ordinaryHypergeometric_sum_eq
+ ordinaryHypergeometric_unop
+ ordinaryHypergeometric_zero
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
EdwardWatine
added
enhancement
Add the definition of the ordinary hypergeometric series, and show that its radius is one. Part of this requires an additional theorem about ascPochhammer, which can be found in the Pochhammer file. Closely follows the exponential series definition.
#15966