SumCoeff

📁 Source: Mathlib/NumberTheory/LSeries/SumCoeff.lean

Statistics

Metric	Count
Definitions	0
Theorems LSeriesSummable_of_sum_norm_bigO, LSeriesSummable_of_sum_norm_bigO_and_nonneg, LSeries_eq_mul_integral, LSeries_eq_mul_integral', LSeries_eq_mul_integral_of_nonneg, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg	7
Total	7

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LSeriesSummable_of_sum_norm_bigO 📖	mathematical	Asymptotics.IsBigO Real Real.norm Filter.atTop Nat.instPreorder Finset.sum Real.instAddCommMonoid Finset.Icc Nat.instLocallyFiniteOrder Norm.norm Complex Complex.instNorm Real.instPow Real.instNatCast Real.instLE Real.instZero Real.instLT Complex.re	LSeriesSummable	—	Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.univ_mem' LSeriesSummable.congr' Asymptotics.IsBigO.congr' Filter.Eventually.of_forall Finset.sum_congr LT.lt.ne' LT.lt.trans_le zero_lt_one Nat.instZeroLEOneClass Finset.mem_Icc Filter.EventuallyEq.rfl
LSeriesSummable_of_sum_norm_bigO_and_nonneg 📖	mathematical	Asymptotics.IsBigO Real Real.norm Filter.atTop Nat.instPreorder Finset.sum Real.instAddCommMonoid Finset.Icc Nat.instLocallyFiniteOrder Real.instPow Real.instNatCast Real.instLE Real.instZero Real.instLT Complex.re	LSeriesSummable Complex.ofReal	—	LSeriesSummable_of_sum_norm_bigO Finset.sum_congr Complex.norm_real abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
LSeries_eq_mul_integral 📖	mathematical	Real Real.instLE Real.instZero Real.instLT Complex.re LSeriesSummable Asymptotics.IsBigO Complex Complex.instNorm Real.norm Filter.atTop Nat.instPreorder Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.Icc Nat.instLocallyFiniteOrder Real.instPow Real.instNatCast	LSeries Complex.instMul MeasureTheory.integral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi Real.instPreorder Real.instOne Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Complex.instPow Complex.ofReal Complex.instNeg Complex.instAdd Complex.instOne	—	Finset.sum_congr LT.lt.ne' LT.lt.trans_le zero_lt_one Nat.instZeroLEOneClass Finset.mem_Icc Real.instIsStrictOrderedRing LSeries_congr LSeriesSummable_congr' Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.univ_mem' neg_add_rev
LSeries_eq_mul_integral' 📖	mathematical	Real Real.instLE Real.instZero Real.instLT Complex.re Asymptotics.IsBigO Real.norm Filter.atTop Nat.instPreorder Finset.sum Real.instAddCommMonoid Finset.Icc Nat.instLocallyFiniteOrder Norm.norm Complex Complex.instNorm Real.instPow Real.instNatCast	LSeries Complex.instMul MeasureTheory.integral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi Real.instPreorder Real.instOne ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Complex.instPow Complex.ofReal Complex.instNeg Complex.instAdd Complex.instOne	—	LSeries_eq_mul_integral LSeriesSummable_of_sum_norm_bigO Asymptotics.IsBigO.trans Asymptotics.isBigO_of_le LE.le.trans norm_sum_le Real.le_norm_self
LSeries_eq_mul_integral_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero Real.instLT Complex.re Asymptotics.IsBigO Real.norm Filter.atTop Nat.instPreorder Finset.sum Real.instAddCommMonoid Finset.Icc Nat.instLocallyFiniteOrder Real.instPow Real.instNatCast	LSeries Complex.ofReal Complex Complex.instMul MeasureTheory.integral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi Real.instPreorder Real.instOne ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Complex.instPow Complex.instNeg Complex.instAdd Complex.instOne	—	LSeries_eq_mul_integral' Asymptotics.IsBigO.congr_left Finset.sum_congr Complex.norm_real abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div 📖	mathematical	Filter.Tendsto Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.Icc Nat.instPreorder Nat.instLocallyFiniteOrder Complex.instNatCast Filter.atTop nhds LSeriesSummable Complex.ofReal	Real Complex.instMul Complex.instSub Complex.instOne LSeries nhdsWithin Real.pseudoMetricSpace Real.instOne Set.Ioi Real.instPreorder	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero tendsto_nhdsWithin_of_tendsto_nhds ContinuousAt.tendsto ContinuousAt.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousAt.fun_mul IsTopologicalSemiring.toContinuousMul ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuousAt_id' continuousAt_const zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.IsBoundedUnder.mono_le Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid tendsto_zero_iff_norm_tendsto_zero tendsto_of_le_liminf_of_limsup_le instOrderTopologyReal Filter.le_liminf_of_le Filter.IsBoundedUnder.isCoboundedUnder_ge nhdsGT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' norm_nonneg le_of_forall_pos_le_add AddGroup.existsAddOfLE contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono zero_add Filter.limsup_le_limsup Filter.isCoboundedUnder_le_of_eventually_le Filter.Tendsto.limsup_eq Filter.isBoundedUnder_of_eventually_ge Mathlib.Tactic.Ring.cast_zero Nat.cast_zero IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.continuousAt Complex.continuous_ofReal Filter.Tendsto.congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_overlap_pf_zero Filter.Tendsto.add
LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Finset.sum Real.instAddCommMonoid Finset.Icc Nat.instPreorder Nat.instLocallyFiniteOrder Real.instNatCast Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instLE Real.instZero	Complex Complex.instMul Complex.instSub Complex.ofReal Complex.instOne LSeries nhdsWithin Real.instOne Set.Ioi Real.instPreorder SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div Filter.Tendsto.congr Complex.ofReal_div Complex.ofReal_sum Finset.sum_congr Filter.Tendsto.ofReal LSeriesSummable_of_sum_norm_bigO_and_nonneg Asymptotics.isBigO_atTop_natCast_rpow_of_tendsto_div_rpow Real.rpow_one map_natCast RingHom.instRingHomClass zero_le_one Real.instZeroLEOneClass

---

← Back to Index