Commit 2024-09-16 17:23 47053c51

View on Github →

feat: a continuous linear map into continuous multilinear maps is analytic (#16844) Also move the fact that continuous linear maps are analytic to the proper place, i.e., in Analytic.CPolynomial instead of Calculus.FDeriv.Analytic.

Estimated changes

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

added theorem ContinuousLinearMap.analyticAt_uncurry_of_multilinear

added theorem ContinuousLinearMap.analyticOn_uncurry_of_multilinear

added theorem ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear

added theorem ContinuousLinearMap.analyticWithinOn_uncurry_of_multilinear

added theorem ContinuousLinearMap.continuousAt_uncurry_of_multilinear

added theorem ContinuousLinearMap.continuousOn_uncurry_of_multilinear

added theorem ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear

added theorem ContinuousLinearMap.continuous_uncurry_of_multilinear

added theorem ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear

added theorem ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear

added theorem ContinuousMultilinearMap.analyticAt

added theorem ContinuousMultilinearMap.analyticOn

added theorem ContinuousMultilinearMap.analyticWithinAt

added theorem ContinuousMultilinearMap.analyticWithinOn

added theorem ContinuousMultilinearMap.cpolynomialAt

added theorem ContinuousMultilinearMap.cpolyomialOn

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

added theorem ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self