Documentation Verification Report

SpecificAsymptotics

📁 Source: Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

Statistics

Metric	Count
Definitions	0
Theorems `trans_tendsto_norm_atTop`, `rpow`, `sum_range`, `isEquivalent_nat_ceil`, `isEquivalent_nat_floor`, `isLittleO_pow_pow_atTop_of_lt`, `isLittleO_sum_range_of_tendsto_zero`, `isLittleO_sub_self_inv`, `cesaro`, `cesaro_smul`, `pow_div_pow_eventuallyEq_atBot`, `pow_div_pow_eventuallyEq_atTop`, `tendsto_pow_div_pow_atTop_atTop`, `tendsto_pow_div_pow_atTop_zero`	14
Total	14

Asymptotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEquivalent_nat_ceil` 📖	mathematical	—	`IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Nat.ceil` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `FloorRing.toFloorSemiring`	—	`isEquivalent_of_tendsto_one` `tendsto_nat_ceil_div_atTop`
`isEquivalent_nat_floor` 📖	mathematical	—	`IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Nat.floor` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `FloorRing.toFloorSemiring`	—	`isEquivalent_of_tendsto_one` `tendsto_nat_floor_div_atTop`
`isLittleO_pow_pow_atTop_of_lt` 📖	mathematical	—	`IsLittleO` `NormedField.toNorm` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`isLittleO_iff_tendsto'` `Filter.Eventually.mono` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `LT.lt.ne'` `tendsto_pow_div_pow_atTop_zero`
`isLittleO_sum_range_of_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`IsLittleO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Real.instNatCast`	—	`IsLittleO.sum_range` `isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `zero_le_one` `Real.instZeroLEOneClass` `Finset.sum_const` `Finset.card_range` `Nat.smul_one_eq_cast` `tendsto_natCast_atTop_atTop` `Real.instIsOrderedRing` `Real.instArchimedean`

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans_tendsto_norm_atTop` 📖	—	`Asymptotics.IsBigO` `NormedField.toNorm` `Filter.Tendsto` `Real` `Norm.norm` `Filter.atTop` `Real.instPreorder`	—	—	`exists_pos` `mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `LT.lt.ne` `Filter.Tendsto.atTop_div_const` `Real.instIsStrictOrderedRing` `Filter.tendsto_atTop_mono'` `Asymptotics.IsBigOWith_def`

Asymptotics.IsEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rpow` 📖	mathematical	`Pi.hasLe` `Real` `Real.instLE` `Pi.instZero` `Real.instZero` `Asymptotics.IsEquivalent` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Pi.instPow` `Real.instPow`	—	`exists_eq_mul` `Asymptotics.isEquivalent_iff_exists_eq_mul` `Real.one_rpow` `Filter.Tendsto.comp` `Real.continuousAt_rpow_const` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Nat.cast_zero` `Filter.mp_mem` `Filter.Tendsto.eventually_const_lt` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Filter.univ_mem'` `Real.mul_rpow` `le_of_lt`

Asymptotics.IsLittleO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_range` 📖	mathematical	`Asymptotics.IsLittleO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Pi.hasLe` `Real.instLE` `Pi.instZero` `Real.instZero` `Filter.Tendsto` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.instPreorder`	`ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Real.norm_of_nonneg` `Real.norm_eq_abs` `Finset.abs_sum_of_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Asymptotics.isLittleO_iff` `Nat.instAtLeastTwoHAddOfNat` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Asymptotics.isLittleO_const_left` `Filter.Tendsto.congr` `Filter.mp_mem` `Filter.Ici_mem_atTop` `Filter.univ_mem'` `Finset.sum_range_add_sum_Ico` `norm_add_le` `add_le_add` `covariant_swap_add_of_covariant_add` `le_rfl` `norm_sum_le_of_le` `Finset.mem_Ico` `add_le_add_right` `Finset.sum_le_sum_of_subset_of_nonneg` `Finset.range_eq_Ico` `Finset.Ico_subset_Ico` `zero_le` `Nat.instCanonicallyOrderedAdd` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `Finset.mul_sum` `add_le_add_left` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.add_pf_zero_add`

Filter.IsBoundedUnder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLittleO_sub_self_inv` 📖	mathematical	`Filter.IsBoundedUnder` `Real` `Real.instLE` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Norm.norm`	`Asymptotics.IsLittleO` `NormedField.toNorm` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`Asymptotics.IsBigO.trans_isLittleO` `isBigO_const` `one_ne_zero'` `NeZero.charZero_one` `RCLike.charZero_rclike` `Asymptotics.isLittleO_const_left` `norm_inv` `Filter.Tendsto.inv_tendsto_nhdsGT_zero` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_norm_sub_self_nhdsNE`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cesaro` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.instMul` `Real.instInv` `Real.instNatCast` `Finset.sum` `Real.instAddCommMonoid` `Finset.range`	—	`cesaro_smul`
`cesaro_smul` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Real.instNatCast` `Finset.sum` `Finset.range`	—	`tendsto_sub_nhds_zero_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Asymptotics.isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `Asymptotics.isLittleO_sum_range_of_tendsto_zero` `Asymptotics.IsLittleO.congr'` `Asymptotics.IsBigO.smul_isLittleO` `NormedSpace.toIsBoundedSMul` `NormedSpace.toNormSMulClass` `Asymptotics.isBigO_refl` `Filter.mp_mem` `Filter.Ici_mem_atTop` `Filter.univ_mem'` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `Finset.sum_sub_distrib` `Finset.sum_const` `Finset.card_range` `smul_sub` `Nat.cast_smul_eq_nsmul` `smul_smul` `inv_mul_cancel₀` `LT.lt.ne'` `one_smul` `smul_eq_mul`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_div_pow_eventuallyEq_atBot` 📖	mathematical	—	`Filter.EventuallyEq` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivInvMonoid.toZPow`	—	`Filter.Eventually.mono` `Filter.eventually_lt_atBot` `instNoBotOrderOfNoMinOrder` `instNoMinOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `zpow_sub₀` `LT.lt.ne` `zpow_natCast`
`pow_div_pow_eventuallyEq_atTop` 📖	mathematical	—	`Filter.EventuallyEq` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivInvMonoid.toZPow`	—	`Filter.Eventually.mono` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `zpow_sub₀` `LT.lt.ne'` `zpow_natCast`
`tendsto_pow_div_pow_atTop_atTop` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Filter.tendsto_congr'` `pow_div_pow_eventuallyEq_atTop` `Filter.tendsto_zpow_atTop_atTop`
`tendsto_pow_div_pow_atTop_zero` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`Filter.tendsto_congr'` `pow_div_pow_eventuallyEq_atTop` `tendsto_zpow_atTop_zero`

---

← Back to Index