[Merged by Bors] - feat: define the ordinary hypergeometric function #17455

EdwardWatine · 2024-10-05T20:19:10Z

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 is found in the Pochhammer file. Closely follows the exponential series definition.

#15966

…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 · 2024-10-05T20:19:56Z

PR summary 5a29ad33d6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Polynomial.Pochhammer	955	960	+5 (+0.52%)

Import changes for all files

Files	Import difference
7 files `Mathlib.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.Analytic.OfScalars`	1388
`Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric`	1404

Declarations diff

+ RCLike.tendsto_add_mul_div_add_mul_atTop_nhds
+ ascPochhammer_eval_eq_zero_iff
+ ascPochhammer_eval_neg_coe_nat_of_lt
+ ofScalars
+ ofScalarsSum
+ ofScalarsSum_eq_tsum
+ ofScalars_apply_eq
+ ofScalars_apply_eq'
+ ofScalars_eq_zero
+ ofScalars_norm
+ ofScalars_norm_eq_mul
+ ofScalars_norm_le
+ ofScalars_op
+ ofScalars_radius_eq_inv_of_tendsto
+ ofScalars_radius_eq_of_tendsto
+ ofScalars_sum_eq
+ ofScalars_unop
+ ordinaryHypergeometric
+ ordinaryHypergeometricCoefficient
+ ordinaryHypergeometricSeries
+ ordinaryHypergeometricSeries_apply_eq
+ ordinaryHypergeometricSeries_apply_eq'
+ ordinaryHypergeometricSeries_apply_zero
+ ordinaryHypergeometricSeries_eq_zero_iff
+ ordinaryHypergeometricSeries_eq_zero_of_neg_nat
+ ordinaryHypergeometricSeries_norm_div_succ_norm
+ ordinaryHypergeometricSeries_radius_eq_one
+ ordinaryHypergeometricSeries_symm
+ ordinaryHypergeometric_eq_tsum
+ ordinaryHypergeometric_radius_top_of_neg_nat₁
+ ordinaryHypergeometric_radius_top_of_neg_nat₂
+ ordinaryHypergeometric_radius_top_of_neg_nat₃
+ ordinaryHypergeometric_sum_eq
+ 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 · 2024-10-05T20:20:44Z

I intend to PR the commented inline theorem in Pochhammer after the subsequent build after this is merged, in order to limit the scope of this PR

Mathlib/RingTheory/Polynomial/Pochhammer.lean

…itive integers. Also perform some general performance and style refactors.

ocfnash · 2024-10-13T15:50:41Z

@EdwardWatine Note that this is currently failing CI! I will wait to review again until it is ready.

ocfnash · 2024-10-13T16:07:58Z

One other high level comment as I look at the material in this PR and the similar API for the exponential series is that we should probably introduce a definition:

def FormalMultilinearSeries.ofScalars (c : ℕ → 𝕂) : FormalMultilinearSeries 𝕂 𝔸 𝔸 :=
  fun n ↦ c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸

and develop some API for that. I think it would simplify the work here.

EdwardWatine · 2024-10-13T16:20:11Z

Whoops, I keep forgetting to restart the file after changing the other one...
I agree with adding some more support for scalar Multilinear series, perhaps this could be extended to multiple types of maps and not just MkPiAlgebraFin?

ocfnash

Looking great, a few more nitpicks below:

Mathlib/RingTheory/Polynomial/Pochhammer.lean

Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean

ocfnash · 2024-10-13T20:17:39Z

I agree with adding some more support for scalar Multilinear series, perhaps this could be extended to multiple types of maps and not just MkPiAlgebraFin?

I think MkPiAlgebraFin is special enough to deserve it's own dedicated API. If you have the appetite to write this as part of this PR and use it to implement the work here then that would be great. If not, I'm also OK with leaving things are they are for now and I'll do one final round of review after you've had a chance to react to my latest round of nitpicks.

EdwardWatine · 2024-10-14T12:28:51Z

I was having a look for adding API as you suggest, but I'm not entirely sure where it would lie. Ideally it would go in Mathlib\Analysis\Calculus\FormalMultilinearSeries.lean, but we really want to be able to use other results that come from other files such as Mathlib\Analysis\Analytic\Basic.lean and Mathlib\Analysis\NormedSpace\Multilinear\Basic.lean (I think). Perhaps this needs a new file?

ocfnash · 2024-10-14T13:17:15Z

I was having a look for adding API as you suggest, but I'm not entirely sure where it would lie. [...] Perhaps this needs a new file?

Yes I think a new file would be the right move. Maybe Mathlib.Analysis.Analytic.ScalarSeries or Mathlib.Analysis.Analytic.OfScalars or ...

ocfnash

Thanks for all of this!

Please apply the remaining suggestions and then feel free to merge 🎉

bors d+

Mathlib/Analysis/SpecificLimits/RCLike.lean

Mathlib/RingTheory/Polynomial/Pochhammer.lean

Mathlib/Analysis/Analytic/OfScalars.lean

Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean

mathlib-bors · 2024-10-16T20:46:41Z

✌️ EdwardWatine can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

jcommelin

Thanks 🎉

bors merge

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 is found in the Pochhammer file. Closely follows the exponential series definition. #15966 Co-authored-by: Alvan Caleb Arulandu <[email protected]>

mathlib-bors · 2024-10-17T08:51:17Z

Pull request successfully merged into master.

Build succeeded:

EdwardWatine and others added 16 commits September 10, 2024 21:03

finish a relatively long theorem about ascPochhammer, necessary to av…

e4b6039

