Commit 2023-10-29 11:56 b56efa53
View on Github →feat(Analysis/Analytic): A few more analyticity lemmas (#7967)
- Analytic at a point means analytic in a ball
- In addition to
AnalyticAt.{smul,mul,pow}
, doAnalyticOn.{smul,mul,pow}
Also changeAnalyticAt.smul
andAnalyticAt.pow
to use pointwisesmul
andpow
rather than functionsmul
andpow
, as I think this is more ergonomic when used in practice (from experience with https://github.com/girving/ray).