Documentation Verification Report

Asymptotics

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

Statistics

Metric	Count
Definitions	0
Theorems `isBigO_comp_ofReal_nhds`, `isBigO_comp_ofReal_nhds_ne`, `isBigO_im_sub_im`, `isBigO_ofReal_left`, `isBigO_ofReal_right`, `isBigO_re_sub_re`, `isLittleO_ofReal_left`, `isLittleO_ofReal_right`, `isTheta_ofReal`, `isTheta_ofReal_left`, `isTheta_ofReal_right`, `cast_complex_isTheta_cast_real`	12
Total	12

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBigO_comp_ofReal_nhds` 📖	mathematical	`Asymptotics.IsBigO` `Complex` `instNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ofReal`	`Real` `Real.pseudoMetricSpace`	—	`Asymptotics.IsBigO.comp_tendsto` `Continuous.tendsto` `continuous_ofReal`
`isBigO_comp_ofReal_nhds_ne` 📖	mathematical	`Asymptotics.IsBigO` `Complex` `instNorm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ofReal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`Real` `Real.pseudoMetricSpace`	—	`Asymptotics.IsBigO.comp_tendsto` `ContinuousWithinAt.tendsto_nhdsWithin` `Continuous.continuousWithinAt` `continuous_ofReal`
`isBigO_im_sub_im` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `Real` `Real.norm` `instNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Real.instSub` `im` `instSub`	—	`Asymptotics.isBigO_of_le` `abs_im_le_norm`
`isBigO_ofReal_left` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `instNorm` `ofReal` `Real` `Real.norm`	—	`Asymptotics.IsTheta.isBigO_congr_left` `isTheta_ofReal`
`isBigO_ofReal_right` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `instNorm` `ofReal` `Real` `Real.norm`	—	`Asymptotics.IsTheta.isBigO_congr_right` `isTheta_ofReal`
`isBigO_re_sub_re` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `Real` `Real.norm` `instNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Real.instSub` `re` `instSub`	—	`Asymptotics.isBigO_of_le` `abs_re_le_norm`
`isLittleO_ofReal_left` 📖	mathematical	—	`Asymptotics.IsLittleO` `Complex` `instNorm` `ofReal` `Real` `Real.norm`	—	`Asymptotics.IsTheta.isLittleO_congr_left` `isTheta_ofReal`
`isLittleO_ofReal_right` 📖	mathematical	—	`Asymptotics.IsLittleO` `Complex` `instNorm` `ofReal` `Real` `Real.norm`	—	`Asymptotics.IsTheta.isLittleO_congr_right` `isTheta_ofReal`
`isTheta_ofReal` 📖	mathematical	—	`Asymptotics.IsTheta` `Complex` `Real` `instNorm` `Real.norm` `ofReal`	—	`Asymptotics.IsTheta.of_norm_left` `norm_real` `Asymptotics.IsTheta.norm_left` `Asymptotics.isTheta_rfl`
`isTheta_ofReal_left` 📖	mathematical	—	`Asymptotics.IsTheta` `Complex` `instNorm` `ofReal` `Real` `Real.norm`	—	`Asymptotics.IsTheta.isTheta_congr_left` `isTheta_ofReal`
`isTheta_ofReal_right` 📖	mathematical	—	`Asymptotics.IsTheta` `Complex` `instNorm` `ofReal` `Real` `Real.norm`	—	`Asymptotics.IsTheta.isTheta_congr_right` `isTheta_ofReal`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_complex_isTheta_cast_real` 📖	mathematical	—	`Asymptotics.IsTheta` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.cofinite` `Complex.instIntCast` `Real.instIntCast`	—	`Asymptotics.IsTheta.of_norm_eventuallyEq_norm` `Filter.univ_mem'` `Complex.norm_intCast`

---

← Back to Index