Commit 2025-01-21 21:33 e3ce54ee

View on Github →

feat(Analysis): relate summable and multipliable sequences using log (#16546) Add some results about transforming summable sequences f n indexed by natural numbers , into multipliable sequeces of the form 1 + f n using complex and real logs.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/FunctionSeries.lean

added theorem tendstoUniformlyOn_tsum_nat_eventually

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

deleted theorem Complex.HasSum_cexp_HasProd

modified theorem Complex.cexp_tsum_eq_tprod

added theorem Complex.hasProd_of_hasSum_log

added theorem Complex.multipliable_of_summable_log

deleted theorem Complex.summable_cexp_multipliable

deleted theorem Real.HasSum_rexp_HasProd

added theorem Real.hasProd_of_hasSum_log

added theorem Real.multipliable_of_summable_log

modified theorem Real.rexp_tsum_eq_tprod

deleted theorem Real.summable_cexp_multipliable

Created Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

added theorem Complex.multipliable_one_add_of_summable

added theorem Complex.summable_log_one_add_of_summable

added theorem Complex.tendstoUniformlyOn_tsum_nat_log_one_add

added theorem Real.multipliable_one_add_of_summable

added theorem Real.summable_log_one_add_of_summable