Commit 2024-07-29 03:09 2159435a

feat: Define AnalyticWithinAt and AnalyticWithinOn (#13971) Unlike ContinuousOn, which allows arbitrary behavior outside of the set, AnalyticOn requires the function to be analytic in a neighborhood of the set. This is inconvenient for analytic manifolds with boundary, as we want analyticity for functions meaningful only up to the boundary. Here we add AnalyticWithinAt and AnalyticWithinOn with the natural definitions. The one subtlety is that we explicitly require ContinuousWithinAt in AnalyticWithinAt, as otherwise the natural definition does not imply a nice value of the function at the point.