CircleAverage

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

Statistics

Metric	Count
Definitions circleAverage	1
Theorems circleAverage_comp_comm, circleAverage, eq_of_eqOn_Ioo, 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, continuous	31
Total	32

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	66 math math: circleAverage_map_add_const, DiffContOnCl.circleAverage_poissonKernel_smul', ValueDistribution.proximity_zero, circleAverage_sub, circleAverage_log_norm_sub_const₁, AnalyticOnNhd.circleAverage_log_norm, ContinuousOn.circleAverage, circleAverage_log_norm_sub_const_of_mem_closedBall, InnerProductSpace.HarmonicOnNhd.circleAverage_poissonKernel_smul, circleAverage_sum, HarmonicOnNhd.circleAverage_eq, DiffContOnCl.circleAverage, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, HarmonicContOnCl.circleAverage_eq, 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, DiffContOnCl.circleAverage_poissonKernel_smul, circleAverage_fun_smul, circleAverage_smul, DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul, DiffContOnCl.circleAverage_re_herglotzRieszKernel_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, InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul, circleAverage_sub_sub_inv_smul_of_differentiable_on, ValueDistribution.proximity_zero_of_complexValued, circleAverage_log_norm_sub_const_eq_posLog, circleAverage_log_norm_factorizedRational, InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul, circleAverage_of_differentiable_on_off_countable, circleAverage_log_norm_sub_const₂, circleAverage_eq_intervalAverage, InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul, 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.mul_assoc_rev 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.add_assoc_rev 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	Real instLE circleAverage normedAddCommGroup 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	Real instLE 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_neg_radius 📖	mathematical	—	circleAverage Real instNeg	—	circleMap_neg_radius Nat.instAtLeastTwoHAddOfNat circleAverage_eq_integral_add
circleAverage_nonneg_of_nonneg 📖	mathematical	Real instLE instZero	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

Real.ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage 📖	mathematical	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup setOf Real Set Set.instMembership Norm.norm Complex.instNorm Complex.instSub Real.instLE Real.instZero	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.circleAverage	—	continuousOn_iff_continuous_restrict Continuous.const_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' Real.noAtoms_volume Real.locallyFinite_volume circleMap_sub_center norm_circleMap_zero abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Subtype.coe_prop Continuous.comp Continuous.comp' Real.circleMap.continuous Continuous.prodMk continuous_subtype_val Continuous.fst continuous_id' Continuous.snd
eq_of_eqOn_Ioo 📖	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioc Real.instPreorder Real.instLT Set.EqOn Set.Ioo	—	—	Filter.Tendsto.mono_left Set.right_mem_Ioc nhdsWithin_le_iff mem_nhdsLT_iff_exists_Ioo_subset instOrderTopologyReal instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace nhdsLT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.Tendsto.congr' Filter.eventuallyEq_of_mem Ioo_mem_nhdsLT instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid tendsto_const_nhds

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

Real.circleMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	—	Continuous Real Complex instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField circleMap	—	Continuous.const_add instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Continuous.prodMk Complex.continuous_ofReal Continuous.fst continuous_id' Continuous.cexp Continuous.mul_const IsSemitopologicalSemiring.toSeparatelyContinuousMul Continuous.snd

---

← Back to Index