Documentation Verification Report

JensenFormula

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

Statistics

Metric	Count
Definitions	0
Theorems `circleAverage_log_norm_of_ne_zero`, `circleAverage_log_norm`, `circleAverage_log_norm_factorizedRational`, `countingFunction_finsum_eq_finsum_add`	4
Total	4

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_log_norm_of_ne_zero` 📖	mathematical	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`Real.circleAverage` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.log` `Norm.norm` `Complex.instNorm`	—	`HarmonicOnNhd.circleAverage_eq` `AnalyticAt.harmonicAt_log_norm`

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_log_norm` 📖	mathematical	`MeromorphicOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`Real.circleAverage` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.log` `Norm.norm` `Complex.instNorm` `Real.instAdd` `finsum` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NontriviallyNormedField.toNormedField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike` `divisor` `Real.instInv` `Complex.instSub` `meromorphicTrailingCoeffAt`	—	`Function.locallyFinsuppWithin.finiteSupport` `Complex.instT2Space` `ProperSpace.isCompact_closedBall` `Complex.instProperSpace` `extract_zeros_poles` `extract_zeros_poles_log` `Real.circleAverage_congr_codiscreteWithin` `Filter.codiscreteWithin.mono` `Metric.sphere_subset_closedBall` `Real.circleAverage_add` `circleIntegrable_log_norm_factorizedRational` `circleIntegrable_log_norm_meromorphicOn` `AnalyticOnNhd.meromorphicOn` `AnalyticOnNhd.mono` `circleAverage_log_norm_factorizedRational` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AnalyticOnNhd.circleAverage_log_norm_of_ne_zero` `dist_self` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `accPt_iff_frequently_nhdsNE` `Filter.compl_notMem` `PerfectSpace.not_isolated` `instPerfectSpace` `mem_nhdsWithin` `Metric.ball_subset_closedBall` `log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles` `add_sub_cancel_left` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `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_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `finsum_sub_distrib` `Set.Finite.subset` `Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike` `countingFunction_finsum_eq_finsum_add` `Function.locallyFinsuppWithin.ext` `divisor_apply` `exists_meromorphicOrderAt_ne_top_iff_forall` `Metric.nonempty_closedBall` `abs_nonneg` `Convex.isPreconnected` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `convex_closedBall` `WithTop.untop₀_top` `Function.locallyFinsuppWithin.apply_eq_zero_of_notMem` `Int.cast_zero` `MulZeroClass.zero_mul` `finsum_zero` `add_zero` `zero_add` `MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top` `norm_zero` `Real.log_zero` `Filter.mp_mem` `Filter.self_mem_codiscreteWithin` `meromorphicNFAt_mem_codiscreteWithin` `Filter.univ_mem'` `Int.instIsOrderedAddMonoid` `not_iff_not` `MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff` `mul_inv_rev` `intervalIntegral.integral_zero` `MulZeroClass.mul_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_log_norm_factorizedRational` 📖	mathematical	—	`Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `finsum` `Complex` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Metric.closedBall` `abs` `Real.lattice` `Real.instAddGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike` `Real.log` `Norm.norm` `Complex.instNorm` `Complex.instSub`	—	`Function.locallyFinsuppWithin.finiteSupport` `Complex.instT2Space` `ProperSpace.isCompact_closedBall` `Complex.instProperSpace` `finsum_eq_sum_of_support_subset` `Mathlib.Tactic.Contrapose.contrapose₁` `Set.Finite.coe_toFinset` `Int.cast_zero` `MulZeroClass.zero_mul` `Real.circleAverage_sum` `IntervalIntegrable.const_mul` `circleIntegrable_log_norm_meromorphicOn` `AnalyticOnNhd.meromorphicOn` `AnalyticOnNhd.sub` `analyticOnNhd_id` `analyticOnNhd_const` `Finset.sum_congr` `Real.circleAverage_fun_smul` `NormedSpace.toNormSMulClass` `Algebra.to_smulCommClass` `circleAverage_log_norm_sub_const_of_mem_closedBall` `Function.locallyFinsuppWithin.supportWithinDomain` `Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike`
`countingFunction_finsum_eq_finsum_add` 📖	mathematical	—	`finsum` `Real` `Complex` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `Real.instSub` `Real.log` `Norm.norm` `Complex.instNorm` `Complex.instSub` `Real.instAdd` `Real.instInv`	—	`Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike` `Set.Finite.coe_toFinset` `finsum_eq_sum_of_support_subset` `Finset.sum_eq_sum_diff_singleton_add` `Set.Finite.mem_toFinset` `sub_self` `norm_zero` `Real.log_zero` `sub_zero` `inv_zero` `MulZeroClass.mul_zero` `add_zero` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.sum_congr` `Real.log_mul` `inv_ne_zero` `norm_ne_zero_iff` `Iff.not` `sub_eq_zero` `Real.log_inv` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `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_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `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.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Int.cast_zero` `MulZeroClass.zero_mul` `finsum_congr`

---

← Back to Index