…oid poles in the sum later. TODO: find the minimal classes on ascPochhammer to move to an appropriate location.

show the ratio of two series terms

f66a583

simplify hypergeo succ_norm_div_norm pf

6af7d4e

add radius theorems for terminating cases, as well as a few more helpers

20f2efa

Merge branch 'edwatine/hypergeometric-function' of https://github.com…

c446487

…/leanprover-community/mathlib4 into edwatine/hypergeometric-function

clicked some things I shouldn't have with git, whoopsie

c254c99

Reverted changes that I deleted

6a2e3aa

some radius eq 1 progress

062fe72

Merge branch 'master' of https://github.com/leanprover-community/math…

46d04b7

…lib4 into edwatine/hypergeometric-function

Merge branch 'edwatine/hypergeometric-function' of https://github.com…

1478c65

…/leanprover-community/mathlib4 into edwatine/hypergeometric-function

fix merge

a14fe3b

Linting

fd939a1

delete stray exp

e7fd3aa

lake exe mk_all

39ce6ac

linting

a788736

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Oct 5, 2024

EdwardWatine added awaiting-CI t-analysis Analysis (normed *, calculus) labels Oct 5, 2024

github-actions bot removed the awaiting-CI label Oct 5, 2024

ocfnash self-requested a review October 6, 2024 15:10

typos

f38dec8

jcommelin reviewed Oct 7, 2024

View reviewed changes

Mathlib/RingTheory/Polynomial/Pochhammer.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Polynomial/Pochhammer.lean Outdated Show resolved Hide resolved

EdwardWatine added 3 commits October 9, 2024 13:30

Refactor everywhere to work with negative naturals instead of non-pos…

3e9f769

…itive integers. Also perform some general performance and style refactors.

Update some function names, refactor a couple proofs

aa524f6

fix renamed functions

85ce4ab

ocfnash changed the title ~~feat(Analysis/SpecialFunctions/OrdinaryHypergeometric) and (RingTheory/Polynomial/Pochhammer): add the ordinaryHyperGeometricSeries and related theorems~~ feat: define the ordinary hypergeometric function Oct 13, 2024

Implement changes suggested by @ocfnash

4484d1f

EdwardWatine removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 13, 2024

ocfnash added the awaiting-CI label Oct 13, 2024

Make R parameter implicit in Pochhammer

a7c9ae5

github-actions bot removed the awaiting-CI label Oct 13, 2024

ocfnash reviewed Oct 13, 2024

View reviewed changes

ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 13, 2024

EdwardWatine added 2 commits October 15, 2024 14:43

Implement second round of changes proposed by @ocfnash

82bdfc4

add an API ofScalars

7a17f4a

EdwardWatine removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 15, 2024

lake exe mk_all

84f84cd

ocfnash approved these changes Oct 16, 2024

View reviewed changes

leanprover-community-mathlib4-bot added the delegated label Oct 16, 2024

EdwardWatine added 2 commits October 16, 2024 23:22

Implement final set of changes suggested by @ocfnash

6b91913

making the linter happy makes me sad here :(

5a29ad3

jcommelin reviewed Oct 17, 2024

View reviewed changes

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Oct 17, 2024

mathlib-bors bot changed the title ~~feat: define the ordinary hypergeometric function~~ [Merged by Bors] - feat: define the ordinary hypergeometric function Oct 17, 2024

mathlib-bors bot closed this Oct 17, 2024

mathlib-bors bot deleted the edwatine/hypergeometric-function branch October 17, 2024 08:51

EdwardWatine mentioned this pull request Oct 29, 2024

feat: improve the Analysis.Analytic.OfScalars API and implement it for geometric and exponential functions #18407

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: define the ordinary hypergeometric function #17455

[Merged by Bors] - feat: define the ordinary hypergeometric function #17455

EdwardWatine commented Oct 5, 2024

github-actions bot commented Oct 5, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

EdwardWatine commented Oct 5, 2024

ocfnash commented Oct 13, 2024 •

edited

Loading

ocfnash commented Oct 13, 2024

EdwardWatine commented Oct 13, 2024 •

edited

Loading

ocfnash left a comment

ocfnash commented Oct 13, 2024 •

edited

Loading

EdwardWatine commented Oct 14, 2024

ocfnash commented Oct 14, 2024

ocfnash left a comment

mathlib-bors bot commented Oct 16, 2024

jcommelin left a comment

mathlib-bors bot commented Oct 17, 2024

[Merged by Bors] - feat: define the ordinary hypergeometric function #17455

[Merged by Bors] - feat: define the ordinary hypergeometric function #17455

Conversation

EdwardWatine commented Oct 5, 2024

github-actions bot commented Oct 5, 2024 • edited Loading

PR summary 5a29ad33d6

Import changes for modified files

Declarations diff

EdwardWatine commented Oct 5, 2024

ocfnash commented Oct 13, 2024 • edited Loading

ocfnash commented Oct 13, 2024

EdwardWatine commented Oct 13, 2024 • edited Loading

ocfnash left a comment

Choose a reason for hiding this comment

ocfnash commented Oct 13, 2024 • edited Loading

EdwardWatine commented Oct 14, 2024

ocfnash commented Oct 14, 2024

ocfnash left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Oct 16, 2024

jcommelin left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Oct 17, 2024

github-actions bot commented Oct 5, 2024 •

edited

Loading

ocfnash commented Oct 13, 2024 •

edited

Loading

EdwardWatine commented Oct 13, 2024 •

edited

Loading

ocfnash commented Oct 13, 2024 •

edited

Loading