Documentation Verification Report

Bounds

📁 Source: Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean

Statistics

Metric	Count
Definitions `F_int`, `F_nat`, `f_int`, `f_nat`, `g_nat`	5
Theorems `F_int_eq_of_mem_Icc`, `F_nat_one_le`, `F_nat_zero_le`, `F_nat_zero_zero_sub_le`, `f_int_negSucc`, `f_int_ofNat`, `f_le_g_nat`, `isBigO_atTop_F_int_one`, `isBigO_atTop_F_int_zero_sub`, `isBigO_atTop_F_nat_one`, `isBigO_atTop_F_nat_zero_sub`, `isBigO_exp_neg_mul_of_le`, `summable_f_int`, `summable_f_nat`	14
Total	19

HurwitzKernelBounds

Definitions

Name	Category	Theorems
`F_int` 📖	CompOp	3 math math: `isBigO_atTop_F_int_one`, `F_int_eq_of_mem_Icc`, `isBigO_atTop_F_int_zero_sub`
`F_nat` 📖	CompOp	6 math math: `F_nat_one_le`, `isBigO_atTop_F_nat_one`, `isBigO_atTop_F_nat_zero_sub`, `F_int_eq_of_mem_Icc`, `F_nat_zero_zero_sub_le`, `F_nat_zero_le`
`f_int` 📖	CompOp	3 math math: `f_int_negSucc`, `f_int_ofNat`, `summable_f_int`
`f_nat` 📖	CompOp	4 math math: `f_int_negSucc`, `f_le_g_nat`, `summable_f_nat`, `f_int_ofNat`
`g_nat` 📖	CompOp	1 math math: `f_le_g_nat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`F_int_eq_of_mem_Icc` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne` `Real.instLT`	`F_int` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instAdd` `F_nat` `Real.instSub`	—	`f_int_ofNat` `f_int_negSucc` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Summable.hasSum` `summable_f_nat`
`F_nat_one_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Norm.norm` `Real.norm` `F_nat` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instMul` `Real.instNeg` `Real.pi` `Monoid.toNatPow` `Real.instMonoid` `Real.instOne` `Real.instSub`	—	`tsum_of_norm_bounded` `pow_one` `add_mul` `Distrib.rightDistribClass` `HasSum.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.abs_exp` `mul_comm` `Real.exp_nat_mul` `mul_assoc` `Real.exp_add` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.neg_congr` `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_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.RingNF.nat_rawCast_1` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Mathlib.Tactic.RingNF.add_neg` `mul_add` `Distrib.leftDistribClass` `mul_div_assoc` `HasSum.mul_left` `hasSum_coe_mul_geometric_of_norm_lt_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `hasSum_geometric_of_lt_one` `LT.lt.le` `Real.exp_pos` `f_le_g_nat`
`F_nat_zero_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Norm.norm` `Real.norm` `F_nat` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instMul` `Real.instNeg` `Real.pi` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `Real.instOne`	—	`tsum_of_norm_bounded` `Real.exp_nat_mul` `Real.exp_add` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.neg_congr` `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.cast_pos` `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.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.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Mathlib.Tactic.RingNF.add_neg` `Mathlib.Tactic.Ring.add_pf_add_gt` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasSum_geometric_of_lt_one` `LT.lt.le` `Real.exp_pos` `f_le_g_nat`
`F_nat_zero_zero_sub_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `Real.norm` `Real.instSub` `F_nat` `Real.instOne` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instMul` `Real.instNeg` `Real.pi`	—	`F_nat.eq_1` `Summable.tsum_eq_zero_add` `instIsTopologicalAddGroupReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `summable_f_nat` `f_nat.eq_1` `Nat.cast_zero` `add_zero` `pow_zero` `one_mul` `pow_two` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Real.exp_zero` `add_comm` `add_sub_cancel_right` `Nat.cast_add` `Nat.cast_one` `one_pow` `mul_one` `F_nat_zero_le` `zero_le_one` `Real.instZeroLEOneClass`
`f_int_negSucc` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`f_int` `f_nat` `Real.instSub`	—	`Int.cast_negSucc` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_mul` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `f_int.eq_1` `f_nat.eq_1` `abs_neg` `neg_sq` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_nonpos` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.natCast_nonneg` `Mathlib.Tactic.Linarith.sub_neg_of_lt`
`f_int_ofNat` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`f_int` `f_nat`	—	`f_int.eq_1` `f_nat.eq_1` `Int.cast_natCast` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_nonneg` `Nat.cast_nonneg'` `Real.instZeroLEOneClass`
`f_le_g_nat` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Norm.norm` `Real.norm` `f_nat` `g_nat`	—	`f_nat.eq_1` `Real.norm_of_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `le_of_lt` `Real.exp_pos` `g_nat.eq_1` `Nat.instAtLeastTwoHAddOfNat` `add_sq` `neg_mul` `mul_le_mul_of_nonneg_left` `Real.exp_monotone` `neg_le_neg` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `add_le_add_left` `covariant_swap_add_of_covariant_add` `RCLike.charZero_rclike` `two_ne_zero` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.LinearCombination.le_of_le` `Real.instIsOrderedCancelAddMonoid` `add_le_add` `Mathlib.Tactic.LinearCombination.le_rearrange` `Mathlib.Tactic.Ring.le_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `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_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `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_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `le_refl` `Real.pi_pos`
`isBigO_atTop_F_int_one` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Asymptotics.IsBigO` `Real.norm` `Filter.atTop` `Real.instPreorder` `F_int` `Real.exp` `Real.instMul` `Real.instNeg`	—	`AddCircle.eq_coe_Ico` `Real.instIsOrderedAddMonoid` `ZeroLEOneClass.factZeroLtOne` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.instArchimedean` `isBigO_atTop_F_nat_one` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.le` `lt_min` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.univ_mem'` `F_int_eq_of_mem_Icc` `Set.Ico_subset_Icc_self` `Asymptotics.IsBigO.trans` `Filter.EventuallyEq.isBigO` `Asymptotics.IsBigO.add` `isBigO_exp_neg_mul_of_le` `min_le_left` `min_le_right`
`isBigO_atTop_F_int_zero_sub` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Asymptotics.IsBigO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.instSub` `F_int` `UnitAddCircle` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `QuotientAddGroup.Quotient.addCommGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `AddCommGroup.toAddGroup` `Real.instOne` `QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem` `AddSubgroup.decidableMemZMultiples` `Real.instAddGroup` `Real.exp` `Real.instMul` `Real.instNeg`	—	`AddCircle.eq_coe_Ico` `Real.instIsOrderedAddMonoid` `ZeroLEOneClass.factZeroLtOne` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.instArchimedean` `isBigO_atTop_F_nat_zero_sub` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.le` `AddCircle.coe_eq_zero_iff_of_mem_Ico` `lt_min` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.univ_mem'` `F_int_eq_of_mem_Icc` `Set.Ico_subset_Icc_self` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Asymptotics.IsBigO.trans` `Filter.EventuallyEq.isBigO` `Asymptotics.IsBigO.add` `isBigO_exp_neg_mul_of_le` `min_le_left` `sub_zero` `eq_false_intro` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `min_le_right`
`isBigO_atTop_F_nat_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Real.instLT` `Asymptotics.IsBigO` `Real.norm` `Filter.atTop` `Real.instPreorder` `F_nat` `Real.exp` `Real.instMul` `Real.instNeg`	—	`inv_pow` `one_pow` `Asymptotics.IsBigO.pow` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass` `eq_or_lt_of_le` `Real.pi_pos` `zero_pow` `two_ne_zero` `zero_add` `mul_one` `MulZeroClass.zero_mul` `zero_div` `add_zero` `Asymptotics.IsBigO.mul` `Asymptotics.isBigO_refl` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `Real.instZeroLEOneClass` `Asymptotics.IsBigO.add` `Filter.Eventually.isBigO` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.univ_mem'` `Real.norm_of_nonneg` `LT.lt.le` `Real.exp_pos` `Real.exp_le_exp` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.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.mul_one` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `mul_div_assoc` `Asymptotics.IsBigO.const_mul_left` `Asymptotics.IsBigO.trans` `F_nat_one_le`
`isBigO_atTop_F_nat_zero_sub` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Real.instLT` `Asymptotics.IsBigO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.instSub` `F_nat` `Real.decidableEq` `Real.instOne` `Real.exp` `Real.instMul` `Real.instNeg`	—	`Filter.Eventually.isBigO` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.univ_mem'` `F_nat_zero_zero_sub_le` `Real.pi_pos` `Asymptotics.IsBigO.trans` `neg_mul` `mul_one` `Asymptotics.IsBigO.mul` `NormedDivisionRing.toNormMulClass` `Asymptotics.isBigO_refl` `sub_zero` `F_nat_zero_le` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `sq_pos_of_ne_zero` `AddGroup.existsAddOfLE`
`isBigO_exp_neg_mul_of_le` 📖	mathematical	`Real` `Real.instLE`	`Asymptotics.IsBigO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.exp` `Real.instMul` `Real.instNeg`	—	`Filter.Eventually.isBigO` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.univ_mem'` `Real.norm_of_nonneg` `LT.lt.le` `Real.exp_pos` `Real.exp_monotone` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `neg_le_neg` `Real.instIsOrderedAddMonoid` `le_of_lt`
`summable_f_int` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `f_int` `SummationFilter.unconditional`	—	`Summable.of_norm` `Real.instCompleteSpace` `Int.cast_natCast` `norm_mul` `NormedDivisionRing.toNormMulClass` `abs_pow` `Real.instIsOrderedRing` `abs_abs` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Int.cast_negSucc` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_mul` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `abs_neg` `neg_sq` `Summable.norm` `FiniteDimensional.rclike_to_real` `HasSum.summable` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Summable.hasSum` `summable_f_nat`
`summable_f_nat` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `f_nat` `SummationFilter.unconditional`	—	`Summable.of_norm_bounded` `Real.instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `Summable.comp_injective` `instIsUniformAddGroupReal` `Summable.mul_right` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_pow_mul_jacobiTheta₂_term_bound` `Nat.cast_injective` `Int.instCharZero` `mul_assoc` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `Int.cast_abs` `Real.instIsStrictOrderedRing` `Int.cast_natCast` `Nat.abs_cast` `Real.instIsOrderedRing` `Real.abs_exp` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.exp_monotone` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_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_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `mul_nonneg` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.pi_pos` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `neg_le_iff_add_nonneg` `neg_le_abs` `LT.lt.le` `two_pos` `NeZero.charZero_one` `RCLike.charZero_rclike` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Summable.of_norm_bounded_eventually_nat` `Summable.mul_left` `mul_le_mul_iff_of_pos_right` `IsOrderedRing.toMulPosMono` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.exp_pos` `abs_pow` `two_mul` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `pow_le_pow_left₀` `abs_nonneg` `LE.le.trans` `abs_add_le` `add_le_add` `Eq.le` `Nat.ceil_le`

---

← Back to Index