Documentation Verification Report

Analytic

📁 Source: Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean

Statistics

Metric	Count
Definitions	0
Theorems `clog`, `cpow`, `im_ofReal`, `re_ofReal`, `clog`, `cpow`, `im_ofReal`, `re_ofReal`, `clog`, `cpow`, `im_ofReal`, `re_ofReal`, `clog`, `cpow`, `im_ofReal`, `re_ofReal`, `analyticAt_clog`, `analyticAt_log`, `analyticOnNhd_log`, `analyticOn_log`	20
Total	20

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.log`	—	`comp` `analyticAt_clog`
`cpow` 📖	mathematical	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`analyticWithinAt_univ` `AnalyticWithinAt.cpow`
`im_ofReal` 📖	mathematical	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Complex.ofReal`	`Real` `Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.im`	—	`comp` `ContinuousLinearMap.analyticAt` `restrictScalars` `IsScalarTower.right`
`re_ofReal` 📖	mathematical	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Complex.ofReal`	`Real` `Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.re`	—	`comp` `ContinuousLinearMap.analyticAt` `restrictScalars` `IsScalarTower.right`

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.log`	—	`AnalyticWithinAt.comp` `AnalyticAt.analyticWithinAt` `analyticAt_clog`
`cpow` 📖	mathematical	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`AnalyticWithinAt.cpow`
`im_ofReal` 📖	mathematical	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.image` `Real` `Complex.ofReal`	`Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.im`	—	`comp` `ContinuousLinearMap.analyticOn` `restrictScalars` `IsScalarTower.right` `Set.mapsTo_image`
`re_ofReal` 📖	mathematical	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.image` `Real` `Complex.ofReal`	`Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.re`	—	`comp` `ContinuousLinearMap.analyticOn` `restrictScalars` `IsScalarTower.right` `Set.mapsTo_image`

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.log`	—	`AnalyticAt.comp` `analyticAt_clog`
`cpow` 📖	mathematical	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`AnalyticAt.cpow`
`im_ofReal` 📖	mathematical	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.image` `Real` `Complex.ofReal`	`Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.im`	—	`comp` `ContinuousLinearMap.analyticOnNhd` `restrictScalars` `IsScalarTower.right` `Set.mapsTo_image`
`re_ofReal` 📖	mathematical	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.image` `Real` `Complex.ofReal`	`Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.re`	—	`comp` `ContinuousLinearMap.analyticOnNhd` `restrictScalars` `IsScalarTower.right` `Set.mapsTo_image`

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`AnalyticWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.log`	—	`AnalyticAt.comp_analyticWithinAt` `analyticAt_clog`
`cpow` 📖	mathematical	`AnalyticWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`Filter.mp_mem` `Filter.Tendsto.eventually_ne` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `continuousWithinAt_insert` `Complex.slitPlane_ne_zero` `Filter.univ_mem'` `congr_of_eventuallyEq_insert` `cexp` `mul` `clog`
`im_ofReal` 📖	mathematical	`AnalyticWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.image` `Real` `Complex.ofReal`	`Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.im`	—	`comp` `ContinuousLinearMap.analyticWithinAt` `restrictScalars` `IsScalarTower.right` `Set.mapsTo_image`
`re_ofReal` 📖	mathematical	`AnalyticWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.image` `Real` `Complex.ofReal`	`Real.denselyNormedField` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Complex.re`	—	`comp` `ContinuousLinearMap.analyticWithinAt` `restrictScalars` `IsScalarTower.right` `Set.mapsTo_image`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt_clog` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Complex.slitPlane`	`AnalyticAt` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Complex.log`	—	`Complex.analyticAt_iff_eventually_differentiableAt` `Complex.instCompleteSpace` `Filter.mp_mem` `IsOpen.eventually_mem` `Complex.isOpen_slitPlane` `Filter.univ_mem'` `DifferentiableAt.clog` `differentiableAt_id`
`analyticAt_log` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`AnalyticAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log`	—	`Complex.log_ofReal_re` `AnalyticAt.re_ofReal` `analyticAt_clog`
`analyticOnNhd_log` 📖	mathematical	—	`AnalyticOnNhd` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log` `Set.Ioi` `Real.instPreorder` `Real.instZero`	—	`analyticAt_log`
`analyticOn_log` 📖	mathematical	—	`AnalyticOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log` `Set.Ioi` `Real.instPreorder` `Real.instZero`	—	`AnalyticOnNhd.analyticOn` `analyticOnNhd_log`

---

← Back to Index