Commit 2023-10-29 11:56 b56efa53

View on Github →

feat(Analysis/Analytic): A few more analyticity lemmas (#7967)

  1. Analytic at a point means analytic in a ball
  2. In addition to AnalyticAt.{smul,mul,pow}, do AnalyticOn.{smul,mul,pow} Also change AnalyticAt.smul and AnalyticAt.pow to use pointwise smul and pow rather than function smul and pow, as I think this is more ergonomic when used in practice (from experience with https://github.com/girving/ray).

Estimated changes

modified theorem AnalyticAt.mul
modified theorem AnalyticAt.pow
modified theorem AnalyticAt.smul
added theorem AnalyticOn.mul
added theorem AnalyticOn.pow
added theorem AnalyticOn.smul