feat(Analysis\SpecialFunctions\OrdinaryHypergeometric) and feat(RingTheory\Polynomial\Pochhammer): add the ordinaryHyperGeometricSeries and related theorems #17448
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 39ce6ace36
|
| 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.
|
I intend to PR the commented result in ascPochhammer after this one is merged but wanted to limit the scope of this PR. |
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