Summable

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

Statistics

Metric	Count
Definitions r, r1	2
Theorems abs_le_left_of_norm, abs_le_right_of_norm, abs_norm_eq_max_natAbs, abs_norm_eq_max_natAbs_neg, auxbound1, auxbound2, div_max_sq_ge_one, isBigO_linear_add_const_vec, isLittleO_const_left_of_properSpace_of_discreteTopology, linear_inv_isBigO_left, linear_inv_isBigO_right, linear_inv_isBigO_right_add, linear_isTheta_left, linear_isTheta_right, linear_isTheta_right_add, linear_left_summable, linear_right_summable, norm_eq_max_natAbs, norm_symm, r1_aux_bound, r1_eq, r1_pos, r_lower_bound_on_verticalStrip, r_mul_max_le, r_pos, summable_inv_of_isBigO_rpow_inv, summable_linear_left_mul_linear_left, summable_linear_right_add_one_mul_linear_right, summable_linear_sub_mul_linear_add, summable_of_isBigO_rpow_norm, summable_one_div_norm_rpow, summand_bound, summand_bound_of_mem_verticalStrip, tendsto_zero_inv_linear, tendsto_zero_inv_linear_sub, vec_add_const_isTheta	36
Total	38

EisensteinSeries

Definitions

Name	Category	Theorems
r 📖	CompOp	7 math math: summand_bound_of_mem_verticalStrip, r_lower_bound_on_verticalStrip, r_pos, auxbound1, auxbound2, r_mul_max_le, summand_bound
r1 📖	CompOp	3 math math: r1_aux_bound, r1_pos, r1_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_le_left_of_norm 📖	mathematical	—	Real Real.instLE Real.instIntCast abs instLatticeInt Int.instAddGroup Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Matrix.vecCons Matrix.vecEmpty	—	norm_eq_max_natAbs Matrix.cons_val_fin_one Nat.cast_max Real.instIsStrictOrderedRing Int.abs_eq_natAbs le_refl
abs_le_right_of_norm 📖	mathematical	—	Real Real.instLE Real.instIntCast abs instLatticeInt Int.instAddGroup Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Matrix.vecCons Matrix.vecEmpty	—	norm_eq_max_natAbs Matrix.cons_val_fin_one Nat.cast_max Real.instIsStrictOrderedRing Int.abs_eq_natAbs le_refl
abs_norm_eq_max_natAbs 📖	mathematical	—	Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Matrix.vecCons Matrix.vecEmpty Real Real.instAdd Real.instNatCast Real.instOne	—	norm_eq_max_natAbs Matrix.cons_val_fin_one Nat.cast_one RCLike.charZero_rclike
abs_norm_eq_max_natAbs_neg 📖	mathematical	—	Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Matrix.vecCons Matrix.vecEmpty Real Real.instAdd Real.instNatCast Real.instOne	—	norm_eq_max_natAbs Matrix.cons_val_fin_one Nat.cast_one RCLike.charZero_rclike
auxbound1 📖	mathematical	Real Real.instLE Real.instOne Monoid.toNatPow Real.instMonoid	r Norm.norm Complex Complex.instNorm Complex.instAdd Complex.instMul Complex.ofReal UpperHalfPlane.coe	—	Real.le_sqrt' Complex.im_ofReal_mul mul_pow LE.le.trans le_mul_of_one_le_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_add_of_nonneg_left covariant_swap_add_of_covariant_add Complex.re_ofReal_mul MulZeroClass.zero_mul add_zero
auxbound2 📖	mathematical	Real Real.instLE Real.instOne Monoid.toNatPow Real.instMonoid	r Norm.norm Complex Complex.instNorm Complex.instAdd Complex.instMul Complex.ofReal UpperHalfPlane.coe	—	Real.sqrt_le_sqrt_iff add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul r1_aux_bound Complex.re_ofReal_mul Complex.im_ofReal_mul add_zero
div_max_sq_ge_one 📖	mathematical	—	Real Real.instLE Real.instOne Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing	—	Nat.cast_ne_zero RCLike.charZero_rclike norm_eq_max_natAbs norm_ne_zero_iff Nat.cast_natAbs Int.cast_abs Real.instIsStrictOrderedRing div_pow sq_abs div_self isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat max_choice
isBigO_linear_add_const_vec 📖	mathematical	—	Asymptotics.IsBigO Complex Real Complex.instNorm Real.norm Filter.cofinite Complex.instInv Complex.instAdd Complex.instMul Complex.instIntCast UpperHalfPlane.coe Real.instInv Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing	—	Asymptotics.IsBigO.trans Asymptotics.IsTheta.isBigO vec_add_const_isTheta
isLittleO_const_left_of_properSpace_of_discreteTopology 📖	mathematical	—	Asymptotics.IsLittleO Real NormedAddCommGroup.toNorm Real.norm Filter.cofinite Norm.norm	—	norm_norm tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Topology.IsClosedEmbedding.id
linear_inv_isBigO_left 📖	mathematical	—	Asymptotics.IsBigO Complex Real Complex.instNorm Real.norm Filter.cofinite Complex.instInv Complex.instAdd Complex.instMul Complex.instIntCast Real.instInv Real.instIntCast	—	Asymptotics.IsTheta.isBigO Asymptotics.IsTheta.inv linear_isTheta_left
linear_inv_isBigO_right 📖	mathematical	—	Asymptotics.IsBigO Complex Real Complex.instNorm Real.norm Filter.cofinite Complex.instInv Complex.instAdd Complex.instMul Complex.instIntCast Real.instInv Real.instIntCast	—	—
linear_inv_isBigO_right_add 📖	mathematical	—	Asymptotics.IsBigO Complex Real Complex.instNorm Real.norm Filter.cofinite Complex.instInv Complex.instAdd Complex.instMul Complex.instIntCast Real.instInv Real.instIntCast	—	Asymptotics.IsTheta.isBigO Asymptotics.IsTheta.inv linear_isTheta_right_add
linear_isTheta_left 📖	mathematical	—	Asymptotics.IsTheta Complex Real Complex.instNorm Real.norm Filter.cofinite Complex.instAdd Complex.instMul Complex.instIntCast Real.instIntCast	—	Asymptotics.IsTheta.add_isLittleO mul_comm Asymptotics.IsTheta.const_mul_left Int.cast_complex_isTheta_cast_real Complex.instCharZero tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding instDiscreteTopologyInt instProperSpaceReal Int.isClosedEmbedding_coe_real
linear_isTheta_right 📖	mathematical	—	Asymptotics.IsTheta Complex Real Complex.instNorm Real.norm Filter.cofinite Complex.instAdd Complex.instMul Complex.instIntCast Real.instIntCast	—	Int.cofinite_eq Int.cast_zero add_zero linear_isTheta_right_add
linear_isTheta_right_add 📖	mathematical	—	Asymptotics.IsTheta Complex Real Complex.instNorm Real.norm Filter.cofinite Complex.instAdd Complex.instMul Complex.instIntCast Real.instIntCast	—	Asymptotics.IsTheta.add_isLittleO Asymptotics.IsLittleO.add_isTheta NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding instDiscreteTopologyInt instProperSpaceReal Int.isClosedEmbedding_coe_real Int.cast_complex_isTheta_cast_real
linear_left_summable 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instInv DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instAdd Complex.instMul Complex.instIntCast SummationFilter.unconditional	—	summable_inv_of_isBigO_rpow_inv Complex.instCompleteSpace Nat.cast_one Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike CanLift.prf instCanLiftIntNatCastLeOfNat zpow_natCast Int.cast_natCast Real.rpow_natCast Real.instIsStrictOrderedRing Asymptotics.IsBigO.pow NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Asymptotics.IsBigO.abs_right linear_inv_isBigO_left
linear_right_summable 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instInv DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instAdd Complex.instMul Complex.instIntCast SummationFilter.unconditional	—	summable_inv_of_isBigO_rpow_inv Complex.instCompleteSpace Nat.cast_one Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike CanLift.prf instCanLiftIntNatCastLeOfNat
norm_eq_max_natAbs 📖	mathematical	—	Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Real Real.instNatCast	—	coe_nnnorm NNReal.coe_natCast Nat.cast_max NNReal.instIsStrictOrderedRing eq_of_forall_ge_iff NNReal.natCast_natAbs
norm_symm 📖	mathematical	—	Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Matrix.vecCons Matrix.vecEmpty	—	norm_eq_max_natAbs Matrix.cons_val_fin_one Nat.cast_max Real.instIsStrictOrderedRing Nat.cast_natAbs Int.cast_abs max_comm
r1_aux_bound 📖	mathematical	Real Real.instLE Real.instOne Monoid.toNatPow Real.instMonoid	r1 Real.instAdd Real.instMul UpperHalfPlane.re UpperHalfPlane.im	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr 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 Nat.cast_one r1.eq_1 div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass UpperHalfPlane.im_pos sub_nonneg add_nonneg sq_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing mul_nonneg
r1_eq 📖	mathematical	—	r1 Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instAdd Monoid.toNatPow Real.instMonoid UpperHalfPlane.re UpperHalfPlane.im	—	div_pow div_add_one ne_of_gt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass UpperHalfPlane.im_pos one_div_div r1.eq_1
r1_pos 📖	mathematical	—	Real Real.instLT Real.instZero r1	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toZeroLEOneClass UpperHalfPlane.im_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul
r_lower_bound_on_verticalStrip 📖	mathematical	Real Real.instLT Real.instZero UpperHalfPlane Set Set.instMembership UpperHalfPlane.verticalStrip	Real.instLE r	—	min_le_min Real.sqrt_monotone r1_eq div_pow one_div inv_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul pow_pos IsStrictOrderedRing.toZeroLEOneClass UpperHalfPlane.im_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one add_le_add_iff_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Even.pow_abs even_two div_le_div₀ pow_le_pow_left₀ IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono abs_nonneg le_of_lt
r_mul_max_le 📖	mathematical	—	Real Real.instLE Real.instMul r Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Complex Complex.instNorm Complex.instAdd Complex.instMul Complex.instIntCast UpperHalfPlane.coe	—	norm_ne_zero_iff div_mul_eq_mul_div add_div div_mul_cancel₀ Nat.cast_zero norm_eq_max_natAbs norm_mul NormedDivisionRing.toNormMulClass Complex.norm_real norm_norm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing div_max_sq_ge_one Complex.ofReal_div auxbound1 auxbound2 Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
r_pos 📖	mathematical	—	Real Real.instLT Real.instZero r	—	—
summable_inv_of_isBigO_rpow_inv 📖	mathematical	Real Real.instLT Real.instOne Asymptotics.IsBigO NormedField.toNorm Real.norm Filter.cofinite InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield NormedField.toField Real.instInv Real.instPow abs Real.lattice Real.instAddGroup Real.instIntCast	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SummationFilter.unconditional	—	summable_of_isBigO Summable.congr Real.summable_abs_int_rpow Real.rpow_neg abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
summable_linear_left_mul_linear_left 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instInv Complex.instMul Complex.instAdd Complex.instIntCast SummationFilter.unconditional	—	summable_inv_of_isBigO_rpow_inv Complex.instCompleteSpace Nat.instAtLeastTwoHAddOfNat Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Real.rpow_two pow_two abs_mul_abs_self Int.cofinite_eq mul_inv_rev Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass linear_inv_isBigO_left
summable_linear_right_add_one_mul_linear_right 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instInv Complex.instMul Complex.instAdd Complex.instIntCast Complex.instOne SummationFilter.unconditional	—	summable_inv_of_isBigO_rpow_inv Complex.instCompleteSpace Nat.instAtLeastTwoHAddOfNat Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Int.cofinite_eq mul_inv_rev Real.rpow_ofNat pow_two abs_mul_abs_self Int.cast_one Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass linear_inv_isBigO_right linear_inv_isBigO_right_add
summable_linear_sub_mul_linear_add 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instInv Complex.instMul Complex.instSub Complex.instIntCast Complex.instAdd SummationFilter.unconditional	—	summable_inv_of_isBigO_rpow_inv Complex.instCompleteSpace Nat.instAtLeastTwoHAddOfNat Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Int.cofinite_eq mul_inv_rev Real.rpow_ofNat pow_two abs_mul_abs_self Int.cast_neg inv_neg mul_neg Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass linear_inv_isBigO_right Asymptotics.IsBigO.comp_neg_int
summable_of_isBigO_rpow_norm 📖	mathematical	Real Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.cofinite Real.instInv Real.instPow Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat summable_of_isBigO Summable.congr summable_one_div_norm_rpow Real.rpow_neg norm_nonneg
summable_one_div_norm_rpow 📖	mathematical	Real Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Real.instNeg SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Equiv.summable_iff summable_partition Real.rpow_nonneg norm_nonneg Int.existsUnique_mem_box HasSum.summable hasSum_fintype SummationFilter.instLeAtTopUnconditional tsum_fintype Finset.sum_const Finset.card_attach nsmul_eq_mul Summable.of_norm_bounded_eventually_nat Real.instCompleteSpace Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.summable_nat_rpow lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.univ_mem' Int.card_box LT.lt.ne' Real.norm_of_nonneg le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike LinearOrderedCommMonoidWithZero.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Real.rpow_pos_of_pos sub_eq_add_neg Real.rpow_add Nat.cast_pos Real.instNontrivial Real.rpow_one Nat.cast_mul Nat.cast_ofNat mul_assoc le_refl Summable.congr tsum_congr Int.mem_box Nat.cast_max norm_eq_max_natAbs
summand_bound 📖	mathematical	Real Real.instLE Real.instZero	Real.instPow Norm.norm Complex Complex.instNorm Complex.instAdd Complex.instMul Complex.instIntCast UpperHalfPlane.coe Real.instNeg Real.instMul r NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing	—	Int.cast_zero MulZeroClass.zero_mul add_zero norm_zero Real.rpow_zero one_mul le_refl Real.zero_rpow MulZeroClass.mul_zero Real.mul_rpow LT.lt.le r_pos norm_nonneg Real.rpow_le_rpow_of_nonpos mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff r_mul_max_le neg_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
summand_bound_of_mem_verticalStrip 📖	mathematical	Real Real.instLE Real.instZero Real.instLT UpperHalfPlane Set Set.instMembership UpperHalfPlane.verticalStrip	Real.instPow Norm.norm Complex Complex.instNorm Complex.instAdd Complex.instMul Complex.instIntCast UpperHalfPlane.coe Real.instNeg Real.instMul r NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing	—	LE.le.trans summand_bound mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing Real.rpow_le_rpow_of_nonpos r_pos r_lower_bound_on_verticalStrip neg_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.rpow_nonneg norm_nonneg
tendsto_zero_inv_linear 📖	mathematical	—	Filter.Tendsto Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instAdd Complex.instMul Complex.instIntCast Complex.instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero	—	Asymptotics.IsBigO.trans_tendsto Asymptotics.isBigO_sup linear_inv_isBigO_right Int.cofinite_eq one_div tendsto_inv_atTop_nhds_zero_nat RCLike.charZero_rclike NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero NNRat.instContinuousSMulRatReal
tendsto_zero_inv_linear_sub 📖	mathematical	—	Filter.Tendsto Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instSub Complex.instMul Complex.instIntCast Complex.instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero	—	—
vec_add_const_isTheta 📖	mathematical	—	Asymptotics.IsTheta Real Real.norm Filter.cofinite Real.instInv Norm.norm NormedRing.toNorm Pi.normedRing Fin.fintype NormedCommRing.toNormedRing Int.instNormedCommRing Matrix.vecCons Matrix.vecEmpty	—	Asymptotics.IsTheta.add_isLittleO Asymptotics.isTheta_norm_left Asymptotics.isTheta_refl isLittleO_const_left_of_properSpace_of_discreteTopology Pi.discreteTopology Finite.of_fintype instDiscreteTopologyInt pi_properSpace Int.instProperSpace

---

← Back to Index