Documentation Verification Report

LocallyUniformLimit

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

Statistics

Metric	Count
Definitions `cderiv`	1
Theorems `cderiv_eq_deriv`, `cderiv_sub`, `differentiableOn_tsum_of_summable_norm`, `exists_cthickening_tendstoUniformlyOn`, `hasSum_deriv_of_summable_norm`, `logDeriv_tendsto`, `norm_cderiv_le`, `norm_cderiv_lt`, `norm_cderiv_sub_lt`, `tendstoUniformlyOn_deriv_of_cthickening_subset`, `deriv`, `differentiableOn`, `cderiv`	13
Total	14

Complex

Definitions

Name	Category	Theorems
`cderiv` 📖	CompOp	8 math math: `cderiv_eq_deriv`, `norm_cderiv_le`, `norm_cderiv_sub_lt`, `TendstoUniformlyOn.cderiv`, `exists_cthickening_tendstoUniformlyOn`, `cderiv_sub`, `tendstoUniformlyOn_deriv_of_cthickening_subset`, `norm_cderiv_lt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cderiv_eq_deriv` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLT` `Real.instZero` `Set` `Set.instHasSubset` `Metric.closedBall`	`cderiv` `deriv`	—	`two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable` `Metric.mem_ball_self`
`cderiv_sub` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere`	`cderiv` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`ContinuousOn.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.continuousOn` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_id'` `continuous_const` `LT.lt.ne` `norm_zero` `sq_eq_zero_iff` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `mem_sphere_iff_norm` `smul_sub` `circleIntegral.integral_sub` `ContinuousOn.circleIntegrable` `LT.lt.le` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`differentiableOn_tsum_of_summable_norm` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SummationFilter.unconditional` `DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsOpen` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`TendstoUniformlyOn.tendstoLocallyUniformlyOn` `tendstoUniformlyOn_tsum` `TendstoLocallyUniformlyOn.differentiableOn` `Filter.atTop_neBot` `Finset.isDirected_le` `Filter.Eventually.of_forall` `DifferentiableOn.fun_sum`
`exists_cthickening_tendstoUniformlyOn` 📖	mathematical	`TendstoLocallyUniformlyOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Eventually` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `IsCompact` `IsOpen` `Set` `Set.instHasSubset`	`Real` `Real.instLT` `Real.instZero` `Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `TendstoUniformlyOn` `deriv` `cderiv`	—	`IsCompact.exists_cthickening_subset_open` `tendstoUniformlyOn_deriv_of_cthickening_subset`
`hasSum_deriv_of_summable_norm` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SummationFilter.unconditional` `DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsOpen` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Set` `Set.instMembership`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `deriv` `tsum`	—	`HasSum.eq_1` `TendstoUniformlyOn.tendstoLocallyUniformlyOn` `tendstoUniformlyOn_tsum` `deriv_fun_sum` `DifferentiableOn.differentiableAt` `IsOpen.mem_nhds` `TendstoLocallyUniformlyOn.tendsto_at` `TendstoLocallyUniformlyOn.deriv` `Filter.Eventually.of_forall` `DifferentiableOn.fun_sum`
`logDeriv_tendsto` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Set` `Set.instMembership` `TendstoLocallyUniformlyOn` `Filter.Eventually` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf`	`Filter.Tendsto` `logDeriv` `NormedAlgebra.id` `NontriviallyNormedField.toNormedField` `nhds`	—	`Filter.Tendsto.div` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `TendstoLocallyUniformlyOn.tendsto_at` `TendstoLocallyUniformlyOn.deriv` `instCompleteSpace`
`norm_cderiv_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	`cderiv` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`NormedSpace.sphere_nonempty` `EMetric.instNontrivialTopologyOfNontrivial` `instNontrivial` `LT.lt.le` `LE.le.trans` `norm_nonneg` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `inv_mul_eq_div` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `sq_pos_of_pos` `le_rfl` `Nat.instAtLeastTwoHAddOfNat` `circleIntegral.norm_integral_le_of_norm_le_const` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `le_of_eq` `mul_inv_rev` `inv_I` `neg_mul` `norm_neg` `norm_mul` `norm_I` `norm_real` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.pi_pos` `norm_ofNat` `one_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`norm_cderiv_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere`	`cderiv` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`NormedSpace.sphere_nonempty` `EMetric.instNontrivialTopologyOfNontrivial` `instNontrivial` `LT.lt.le` `Continuous.comp_continuousOn` `continuous_norm` `IsCompact.exists_isMaxOn` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `isCompact_sphere` `instProperSpace` `LE.le.trans_lt` `norm_cderiv_le` `div_lt_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing`
`norm_cderiv_sub_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere`	`cderiv` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`norm_cderiv_lt` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `cderiv_sub`
`tendstoUniformlyOn_deriv_of_cthickening_subset` 📖	mathematical	`TendstoLocallyUniformlyOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Eventually` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real` `Real.instLT` `Real.instZero` `IsCompact` `IsOpen` `Set` `Set.instHasSubset` `Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace`	`TendstoUniformlyOn` `deriv` `cderiv`	—	`Filter.mp_mem` `Filter.univ_mem'` `ContinuousOn.mono` `DifferentiableOn.continuousOn` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsCompact.cthickening` `instProperSpace` `tendstoLocallyUniformlyOn_iff_forall_isCompact` `locallyCompact_of_proper` `TendstoUniformlyOn.congr` `TendstoUniformlyOn.cderiv` `cderiv_eq_deriv` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.closedBall_subset_cthickening`

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv` 📖	mathematical	`TendstoLocallyUniformlyOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Eventually` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `IsOpen`	`deriv`	—	`tendstoLocallyUniformlyOn_iff_forall_isCompact` `locallyCompact_of_proper` `Complex.instProperSpace` `Filter.eq_or_neBot` `Complex.exists_cthickening_tendstoUniformlyOn` `TendstoUniformlyOn.congr_right` `Complex.cderiv_eq_deriv` `differentiableOn` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.closedBall_subset_cthickening`
`differentiableOn` 📖	—	`TendstoLocallyUniformlyOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Eventually` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `IsOpen`	—	—	`Filter.HasBasis.mem_iff` `compact_basis_nhds` `locallyCompact_of_proper` `Complex.instProperSpace` `IsOpen.mem_nhds` `Complex.exists_cthickening_tendstoUniformlyOn` `HasSubset.Subset.trans` `Set.instIsTransSubset` `interior_subset` `Filter.mp_mem` `Filter.univ_mem'` `DifferentiableOn.mono` `mono` `TendstoUniformlyOn.tendstoLocallyUniformlyOn` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `hasDerivAt_of_tendsto_locally_uniformly_on'` `instIsRCLikeNormedField` `isOpen_interior` `tendsto_at` `DifferentiableAt.differentiableWithinAt` `HasDerivAt.differentiableAt` `DifferentiableOn.differentiableAt` `interior_mem_nhds`

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cderiv` 📖	mathematical	`TendstoUniformlyOn` `Complex` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `Complex.instNormedField` `Real` `Real.instLT` `Real.instZero` `Filter.Eventually` `ContinuousOn` `UniformSpace.toTopologicalSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`Complex.cderiv`	—	`Filter.eq_or_neBot` `continuousOn` `Filter.Eventually.frequently` `Metric.tendstoUniformlyOn_iff` `Filter.mp_mem` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.univ_mem'` `dist_eq_norm` `Metric.closedBall_subset_cthickening` `Metric.sphere_subset_closedBall` `HasSubset.Subset.trans` `Set.instIsTransSubset` `ContinuousOn.mono` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass` `LT.lt.ne` `Complex.norm_cderiv_sub_lt`

---

← Back to Index