Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-10 17:14 41014e50

View on Github →

rename has_sum and is_sum to summable and has_sum (#912)

Estimated changes

Modified src/analysis/normed_space/basic.lean

deleted theorem has_sum_iff_vanishing_norm

deleted theorem has_sum_of_has_sum_norm

deleted theorem has_sum_of_norm_bounded

modified theorem norm_tsum_le_tsum_norm

added theorem summable_iff_vanishing_norm

added theorem summable_of_norm_bounded

added theorem summable_of_summable_norm

Modified src/analysis/specific_limits.lean

added theorem has_sum_geometric

added theorem has_sum_geometric_two

deleted theorem has_sum_of_absolute_convergence_real

deleted theorem is_sum_geometric

deleted theorem is_sum_geometric_two

added theorem summable_of_absolute_convergence_real

Modified src/measure_theory/probability_mass_function.lean

deleted theorem pmf.has_sum_coe

added theorem pmf.has_sum_coe_one

deleted theorem pmf.is_sum_coe_one

modified def pmf.pure

added theorem pmf.summable_coe

modified theorem pmf.tsum_coe

modified def {u}

Modified src/topology/algebra/infinite_sum.lean

deleted theorem cauchy_seq_of_has_sum_dist

added theorem cauchy_seq_of_summable_dist

modified def has_sum

modified theorem has_sum_add

deleted theorem has_sum_comp_of_has_sum_of_injective

added theorem has_sum_hom

deleted theorem has_sum_iff_cauchy

added theorem has_sum_iff_has_sum

deleted theorem has_sum_iff_has_sum_ne_zero

deleted theorem has_sum_iff_has_sum_ne_zero_bij

added theorem has_sum_iff_has_sum_of_iso

added theorem has_sum_iff_has_sum_of_ne_zero

added theorem has_sum_iff_has_sum_of_ne_zero_bij

added theorem has_sum_iff_of_summable

deleted theorem has_sum_iff_vanishing

added theorem has_sum_ite_eq

added theorem has_sum_le

added theorem has_sum_le_inj

modified theorem has_sum_mul_left

modified theorem has_sum_mul_right

modified theorem has_sum_neg

added theorem has_sum_of_has_sum

added theorem has_sum_of_has_sum_ne_zero

deleted theorem has_sum_of_has_sum_of_sub

added theorem has_sum_of_iso

modified theorem has_sum_sigma

deleted theorem has_sum_spec

modified theorem has_sum_sub

modified theorem has_sum_sum

modified theorem has_sum_sum_of_ne_finset_zero

added theorem has_sum_tsum

added theorem has_sum_unique

modified theorem has_sum_zero

deleted def is_sum

deleted theorem is_sum_add

deleted theorem is_sum_hom

deleted theorem is_sum_iff_is_sum

deleted theorem is_sum_iff_is_sum_of_iso

deleted theorem is_sum_iff_is_sum_of_ne_zero

deleted theorem is_sum_iff_is_sum_of_ne_zero_bij

deleted theorem is_sum_iff_of_has_sum

deleted theorem is_sum_ite_eq

deleted theorem is_sum_le

deleted theorem is_sum_le_inj

deleted theorem is_sum_mul_left

deleted theorem is_sum_mul_right

deleted theorem is_sum_neg

deleted theorem is_sum_of_is_sum

deleted theorem is_sum_of_is_sum_ne_zero

deleted theorem is_sum_of_iso

deleted theorem is_sum_sigma

deleted theorem is_sum_sub

deleted theorem is_sum_sum

deleted theorem is_sum_sum_of_ne_finset_zero

deleted theorem is_sum_tsum

deleted theorem is_sum_unique

deleted theorem is_sum_zero

added def summable

added theorem summable_add

added theorem summable_comp_of_summable_of_injective

added theorem summable_iff_cauchy

added theorem summable_iff_summable_ne_zero

added theorem summable_iff_summable_ne_zero_bij

added theorem summable_iff_vanishing

added theorem summable_mul_left

added theorem summable_mul_right

added theorem summable_neg

added theorem summable_of_summable_of_sub

added theorem summable_sigma

added theorem summable_spec

added theorem summable_sub

added theorem summable_sum

added theorem summable_sum_of_ne_finset_zero

added theorem summable_zero

added theorem tendsto_sum_nat_of_has_sum

deleted theorem tendsto_sum_nat_of_is_sum

modified def tsum

modified theorem tsum_add

added theorem tsum_eq_has_sum

deleted theorem tsum_eq_is_sum

added theorem tsum_eq_tsum_of_has_sum_iff_has_sum

deleted theorem tsum_eq_tsum_of_is_sum_iff_is_sum

modified theorem tsum_le_tsum

modified theorem tsum_mul_left

modified theorem tsum_mul_right

modified theorem tsum_neg

modified theorem tsum_sub

modified theorem tsum_sum

modified theorem tsum_zero

Modified src/topology/instances/ennreal.lean

added theorem ennreal.has_sum_iff_tendsto_nat

deleted theorem ennreal.is_sum_iff_tendsto_nat

added theorem has_sum_iff_tendsto_nat_of_nonneg

deleted theorem has_sum_of_nonneg_of_le

deleted theorem is_sum_iff_tendsto_nat_of_nonneg

added theorem nnreal.exists_le_has_sum_of_le

deleted theorem nnreal.exists_le_is_sum_of_le

added theorem nnreal.has_sum_iff_tendsto_nat

deleted theorem nnreal.has_sum_of_le

deleted theorem nnreal.is_sum_iff_tendsto_nat

added theorem nnreal.summable_of_le

added theorem summable_of_nonneg_of_le

Modified src/topology/instances/nnreal.lean

modified theorem nnreal.has_sum_coe

deleted theorem nnreal.is_sum_coe

added theorem nnreal.summable_coe

modified theorem nnreal.tsum_coe