Commit 2025-07-26 14:25 0eeb5f25

View on Github →

feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap (#26255)

Add basic lemmas compContinuousLinearMap_id and compContinuousLinearMap_comp.
Prove lower and upper bounds for the convergence radius of f.compContinuousLinearMap.
Prove radius_compNeg: the convergence radii of f(x) and f(-x) are equal.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem FormalMultilinearSeries.div_le_radius_compContinuousLinearMap

added theorem FormalMultilinearSeries.enorm_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.le_radius_compContinuousLinearMap

added theorem FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.norm_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.radius_compContinuousLinearMap_eq

added theorem FormalMultilinearSeries.radius_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq

added theorem FormalMultilinearSeries.radius_compNeg

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added theorem FormalMultilinearSeries.compContinuousLinearMap_comp

added theorem FormalMultilinearSeries.compContinuousLinearMap_id

added theorem compContinuousLinearMap_zero

deleted theorem constFormalMultilinearSeries_apply

added theorem constFormalMultilinearSeries_apply_of_nonzero

added theorem constFormalMultilinearSeries_apply_succ

added theorem constFormalMultilinearSeries_apply_zero

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

added theorem LinearIsometry.enorm_toContinuousLinearMap

added theorem LinearIsometry.nnnorm_toContinuousLinearMap