Documentation Verification Report

MeanValue

📁 Source: Mathlib/Analysis/Complex/Harmonic/MeanValue.lean

Statistics

Metric	Count
Definitions	0
Theorems `circleAverage_eq`, `circleAverage_eq`	2
Total	2

HarmonicContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_eq` 📖	mathematical	`InnerProductSpace.HarmonicContOnCl` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup`	`Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`Complex.instFiniteDimensionalReal` `Real.circleAverage_zero` `Real.instCompleteSpace` `Real.ContinuousOn.circleAverage` `ContinuousOn.mono` `InnerProductSpace.HarmonicContOnCl.continuousOn` `closure_ball` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mem_closedBall_iff_norm` `LT.lt.le` `Real.circleAverage_abs_radius` `Real.ContinuousOn.eq_of_eqOn_Ioo` `HarmonicOnNhd.circleAverage_eq` `InnerProductSpace.HarmonicOnNhd.mono` `InnerProductSpace.HarmonicContOnCl.harmonicOnNhd` `abs_of_pos` `Metric.closedBall_subset_ball`

HarmonicOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_eq` 📖	mathematical	`InnerProductSpace.HarmonicOnNhd` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup`	`Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`Complex.instFiniteDimensionalReal` `IsCompact.exists_thickening_subset_open` `ProperSpace.isCompact_closedBall` `Complex.instProperSpace` `InnerProductSpace.isOpen_setOf_harmonicAt` `InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq` `thickening_closedBall` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `AnalyticAt.differentiableWithinAt` `Metric.sphere_subset_ball` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Real.circleAverage_congr_sphere` `ContinuousLinearMap.circleAverage_comp_comm` `Real.instCompleteSpace` `Complex.instCompleteSpace` `ContinuousOn.circleIntegrable'` `ContinuousOn.mono` `AnalyticOnNhd.continuousOn` `dist_eq_norm` `DiffContOnCl.circleAverage` `DifferentiableOn.diffContOnCl` `dist_self` `add_pos_of_pos_of_nonneg`

---

← Back to Index