Commit 2024-03-07 16:36 c5eaf25c

View on Github →

feat: sums over residue classes (#11189) This adds a file Analysis.SumOverResidueClass, whose main result is

/-- A decreasing sequence of real numbers is summable on a residue class
if and only if it is summable. -/
lemma summable_indicator_mod_iff {m : ℕ} [NeZero m] {f : ℕ → ℝ} (hf : Antitone f) (k : ZMod m) :
    Summable ({n : ℕ | (n : ZMod m) = k}.indicator f) ↔ Summable f

We then use this to show that the harmonic series still diverges when restricted to a residue class. This is needed for the proof that the abscissa of absolute convergence of a Dirichlet L-series is 1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/PSeries.lean

modified theorem NNReal.summable_one_div_rpow

modified theorem NNReal.summable_rpow

modified theorem NNReal.summable_rpow_inv

added theorem Real.not_summable_indicator_one_div_natCast

modified theorem Real.not_summable_nat_cast_inv

modified theorem Real.not_summable_one_div_nat_cast

modified theorem Real.summable_abs_int_rpow

modified theorem Real.summable_nat_pow_inv

modified theorem Real.summable_nat_rpow

modified theorem Real.summable_nat_rpow_inv

modified theorem Real.summable_one_div_int_pow

modified theorem Real.summable_one_div_nat_pow

modified theorem Real.summable_one_div_nat_rpow

modified theorem Real.tendsto_sum_range_one_div_nat_succ_atTop

Created Mathlib/Analysis/SumOverResidueClass.lean

added theorem Finset.sum_indicator_mod

added theorem not_summable_indicator_mod_of_antitone_of_neg

added theorem not_summable_of_antitone_of_neg

added theorem summable_indicator_mod_iff

added theorem summable_indicator_mod_iff_summable

added theorem summable_indicator_mod_iff_summable_indicator_mod

Modified Mathlib/Data/ZMod/Basic.lean

added theorem Nat.range_mul_add