Commit 2024-03-01 13:29 9a322358

View on Github →

feat: Abel's limit theorem (#10000) From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Bounds.20on.20alternating.20convergent.20series/near/418770183

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

added theorem Finset.sum_Ico_Ico_comm'

Created Mathlib/Analysis/Complex/AbelLimit.lean

added theorem Complex.abel_aux

added theorem Complex.nhdsWithin_lt_le_nhdsWithin_stolzSet

added theorem Complex.nhdsWithin_stolzCone_le_nhdsWithin_stolzSet

added def Complex.stolzCone

added theorem Complex.stolzCone_subset_StolzSet_aux

added def Complex.stolzSet

added theorem Complex.stolzSet_empty

added theorem Complex.tendsto_tsum_powerSeries_nhdsWithin_lt

added theorem Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone

added theorem Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSet

added theorem Real.tendsto_tsum_powerSeries_nhdsWithin_lt

Modified Mathlib/Data/Complex/Abs.lean

added theorem Complex.abs_eq_sqrt_sq_add_sq

Modified Mathlib/Data/Real/Sqrt.lean

added theorem Real.sqrt_one_add_le