SumPrimeReciprocals

📁 Source: Mathlib/NumberTheory/SumPrimeReciprocals.lean

Statistics

Metric	Count
Definitions	0
Theorems not_summable_one_div, summable_rpow, roughNumbersUpTo_card_le', not_summable_one_div_on_primes, one_half_le_sum_primes_ge_one_div	5
Total	5

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
roughNumbersUpTo_card_le' 📖	mathematical	—	Real Real.instLE Real.instNatCast Finset.card roughNumbersUpTo Real.instMul Finset.sum Real.instAddCommMonoid Finset Finset.instSDiff primesBelow DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	Finset.mul_sum Finset.sum_congr mul_one_div LE.le.trans cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike roughNumbersUpTo_card_le Finset.sum_le_sum cast_div_le Real.instIsStrictOrderedRing cast_sum

Nat.Primes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_summable_one_div 📖	mathematical	—	Summable Real Nat.Primes Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast Nat.Prime SummationFilter.unconditional	—	Function.mt summable_subtype_iff_indicator not_summable_one_div_on_primes
summable_rpow 📖	mathematical	—	Summable Real Nat.Primes Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Real.instNatCast Nat.Prime SummationFilter.unconditional Real.instLT Real.instNeg Real.instOne	—	Summable.subtype instIsUniformAddGroupReal Real.instCompleteSpace Real.summable_nat_rpow not_summable_one_div Summable.of_nonneg_of_le Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass one_div Real.rpow_neg_one Real.rpow_le_rpow_of_exponent_le RCLike.charZero_rclike LT.lt.le Nat.Prime.one_lt Subtype.prop not_lt

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_summable_one_div_on_primes 📖	mathematical	—	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.indicator Real.instZero setOf Nat.Prime DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Summable.nat_tsum_vanishing instIsTopologicalAddGroupReal Iio_mem_nhds instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.indicator_indicator Set.inter_comm Summable.indicator instIsUniformAddGroupReal Real.instCompleteSpace LT.lt.false LE.le.trans_lt one_half_le_sum_primes_ge_one_div Finset.sum_congr Finset.mem_sdiff Set.mem_setOf_eq Nat.prime_of_mem_primesBelow Set.indicator_of_mem Summable.sum_le_tsum SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional Set.indicator_nonneg Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass Set.mem_Iio Set.inter_eq_left tsum_subtype Set.inter_subset_right
one_half_le_sum_primes_ge_one_div 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Finset.sum Real.instAddCommMonoid Finset Finset.instSDiff Nat.primesBelow Monoid.toNatPow Nat.instMonoid Finset.card	—	Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike Nat.smoothNumbersUpTo_card_add_roughNumbersUpTo_card IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Nat.smoothNumbersUpTo_card_le le_imp_le_of_le_of_le add_le_add_right Nat.roughNumbersUpTo_card_le' le_refl Finset.sum_congr Nat.cast_one mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' NeZero.charZero_one Nat.instIsStrictOrderedRing IsStrictOrderedRing.toIsOrderedRing Nat.instNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Nat.cast_two Nat.cast_pow Nat.cast_mul sub_le_iff_le_add' Nat.sqrt_eq' mul_pow pow_two mul_assoc pow_right_comm Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0

---

← Back to Index