Theorems · Definition · measure theory
Real.circleAverage
{E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℂ → E) → ℂ → ℝ → EDefine circleAverage f c R as the average value of f on the circle with center c and radius
R. This is a real notion, which should not be confused with the complex path integral notion
defined in circleIntegral (integrating with respect to dz).
- Cited by
- 106 results in Mathlib
- Foundations
- Depth 251 from the axioms, rests on 7,985 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Complexstatement and proof · cited by 5,565
- Real.piproof · cited by 1,774
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- intervalIntegralproof · cited by 546
- circleMapproof · cited by 117
Cited by108
Results whose statement or proof uses this declaration.
- ValueDistribution.proximityproof · cited by 28
- Polynomial.logMahlerMeasureproof · cited by 21
- Real.circleAverage_congr_spherestatement · cited by 9
- Real.circleAverage_conststatement · cited by 9
- Real.circleAverage_addstatement and proof · cited by 6
- Real.circleAverage_zerostatement · cited by 6
- InnerProductSpace.HarmonicOnNhd.circleAverage_eqstatement · cited by 5
- Polynomial.mahlerMeasure_mulproof · cited by 5
- Real.circleAverage_congr_codiscreteWithinstatement · cited by 4
- circleAverage_log_norm_sub_const_eq_posLogstatement · cited by 4
- Polynomial.logMahlerMeasure_eq_log_MahlerMeasureproof · cited by 4
- ContinuousLinearMap.circleAverage_comp_commstatement · cited by 4