MeanValue

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

Statistics

Metric	Count
Definitions	0
Theorems circleAverage_eq	1
Total	1

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	—	Complex.instFiniteDimensionalReal IsCompact.exists_thickening_subset_open ProperSpace.isCompact_closedBall Complex.instProperSpace InnerProductSpace.isOpen_setOf_harmonicAt harmonic_is_realOfHolomorphic 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 AddRightCancelSemigroup.toIsRightCancelAdd Real.circleAverage_congr_sphere ContinuousLinearMap.circleAverage_comp_comm Real.instCompleteSpace Complex.instCompleteSpace ContinuousOn.circleIntegrable' ContinuousOn.mono AnalyticOnNhd.continuousOn dist_eq_norm contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le DiffContOnCl.circleAverage DifferentiableOn.diffContOnCl dist_self add_pos_of_pos_of_nonneg

---

← Back to Index