CircleAverage

📁 Source: Mathlib/MeasureTheory/Integral/CircleAverage.lean

Statistics

Metric	Count
Definitions circleAverage	1
Theorems circleAverage_comp_comm, abs_circleAverage_le_circleAverage_abs, integral_undef, circleAverage_abs_radius, circleAverage_add, circleAverage_congr_codiscreteWithin, circleAverage_congr_sphere, circleAverage_const, circleAverage_const_on_circle, circleAverage_def, circleAverage_eq_circleAverage_zero_one, circleAverage_eq_circleIntegral, circleAverage_eq_integral_add, circleAverage_eq_intervalAverage, circleAverage_fun_add, circleAverage_fun_smul, circleAverage_fun_sub, circleAverage_fun_sum, circleAverage_map_add_const, circleAverage_mono, circleAverage_mono_on_of_le_circle, circleAverage_neg_radius, circleAverage_nonneg_of_nonneg, circleAverage_smul, circleAverage_sub, circleAverage_sum, circleAverage_zero, circleAverage_zero_one_congr_inv	28
Total	29

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage_comp_comm 📖	mathematical	CircleIntegrable	Real.circleAverage Complex DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField funLike	—	map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass intervalIntegral_comp_comm

Real

Definitions

Name	Category	Theorems
circleAverage 📖	CompOp	55 math math: circleAverage_map_add_const, ValueDistribution.proximity_zero, circleAverage_sub, circleAverage_log_norm_sub_const₁, circleAverage_log_norm_sub_const_of_mem_closedBall, circleAverage_sum, HarmonicOnNhd.circleAverage_eq, DiffContOnCl.circleAverage, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, circleAverage_eq_circleIntegral, circleAverage_fun_sum, circleAverage_zero, circleAverage_log_norm_sub_const₀, circleAverage_neg_radius, AnalyticOnNhd.circleAverage_log_norm_of_ne_zero, circleAverage_def, circleAverage_mono_on_of_le_circle, DiffContOnCl.circleAverage_smul_div, Polynomial.logMahlerMeasure_def, circleAverage_eq_integral_add, circleAverage_congr_codiscreteWithin, ValueDistribution.characteristic_sub_characteristic_inv, circleAverage_eq_circleAverage_zero_one, circleAverage_congr_sphere, circleAverage_fun_smul, circleAverage_smul, Polynomial.sum_sq_norm_coeff_eq_circleAverage, abs_circleAverage_le_circleAverage_abs, circleAverage_log_norm_add_const_eq_posLog, MeromorphicOn.circleAverage_log_norm, circleAverage.integral_undef, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, circleAverage_sub_sub_inv_smul_of_differentiable_on, ValueDistribution.proximity_zero_of_complexValued, circleAverage_log_norm_sub_const_eq_posLog, circleAverage_log_norm_factorizedRational, circleAverage_of_differentiable_on_off_countable, circleAverage_log_norm_sub_const₂, circleAverage_eq_intervalAverage, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, circleAverage_abs_radius, circleAverage_zero_one_congr_inv, circleAverage_of_differentiable_on, circleAverage_mono, circleAverage_add, ValueDistribution.proximity_coe, circleAverage_fun_add, circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable, ValueDistribution.proximity_top, circleAverage_nonneg_of_nonneg, ContinuousLinearMap.circleAverage_comp_comm, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, circleAverage_const, circleAverage_const_on_circle, circleAverage_fun_sub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_circleAverage_le_circleAverage_abs 📖	mathematical	—	Real instLE abs lattice instAddGroup circleAverage normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.instLattice Complex Pi.addGroup	—	circleAverage.eq_1 smul_eq_mul abs_mul instIsOrderedRing Nat.instAtLeastTwoHAddOfNat abs_of_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing two_pi_pos mul_le_mul_iff_of_pos_left IsOrderedRing.toPosMulMono intervalIntegral.abs_integral_le_integral_abs le_of_lt
circleAverage_abs_radius 📖	mathematical	—	circleAverage abs Real lattice instAddGroup	—	abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid abs_of_neg circleAverage_neg_radius
circleAverage_add 📖	mathematical	CircleIntegrable	circleAverage Pi.instAdd Complex AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	circleAverage.eq_1 smul_add intervalIntegral.integral_add
circleAverage_congr_codiscreteWithin 📖	mathematical	Filter.EventuallyEq Complex Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Metric.sphere abs Real lattice instAddGroup	circleAverage	—	intervalIntegral.integral_congr_ae_restrict ae_restrict_le_codiscreteWithin instSecondCountableTopologyReal noAtoms_volume measurableSet_uIoc BorelSpace.opensMeasurable borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid Filter.codiscreteWithin.mono circleMap_preimage_codiscrete
circleAverage_congr_sphere 📖	mathematical	Set.EqOn Complex Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField abs Real lattice instAddGroup	circleAverage	—	intervalIntegral.integral_congr circleMap_mem_sphere'
circleAverage_const 📖	mathematical	—	circleAverage	—	intervalIntegral.integral_const sub_zero IsScalarTower.left Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero mul_inv_cancel₀ one_smul
circleAverage_const_on_circle 📖	mathematical	—	circleAverage	—	circleAverage.eq_1 circleMap_mem_sphere' circleAverage_const
circleAverage_def 📖	mathematical	—	circleAverage Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instMonoid Module.toDistribMulAction semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule normedField instInv instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi intervalIntegral circleMap instZero MeasureTheory.MeasureSpace.volume measureSpace	—	—
circleAverage_eq_circleAverage_zero_one 📖	mathematical	—	circleAverage Complex Complex.instAdd Complex.instMul Complex.ofReal Complex.instZero Real instOne	—	Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left 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_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero
circleAverage_eq_circleIntegral 📖	mathematical	—	circleAverage NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instInv Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal pi Complex.I circleIntegral Complex.instSub	—	Nat.instAtLeastTwoHAddOfNat mul_inv_rev Complex.ofReal_mul Complex.ofReal_inv intervalIntegral.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal smulCommClass_self smul_smul Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one 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.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos deriv_circleMap circleMap_sub_center Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq circleMap_ne_center Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one
circleAverage_eq_integral_add 📖	mathematical	—	circleAverage Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instMonoid Module.toDistribMulAction semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule normedField instInv instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi intervalIntegral circleMap instAdd instZero MeasureTheory.MeasureSpace.volume measureSpace	—	Nat.instAtLeastTwoHAddOfNat intervalIntegral.integral_comp_add_right periodic_circleMap Function.Periodic.intervalIntegral_add_eq zero_add mul_inv_rev add_comm
circleAverage_eq_intervalAverage 📖	mathematical	—	circleAverage MeasureTheory.average Real MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.uIoc linearOrder instZero instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi circleMap	—	Nat.instAtLeastTwoHAddOfNat mul_inv_rev interval_average_eq sub_zero
circleAverage_fun_add 📖	mathematical	CircleIntegrable	circleAverage AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	circleAverage_add
circleAverage_fun_smul 📖	mathematical	—	circleAverage SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	circleAverage_smul
circleAverage_fun_sub 📖	mathematical	CircleIntegrable	circleAverage SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	circleAverage_sub
circleAverage_fun_sum 📖	mathematical	CircleIntegrable	circleAverage Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Finset.sum_apply circleAverage_sum
circleAverage_map_add_const 📖	mathematical	—	circleAverage Complex Complex.instAdd Complex.instZero	—	zero_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt
circleAverage_mono 📖	mathematical	CircleIntegrable Real normedAddCommGroup instLE	circleAverage InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	mul_le_mul_iff_of_pos_left IsOrderedRing.toPosMulMono instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing mul_inv_rev PosMulReflectLE.toPosMulReflectLT instNontrivial intervalIntegral.integral_mono_on_of_le_Ioo Nat.instAtLeastTwoHAddOfNat le_of_lt two_pi_pos noAtoms_volume circleMap_sub_center norm_circleMap_zero
circleAverage_mono_on_of_le_circle 📖	mathematical	CircleIntegrable Real normedAddCommGroup instLE	circleAverage InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	circleAverage_const instCompleteSpace circleAverage.eq_1 smul_eq_mul Nat.instAtLeastTwoHAddOfNat mul_le_mul_iff_of_pos_left IsOrderedRing.toPosMulMono instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing inv_pos PosMulReflectLE.toPosMulReflectLT two_pi_pos intervalIntegral.integral_mono_on_of_le_Ioo le_of_lt intervalIntegrable_const locallyFinite_volume enorm_ne_top noAtoms_volume circleMap_mem_sphere'
circleAverage_neg_radius 📖	mathematical	—	circleAverage Real instNeg	—	circleMap_neg_radius Nat.instAtLeastTwoHAddOfNat circleAverage_eq_integral_add
circleAverage_nonneg_of_nonneg 📖	mathematical	Real instLE instZero	circleAverage normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	circleAverage_const instCompleteSpace circleAverage.eq_1 smul_eq_mul Nat.instAtLeastTwoHAddOfNat mul_le_mul_iff_of_pos_left IsOrderedRing.toPosMulMono instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing inv_pos PosMulReflectLE.toPosMulReflectLT two_pi_pos intervalIntegral.integral_mono_on_of_le_Ioo le_of_lt intervalIntegrable_const locallyFinite_volume enorm_ne_top noAtoms_volume circleMap_mem_sphere' circleAverage.integral_undef le_refl
circleAverage_smul 📖	mathematical	—	circleAverage Function.hasSMul Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	SMulCommClass.symm SMulCommClass.smul_comm mul_inv_rev intervalIntegral.integral_smul
circleAverage_sub 📖	mathematical	CircleIntegrable	circleAverage Pi.instSub Complex SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	circleAverage.eq_1 smul_sub intervalIntegral.integral_sub
circleAverage_sum 📖	mathematical	CircleIntegrable	circleAverage Finset.sum Pi.addCommMonoid Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	mul_inv_rev Finset.sum_apply intervalIntegral.integral_finset_sum Finset.sum_congr
circleAverage_zero 📖	mathematical	—	circleAverage Real instZero	—	circleAverage.eq_1 circleMap_zero_radius intervalIntegral.integral_const sub_zero IsScalarTower.left inv_mul_cancel₀ Nat.instAtLeastTwoHAddOfNat mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike pi_ne_zero one_smul
circleAverage_zero_one_congr_inv 📖	mathematical	—	circleAverage Complex Complex.instInv Complex.instZero Real instOne	—	Nat.instAtLeastTwoHAddOfNat circleMap_zero_inv inv_one intervalIntegral.integral_comp_neg periodic_circleMap neg_zero neg_add_cancel zero_add Function.Periodic.intervalIntegral_add_eq_of_pos two_pi_pos

Real.circleAverage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_undef 📖	mathematical	CircleIntegrable	Real.circleAverage NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	mul_inv_rev intervalIntegral.integral_undef smul_zero

---

← Back to Index