Commit 2025-08-16 00:05 65eb374c

View on Github →

chore(Analysis/Analytic): split Analytic.Basic (#26270) Move the results on the radius of convergence from Analytic/Basic.lean to a new file Analytic/ConvergenceRadius.lean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Analytic/Basic.lean

deleted theorem FormalMultilinearSeries.constFormalMultilinearSeries_radius

deleted theorem FormalMultilinearSeries.div_le_radius_compContinuousLinearMap

deleted theorem FormalMultilinearSeries.enorm_compContinuousLinearMap_le

deleted theorem FormalMultilinearSeries.isLittleO_of_lt_radius

deleted theorem FormalMultilinearSeries.isLittleO_one_of_lt_radius

deleted theorem FormalMultilinearSeries.le_mul_pow_of_radius_pos

deleted theorem FormalMultilinearSeries.le_radius_compContinuousLinearMap

deleted theorem FormalMultilinearSeries.le_radius_of_bound

deleted theorem FormalMultilinearSeries.le_radius_of_bound_nnreal

deleted theorem FormalMultilinearSeries.le_radius_of_eventually_le

deleted theorem FormalMultilinearSeries.le_radius_of_isBigO

deleted theorem FormalMultilinearSeries.le_radius_of_summable

deleted theorem FormalMultilinearSeries.le_radius_of_summable_nnnorm

deleted theorem FormalMultilinearSeries.le_radius_of_summable_norm

deleted theorem FormalMultilinearSeries.le_radius_of_tendsto

deleted theorem FormalMultilinearSeries.lt_radius_of_isBigO

deleted theorem FormalMultilinearSeries.min_radius_le_radius_add

deleted theorem FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le

deleted theorem FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius

deleted theorem FormalMultilinearSeries.norm_compContinuousLinearMap_le

deleted theorem FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius

deleted theorem FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius

deleted theorem FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius

deleted theorem FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm

deleted def FormalMultilinearSeries.partialSum

deleted theorem FormalMultilinearSeries.partialSum_continuous

deleted def FormalMultilinearSeries.radius

deleted theorem FormalMultilinearSeries.radius_compContinuousLinearMap_eq

deleted theorem FormalMultilinearSeries.radius_compContinuousLinearMap_le

deleted theorem FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq

deleted theorem FormalMultilinearSeries.radius_compNeg

deleted theorem FormalMultilinearSeries.radius_eq_top_iff_summable_norm

deleted theorem FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero

deleted theorem FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero

deleted theorem FormalMultilinearSeries.radius_eq_top_of_forall_nnreal_isBigO

deleted theorem FormalMultilinearSeries.radius_eq_top_of_summable_norm

deleted theorem FormalMultilinearSeries.radius_le_of_le

deleted theorem FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp

deleted theorem FormalMultilinearSeries.radius_le_smul

deleted theorem FormalMultilinearSeries.radius_neg

deleted theorem FormalMultilinearSeries.radius_shift

deleted theorem FormalMultilinearSeries.radius_smul_eq

deleted theorem FormalMultilinearSeries.radius_unshift

deleted theorem FormalMultilinearSeries.summable_nnnorm_mul_pow

deleted theorem FormalMultilinearSeries.summable_norm_apply

deleted theorem FormalMultilinearSeries.summable_norm_mul_pow

deleted theorem FormalMultilinearSeries.zero_radius

Created Mathlib/Analysis/Analytic/ConvergenceRadius.lean

added theorem FormalMultilinearSeries.constFormalMultilinearSeries_radius

added theorem FormalMultilinearSeries.div_le_radius_compContinuousLinearMap

added theorem FormalMultilinearSeries.enorm_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.isLittleO_of_lt_radius

added theorem FormalMultilinearSeries.isLittleO_one_of_lt_radius

added theorem FormalMultilinearSeries.le_mul_pow_of_radius_pos

added theorem FormalMultilinearSeries.le_radius_compContinuousLinearMap

added theorem FormalMultilinearSeries.le_radius_of_bound

added theorem FormalMultilinearSeries.le_radius_of_bound_nnreal

added theorem FormalMultilinearSeries.le_radius_of_eventually_le

added theorem FormalMultilinearSeries.le_radius_of_isBigO

added theorem FormalMultilinearSeries.le_radius_of_summable

added theorem FormalMultilinearSeries.le_radius_of_summable_nnnorm

added theorem FormalMultilinearSeries.le_radius_of_summable_norm

added theorem FormalMultilinearSeries.le_radius_of_tendsto

added theorem FormalMultilinearSeries.lt_radius_of_isBigO

added theorem FormalMultilinearSeries.min_radius_le_radius_add

added theorem FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius

added theorem FormalMultilinearSeries.norm_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius

added theorem FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius

added theorem FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius

added theorem FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm

added def FormalMultilinearSeries.partialSum

added theorem FormalMultilinearSeries.partialSum_continuous

added def FormalMultilinearSeries.radius

added theorem FormalMultilinearSeries.radius_compContinuousLinearMap_eq

added theorem FormalMultilinearSeries.radius_compContinuousLinearMap_le

added theorem FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq

added theorem FormalMultilinearSeries.radius_compNeg

added theorem FormalMultilinearSeries.radius_eq_top_iff_summable_norm

added theorem FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero

added theorem FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero

added theorem FormalMultilinearSeries.radius_eq_top_of_forall_nnreal_isBigO

added theorem FormalMultilinearSeries.radius_eq_top_of_summable_norm

added theorem FormalMultilinearSeries.radius_le_of_le

added theorem FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp

added theorem FormalMultilinearSeries.radius_le_smul

added theorem FormalMultilinearSeries.radius_neg

added theorem FormalMultilinearSeries.radius_shift

added theorem FormalMultilinearSeries.radius_smul_eq

added theorem FormalMultilinearSeries.radius_unshift

added theorem FormalMultilinearSeries.summable_nnnorm_mul_pow

added theorem FormalMultilinearSeries.summable_norm_apply

added theorem FormalMultilinearSeries.summable_norm_mul_pow

added theorem FormalMultilinearSeries.zero_radius

Modified Mathlib/Analysis/Analytic/OfScalars.lean

Modified Mathlib/Analysis/Analytic/RadiusLiminf.lean