CircleIntegral

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

Statistics

Metric	Count
Definitions `CircleIntegrable`, `cauchyPowerSeries`, `circleIntegral`, `«term∮_InC(_,_),_»`,_»)	4
Theorems `abs`, `add`, `congr_codiscreteWithin`, `const_fun_smul`, `const_smul`, `finsum`, `fun_sum`, `neg`, `out`, `sum`, `circleIntegrable`, `circleIntegrable'`, `analyticOnNhd_circleMap`, `cauchyPowerSeries_apply`, `circleIntegrable_congr_codiscreteWithin`, `circleIntegrable_const`, `circleIntegrable_def`, `circleIntegrable_iff`, `circleIntegrable_sub_inv_iff`, `circleIntegrable_sub_zpow_iff`, `circleIntegrable_zero_radius`, `circleIntegral_congr_codiscreteWithin`, `integral_add`, `integral_congr`, `integral_const_mul`, `integral_eq_zero_of_hasDerivWithinAt`, `integral_eq_zero_of_hasDerivWithinAt'`, `integral_fun_sum`, `integral_radius_zero`, `integral_smul`, `integral_smul_const`, `integral_sub`, `integral_sub_center_inv`, `integral_sub_inv_of_mem_ball`, `integral_sub_inv_smul_sub_smul`, `integral_sub_zpow_of_ne`, `integral_sub_zpow_of_undef`, `integral_undef`, `norm_integral_le_of_norm_le_const`, `norm_integral_le_of_norm_le_const'`, `norm_integral_lt_of_norm_le_const_of_lt`, `norm_two_pi_i_inv_smul_integral_le_of_norm_le_const`, `circleIntegral_def_Icc`, `circleMap_neg_radius`, `circleMap_preimage_codiscrete`, `contDiff_circleMap`, `continuous_circleMap`, `continuous_circleMap_inv`, `deriv_circleMap`, `deriv_circleMap_eq_zero_iff`, `deriv_circleMap_ne_zero`, `differentiable_circleMap`, `hasDerivAt_circleMap`, `hasFPowerSeriesOn_cauchy_integral`, `hasSum_cauchyPowerSeries_integral`, `hasSum_two_pi_I_cauchyPowerSeries_integral`, `image_circleMap_Ioc`, `le_radius_cauchyPowerSeries`, `lipschitzWith_circleMap`, `measurable_circleMap`, `norm_cauchyPowerSeries_le`, `range_circleMap`, `sum_cauchyPowerSeries_eq_integral`	63
Total	67

CircleIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`CircleIntegrable` `Real` `Real.normedAddCommGroup`	`abs` `Pi.instLattice` `Complex` `Real.lattice` `Pi.addGroup` `Real.instAddGroup`	—	`IntervalIntegrable.abs`
`add` 📖	mathematical	`CircleIntegrable`	`Pi.instAdd` `Complex` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IntervalIntegrable.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`congr_codiscreteWithin` 📖	—	`Filter.EventuallyEq` `Complex` `Filter.codiscreteWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Metric.sphere` `abs` `Real` `Real.lattice` `Real.instAddGroup` `CircleIntegrable`	—	—	`intervalIntegrable_congr_codiscreteWithin` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.noAtoms_volume` `Filter.eventuallyEq_iff_exists_mem` `Filter.codiscreteWithin.mono` `circleMap_preimage_codiscrete`
`const_fun_smul` 📖	mathematical	`CircleIntegrable` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing`	`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` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`const_smul`
`const_smul` 📖	mathematical	`CircleIntegrable` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing`	`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` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`IntervalIntegrable.const_mul`
`finsum` 📖	mathematical	`CircleIntegrable`	`finsum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`finsum_eq_sum` `sum` `finsum_of_infinite_support` `circleIntegrable_const`
`fun_sum` 📖	mathematical	`CircleIntegrable`	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Finset.sum_apply` `sum`
`neg` 📖	mathematical	`CircleIntegrable`	`Pi.instNeg` `Complex` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IntervalIntegrable.neg`
`out` 📖	mathematical	`CircleIntegrable`	`IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex.addCommGroup` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `circleMap` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `deriv_circleMap` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.Integrable.mono'` `MeasureTheory.Integrable.const_mul` `MeasureTheory.Integrable.norm` `MeasureTheory.AEStronglyMeasurable.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `Complex.instProperSpace` `continuous_circleMap` `MeasureTheory.Integrable.aestronglyMeasurable` `MeasureTheory.Measure.instOuterMeasureClass` `norm_smul` `NormedSpace.toNormSMulClass` `Complex.norm_mul` `norm_circleMap_zero` `Complex.norm_I` `mul_one`
`sum` 📖	mathematical	`CircleIntegrable`	`Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`eq_1` `Finset.sum_apply` `IntervalIntegrable.sum` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleIntegrable` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere`	`CircleIntegrable`	—	`circleIntegrable'` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`circleIntegrable'` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`CircleIntegrable`	—	`Continuous.intervalIntegrable` `Real.locallyFinite_volume` `comp_continuous` `continuous_circleMap` `circleMap_mem_sphere'`

(root)

Definitions

Name	Category	Theorems
`CircleIntegrable` 📖	MathDef	15 math math: `circleIntegrable_congr_codiscreteWithin`, `circleIntegrable_iff`, `ContinuousOn.circleIntegrable`, `circleIntegrable_posLog_norm_meromorphicOn`, `circleIntegrable_log_norm_factorizedRational`, `circleIntegrable_log_norm_meromorphicOn`, `circleIntegrable_zero_radius`, `circleIntegrable_sub_zpow_iff`, `circleIntegrable_def`, `circleIntegrable_sub_inv_iff`, `ContinuousOn.circleIntegrable'`, `circleIntegrable_log_norm_sub_const`, `circleIntegrable_posLog_norm_meromorphicOn_of_nonneg`, `circleIntegrable_const`, `circleIntegrable_log_norm_meromorphicOn_of_nonneg`
`cauchyPowerSeries` 📖	CompOp	10 math math: `sum_cauchyPowerSeries_eq_integral`, `cauchyPowerSeries_apply`, `Differentiable.hasFPowerSeriesOnBall`, `norm_cauchyPowerSeries_le`, `hasSum_cauchyPowerSeries_integral`, `le_radius_cauchyPowerSeries`, `hasFPowerSeriesOn_cauchy_integral`, `DifferentiableOn.hasFPowerSeriesOnBall`, `Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable`, `DiffContOnCl.hasFPowerSeriesOnBall`
`circleIntegral` 📖	CompOp	53 math math: `Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable`, `circleIntegral_def_Icc`, `circleIntegral.integral_sub_inv_of_mem_ball`, `Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux`, `sum_cauchyPowerSeries_eq_integral`, `torusIntegral_succ`, `DifferentiableOn.circleIntegral_sub_inv_smul`, `circleIntegral.integral_fun_sum`, `Complex.integral_circleTransform`, `circleIntegral.integral_eq_zero_of_hasDerivWithinAt'`, `Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable`, `circleIntegral.integral_congr`, `circleIntegral.integral_sub_inv_smul_sub_smul`, `cauchyPowerSeries_apply`, `DiffContOnCl.circleIntegral_sub_inv_smul`, `DiffContOnCl.circleIntegral_eq_zero`, `Real.circleAverage_eq_circleIntegral`, `circleIntegral.integral_add`, `DiffContOnCl.deriv_eq_smul_circleIntegral`, `DifferentiableOn.deriv_eq_smul_circleIntegral`, `circleIntegral.integral_sub_zpow_of_undef`, `circleIntegral.norm_integral_le_of_norm_le_const`, `DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul`, `circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const`, `hasSum_cauchyPowerSeries_integral`, `Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable`, `circleIntegral.integral_radius_zero`, `hasSum_two_pi_I_cauchyPowerSeries_integral`, `circleIntegral.norm_integral_lt_of_norm_le_const_of_lt`, `circleIntegral.integral_sub`, `circleIntegral.integral_smul`, `Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable`, `circleIntegral.integral_undef`, `hasFPowerSeriesOn_cauchy_integral`, `Complex.circleIntegral_div_sub_of_differentiable_on_off_countable`, `Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable`, `torusIntegral_dim1`, `Complex.differentiable_on_off_countable_deriv_eq_smul_circleIntegral`, `circleIntegral.integral_sub_zpow_of_ne`, `circleIntegral.integral_smul_const`, `Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto`, `ModularFormClass.qExpansion_coeff_eq_circleIntegral`, `DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul`, `circleIntegral.circleIntegral_congr_codiscreteWithin`, `circleIntegral.norm_integral_le_of_norm_le_const'`, `Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable`, `circleIntegral.integral_eq_zero_of_hasDerivWithinAt`, `circleIntegral.integral_sub_center_inv`, `Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable`, `Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable`, `DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul`, `torusIntegral_succAbove`, `circleIntegral.integral_const_mul`
`«term∮_InC(_,_),_»` 📖,_» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticOnNhd_circleMap` 📖	mathematical	—	`AnalyticOnNhd` `Real` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `circleMap` `Set.univ`	—	`AnalyticAt.add` `analyticAt_const` `AnalyticAt.mul` `AnalyticAt.comp` `AnalyticAt.restrictScalars` `IsScalarTower.right` `analyticAt_cexp` `ContinuousLinearMap.analyticAt`
`cauchyPowerSeries_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMultilinearMap` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instModuleSelf` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `cauchyPowerSeries` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Complex.instInv` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `circleIntegral` `Monoid.toNatPow` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instSub`	—	`Nat.instAtLeastTwoHAddOfNat` `Fin.prod_const` `div_eq_mul_inv` `mul_pow` `SemigroupAction.mul_smul` `circleIntegral.integral_smul` `smulCommClass_self` `SMulCommClass.smul_comm`
`circleIntegrable_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` `Real.lattice` `Real.instAddGroup`	`CircleIntegrable`	—	`CircleIntegrable.congr_codiscreteWithin` `Filter.EventuallyEq.symm`
`circleIntegrable_const` 📖	mathematical	—	`CircleIntegrable`	—	`intervalIntegrable_const` `Real.locallyFinite_volume` `enorm_ne_top`
`circleIntegrable_def` 📖	mathematical	—	`CircleIntegrable` `IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `circleMap` `MeasureTheory.MeasureSpace.volume` `Real` `Real.measureSpace` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	—
`circleIntegrable_iff` 📖	mathematical	—	`CircleIntegrable` `IntervalIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex.addCommGroup` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `circleMap` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `circleMap_zero_radius` `deriv_const'` `zero_smul` `Real.locallyFinite_volume` `enorm_zero` `CircleIntegrable.out` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.Integrable.mono'` `MeasureTheory.Integrable.const_mul` `MeasureTheory.Integrable.norm` `deriv_circleMap` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `inv_smul_smul₀` `MeasureTheory.AEStronglyMeasurable.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `AEMeasurable.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Complex.borelSpace` `secondCountable_of_proper` `Complex.instProperSpace` `AEMeasurable.inv` `ContinuousInv₀.measurableInv` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `MeasureTheory.AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `Continuous.aestronglyMeasurable` `Real.borelSpace` `secondCountableTopologyEither_of_right` `continuous_circleMap` `MeasureTheory.Integrable.aestronglyMeasurable` `MeasureTheory.Measure.instOuterMeasureClass` `norm_smul` `NormedSpace.toNormSMulClass` `Complex.norm_mul` `norm_circleMap_zero` `Complex.norm_I` `mul_one` `inv_mul_cancel_left₀` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`circleIntegrable_sub_inv_iff` 📖	mathematical	—	`CircleIntegrable` `Complex` `Complex.instNormedAddCommGroup` `Complex.instInv` `Complex.instSub` `Real` `Real.instZero` `Set` `Set.instMembership` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup`	—	—
`circleIntegrable_sub_zpow_iff` 📖	mathematical	—	`CircleIntegrable` `Complex` `Complex.instNormedAddCommGroup` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `Complex.instSub` `Real` `Real.instZero` `Set` `Set.instMembership` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Nat.instAtLeastTwoHAddOfNat` `circleIntegrable_iff` `deriv_circleMap` `image_circleMap_Ioc` `Set.Icc_subset_uIcc` `Set.Ioc_subset_Icc_self` `not_intervalIntegrable_of_sub_inv_isBigO_punctured` `Filter.mp_mem` `mem_nhdsWithin_of_mem_nhds` `Metric.ball_mem_nhds` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `self_mem_nhdsWithin` `Filter.univ_mem'` `dist_zero_right` `Filter.Tendsto.eventually` `HasDerivAt.tendsto_nhdsNE` `DifferentiableAt.hasDerivAt` `differentiable_circleMap` `deriv_circleMap_ne_zero` `Asymptotics.IsBigO.trans` `Asymptotics.IsBigO.inv_rev` `Asymptotics.IsBigO.mono` `HasDerivAtFilter.isBigO_sub` `hasDerivAt_circleMap` `inf_le_left` `Filter.Eventually.mono` `Asymptotics.IsBigO.of_bound` `zpow_neg_one` `StrictAnti.le_iff_ge` `zpow_right_strictAnti₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_inv` `norm_mul` `NormedDivisionRing.toNormMulClass` `Complex.norm_I` `mul_one` `norm_circleMap_zero` `norm_zpow` `inv_mul_cancel_left₀` `Iff.not` `abs_eq_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.ne` `Real.two_pi_pos` `circleIntegrable_zero_radius` `ContinuousOn.circleIntegrable'` `ContinuousOn.zpow₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousOn_id` `continuousOn_const` `sub_ne_zero`
`circleIntegrable_zero_radius` 📖	mathematical	—	`CircleIntegrable` `Real` `Real.instZero`	—	`circleMap_zero_radius` `Real.locallyFinite_volume`
`circleIntegral_def_Icc` 📖	mathematical	—	`circleIntegral` `MeasureTheory.integral` `Real` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `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` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex.addCommGroup` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `circleMap`	—	`Nat.instAtLeastTwoHAddOfNat` `circleIntegral.eq_1` `intervalIntegral.integral_of_le` `LT.lt.le` `Real.two_pi_pos` `MeasureTheory.Measure.restrict_congr_set` `MeasureTheory.Ioc_ae_eq_Icc` `Real.noAtoms_volume`
`circleMap_neg_radius` 📖	mathematical	—	`circleMap` `Real` `Real.instNeg` `Real.instAdd` `Real.pi`	—	`Complex.ofReal_neg` `neg_mul` `Complex.ofReal_add` `add_mul` `Distrib.rightDistribClass` `Complex.exp_add` `Complex.exp_pi_mul_I` `mul_neg` `mul_one`
`circleMap_preimage_codiscrete` 📖	mathematical	—	`Filter` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.map` `Real` `circleMap` `Filter.codiscrete` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Filter.codiscreteWithin` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Metric.sphere` `abs` `Real.lattice` `Real.instAddGroup`	—	`AnalyticOnNhd.preimage_mem_codiscreteWithin` `analyticOnNhd_circleMap` `Filter.eventuallyConst_iff_exists_eventuallyEq` `Filter.EventuallyEq.eq_of_nhds` `Filter.EventuallyEq.deriv` `deriv_circleMap` `deriv_const'` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Set.image_univ` `range_circleMap`
`contDiff_circleMap` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `circleMap`	—	`AnalyticOnNhd.contDiff` `analyticOnNhd_circleMap`
`continuous_circleMap` 📖	mathematical	—	`Continuous` `Real` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `circleMap`	—	`Differentiable.continuous` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `differentiable_circleMap`
`continuous_circleMap_inv` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Complex.instInv` `Complex.instSub` `circleMap`	—	`circleMap_ne_mem_ball` `Continuous.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_circleMap` `continuous_const`
`deriv_circleMap` 📖	mathematical	—	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex` `Complex.addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `circleMap` `Complex.instMul` `Complex.instZero` `Complex.I`	—	`HasDerivAt.deriv` `hasDerivAt_circleMap`
`deriv_circleMap_eq_zero_iff` 📖	mathematical	—	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex` `Complex.addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `circleMap` `Complex.instZero` `Real.instZero`	—	`deriv_circleMap` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`deriv_circleMap_ne_zero` 📖	—	—	—	—	`deriv_circleMap_eq_zero_iff`
`differentiable_circleMap` 📖	mathematical	—	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Complex` `Complex.addCommGroup` `NormedField.toNormedCommRing` `Complex.instNormedField` `instInnerProductSpaceRealComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `circleMap`	—	`HasDerivAt.differentiableAt` `hasDerivAt_circleMap`
`hasDerivAt_circleMap` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex` `Complex.addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `Complex.instZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `circleMap` `Complex.instMul` `Complex.I`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivAt.congr_simp` `zero_add` `mul_assoc` `one_mul` `HasDerivAt.const_add` `HasDerivAt.const_mul` `HasDerivAt.cexp` `HasDerivAt.mul_const` `ContinuousLinearMap.hasDerivAt`
`hasFPowerSeriesOn_cauchy_integral` 📖	mathematical	`CircleIntegrable` `NNReal.toReal` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`HasFPowerSeriesOnBall` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `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` `Real.pi` `Complex.I` `circleIntegral` `Complex.instSub` `cauchyPowerSeries` `ENNReal.ofNNReal`	—	`Nat.instAtLeastTwoHAddOfNat` `le_radius_cauchyPowerSeries` `ENNReal.coe_pos` `hasSum_cauchyPowerSeries_integral` `Metric.eball_coe` `dist_zero_right`
`hasSum_cauchyPowerSeries_integral` 📖	mathematical	`CircleIntegrable` `Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `Complex.instSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instNormedAddCommGroup` `Complex.instModuleSelf` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `cauchyPowerSeries` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Complex.instInv` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `circleIntegral` `Complex.instSub` `Complex.instAdd` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `cauchyPowerSeries_apply` `HasSum.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `hasSum_two_pi_I_cauchyPowerSeries_integral`
`hasSum_two_pi_I_cauchyPowerSeries_integral` 📖	mathematical	`CircleIntegrable` `Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `circleIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `Complex.instNormedField` `Monoid.toNatPow` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instSub` `Complex.instInv` `Complex.instAdd` `SummationFilter.unconditional`	—	`LE.le.trans_lt` `norm_nonneg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.le` `div_lt_one` `intervalIntegral.hasSum_integral_of_dominated_convergence` `instCountableNat` `deriv_circleMap` `MeasureTheory.AEStronglyMeasurable.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountable_of_proper` `Complex.instProperSpace` `BorelSpace.opensMeasurable` `Complex.borelSpace` `Measurable.mul_const` `ContinuousMul.measurableMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `measurable_circleMap` `Measurable.pow_const` `Monoid.measurablePow` `ContinuousMul.measurableMul₂` `Measurable.const_div` `measurableDiv_of_mul_inv` `ContinuousInv₀.measurableInv` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `Measurable.sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Measurable.inv` `IntervalIntegrable.def'` `MeasureTheory.Measure.instOuterMeasureClass` `circleMap_sub_center` `norm_smul` `NormedSpace.toNormSMulClass` `Complex.norm_mul` `norm_circleMap_zero` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Complex.norm_I` `mul_one` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Complex.norm_div` `norm_inv` `mul_left_comm` `inv_mul_cancel_left₀` `LT.lt.ne'` `mul_comm` `Filter.Eventually.of_forall` `Summable.mul_left` `instIsTopologicalRingReal` `summable_geometric_of_lt_one` `tsum_mul_left` `TopologicalSpace.t2Space_of_metrizableSpace` `tsum_geometric_of_lt_one` `IntervalIntegrable.mul_continuousOn` `IntervalIntegrable.norm` `continuousOn_const` `HasSum.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `smul_smul` `HasSum.smul_const` `sub_mul` `one_mul` `div_mul_cancel₀` `circleMap_ne_center` `HasSum.mul_right` `hasSum_geometric_of_norm_lt_one`
`image_circleMap_Ioc` 📖	mathematical	—	`Set.image` `Real` `Complex` `circleMap` `Set.Ioc` `Real.instPreorder` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `range_circleMap` `Function.Periodic.image_Ioc` `Real.instIsOrderedAddMonoid` `Real.instArchimedean` `periodic_circleMap` `Real.two_pi_pos` `zero_add`
`le_radius_cauchyPowerSeries` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `FormalMultilinearSeries.radius` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `cauchyPowerSeries` `NNReal.toReal`	—	`FormalMultilinearSeries.le_radius_of_bound` `Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_cauchyPowerSeries_le` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `NNReal.coe_nonneg` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `eq_or_ne` `Nat.cast_zero` `MulZeroClass.mul_zero` `mul_nonneg` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.le` `Real.two_pi_pos` `intervalIntegral.integral_nonneg` `norm_nonneg` `inv_pow` `inv_mul_cancel_right₀` `le_refl`
`lipschitzWith_circleMap` 📖	mathematical	—	`LipschitzWith` `Real` `Complex` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NormedField.toMetricSpace` `Complex.instNormedField` `DFunLike.coe` `MonoidWithZeroHom` `NNReal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Real.semiring` `instSemiringNNReal` `MonoidWithZeroHom.funLike` `Real.nnabs` `circleMap`	—	`lipschitzWith_of_nnnorm_deriv_le` `differentiable_circleMap` `NNReal.coe_le_coe` `deriv_circleMap` `nnnorm_mul` `NormedDivisionRing.toNormMulClass` `Complex.nnnorm_I` `mul_one` `norm_circleMap_zero`
`measurable_circleMap` 📖	mathematical	—	`Measurable` `Real` `Complex` `Real.measurableSpace` `Complex.measurableSpace` `circleMap`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `Complex.borelSpace` `continuous_circleMap`
`norm_cauchyPowerSeries_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousMultilinearMap` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instModuleSelf` `NormedSpace.toModule` `ContinuousMultilinearMap.hasOpNorm'` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace` `Fin.fintype` `cauchyPowerSeries` `Real.instMul` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `intervalIntegral` `Real.normedAddCommGroup` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `NormedAddCommGroup.toNorm` `circleMap` `Real.instZero` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Monoid.toNatPow` `Real.instMonoid` `abs` `Real.lattice` `Real.instAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `ContinuousMultilinearMap.mkPiRing.congr_simp` `mul_inv_rev` `Complex.inv_I` `neg_mul` `inv_pow` `neg_smul` `ContinuousMultilinearMap.norm_mkPiRing` `norm_neg` `norm_smul` `NormedSpace.toNormSMulClass` `Complex.norm_mul` `Complex.norm_I` `norm_inv` `Complex.norm_real` `Complex.norm_ofNat` `one_mul` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `Real.instIsOrderedAddMonoid` `LT.lt.le` `Real.pi_pos` `RCLike.charZero_rclike` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `intervalIntegral.norm_integral_le_integral_norm` `Real.two_pi_pos` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instNontrivial` `deriv_circleMap` `circleMap_sub_center` `norm_circleMap_zero` `mul_one` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `mul_left_comm` `intervalIntegral.integral_const_mul` `eq_or_ne` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `inv_zero` `pow_zero` `circleMap_zero_radius` `intervalIntegral.integral_const` `Real.instCompleteSpace` `sub_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `inv_mul_cancel_left₀` `NormMulClass.toNoZeroDivisors` `zero_pow` `mul_inv_cancel_left₀` `abs_eq_zero` `covariant_swap_add_of_covariant_add` `mul_assoc` `mul_comm` `le_refl`
`range_circleMap` 📖	mathematical	—	`Set.range` `Complex` `Real` `circleMap` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup`	—	`Set.image_congr` `Complex.range_exp_mul_I` `smul_sphere` `Complex.instNontrivial` `zero_le_one` `Real.instZeroLEOneClass` `smul_zero` `mul_one` `Metric.vadd_sphere` `NormedAddGroup.to_isIsometricVAdd_left` `add_zero`
`sum_cauchyPowerSeries_eq_integral` 📖	mathematical	`CircleIntegrable` `Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm`	`FormalMultilinearSeries.sum` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instModuleSelf` `NormedSpace.toModule` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsBoundedSMul.toUniformContinuousConstSMul` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `cauchyPowerSeries` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Complex.instInv` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `circleIntegral` `Complex.instSub` `Complex.instAdd`	—	`HasSum.tsum_eq` `Nat.instAtLeastTwoHAddOfNat` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_cauchyPowerSeries_integral`

circleIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleIntegral_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` `Real.lattice` `Real.instAddGroup`	`circleIntegral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	—	`intervalIntegral.integral_congr_ae_restrict` `ae_restrict_le_codiscreteWithin` `instSecondCountableTopologyReal` `Real.noAtoms_volume` `measurableSet_uIoc` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `deriv_circleMap` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Filter.codiscreteWithin.mono` `circleMap_preimage_codiscrete`
`integral_add` 📖	mathematical	`CircleIntegrable`	`circleIntegral` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `smul_add` `intervalIntegral.integral_add` `CircleIntegrable.out`
`integral_congr` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Set.EqOn` `Complex` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`circleIntegral`	—	`intervalIntegral.integral_congr` `circleMap_mem_sphere`
`integral_const_mul` 📖	mathematical	—	`circleIntegral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Complex.instMul`	—	`integral_smul` `Algebra.to_smulCommClass`
`integral_eq_zero_of_hasDerivWithinAt` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `HasDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Metric.sphere`	`circleIntegral`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `integral_eq_zero_of_hasDerivWithinAt'` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`integral_eq_zero_of_hasDerivWithinAt'` 📖	mathematical	`HasDerivWithinAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Metric.sphere` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`circleIntegral`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Nat.instAtLeastTwoHAddOfNat` `sub_eq_zero` `Function.Periodic.eq` `Function.Periodic.comp` `periodic_circleMap` `intervalIntegral.integral_eq_sub_of_hasDerivAt` `HasDerivWithinAt.scomp_hasDerivAt` `IsScalarTower.complexToReal` `IsScalarTower.left` `circleMap_mem_sphere'` `DifferentiableAt.hasDerivAt` `differentiable_circleMap` `CircleIntegrable.out` `integral_undef`
`integral_fun_sum` 📖	mathematical	`CircleIntegrable`	`circleIntegral` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.smul_sum` `intervalIntegral.integral_finset_sum` `CircleIntegrable.out` `Finset.sum_congr`
`integral_radius_zero` 📖	mathematical	—	`circleIntegral` `Real` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`circleMap_zero_radius` `deriv_const'` `zero_smul` `intervalIntegral.integral_zero`
`integral_smul` 📖	mathematical	—	`circleIntegral` `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` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`SMulCommClass.smul_comm` `intervalIntegral.integral_smul` `NormedSpace.toNormSMulClass` `IsScalarTower.to_smulCommClass` `Real.isScalarTower` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`integral_smul_const` 📖	mathematical	—	`circleIntegral` `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` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `RCLike.innerProductSpace`	—	`IsScalarTower.left` `intervalIntegral.integral_smul_const`
`integral_sub` 📖	mathematical	`CircleIntegrable`	`circleIntegral` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `smul_sub` `intervalIntegral.integral_sub` `CircleIntegrable.out`
`integral_sub_center_inv` 📖	mathematical	—	`circleIntegral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Complex.instInv` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`Nat.instAtLeastTwoHAddOfNat` `deriv_circleMap` `circleMap_sub_center` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `circleMap_ne_center` `intervalIntegral.integral_const` `Complex.instCompleteSpace` `sub_zero` `Complex.ofReal_mul`
`integral_sub_inv_of_mem_ball` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`circleIntegral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Complex.instInv` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`LE.le.trans_lt` `dist_nonneg` `Nat.instAtLeastTwoHAddOfNat` `integral_sub_zpow_of_ne` `pow_zero` `one_mul` `integral_sub_center_inv` `LT.lt.ne'` `hasSum_single` `div_eq_mul_inv` `mul_pow` `mul_assoc` `integral_const_mul` `integral_congr` `LT.lt.le` `pow_succ` `zpow_natCast` `inv_zpow` `zpow_neg` `neg_add` `sub_eq_add_neg` `MulZeroClass.mul_zero` `SummationFilter.instLeAtTopUnconditional` `ContinuousOn.circleIntegrable'` `continuousOn_const` `HasSum.unique` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional` `mul_one` `add_sub_cancel` `hasSum_two_pi_I_cauchyPowerSeries_integral`
`integral_sub_inv_smul_sub_smul` 📖	mathematical	—	`circleIntegral` `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` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Complex.instInv` `Complex.instSub`	—	`eq_or_ne` `integral_radius_zero` `Set.Countable.preimage_circleMap` `Set.countable_singleton` `intervalIntegral.integral_congr_ae` `Filter.Eventually.mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.Countable.ae_notMem` `Real.noAtoms_volume` `inv_smul_smul₀` `sub_ne_zero`
`integral_sub_zpow_of_ne` 📖	mathematical	—	`circleIntegral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `Complex.instSub` `Complex.instZero`	—	`integral_sub_zpow_of_undef` `LT.lt.trans` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `eq_neg_iff_add_eq_zero` `Int.cast_one` `Int.cast_neg` `Complex.instCharZero` `Int.cast_add` `add_sub_cancel_right` `mul_one` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `HasDerivAt.div_const` `HasDerivAt.comp` `hasDerivAt_zpow` `sub_ne_zero` `neg_le_iff_add_nonneg` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `HasDerivAt.sub_const` `hasDerivAt_id` `integral_eq_zero_of_hasDerivWithinAt'` `Complex.instCompleteSpace` `HasDerivAt.hasDerivWithinAt` `Mathlib.Tactic.Push.not_and_eq` `ne_or_eq`
`integral_sub_zpow_of_undef` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`circleIntegral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `Complex.instSub` `Complex.instZero`	—	`eq_or_ne` `integral_radius_zero` `integral_undef`
`integral_undef` 📖	mathematical	`CircleIntegrable`	`circleIntegral` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`intervalIntegral.integral_undef` `Nat.instAtLeastTwoHAddOfNat` `circleIntegrable_iff`
`norm_integral_le_of_norm_le_const` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedAddCommGroup.toNorm`	`circleIntegral` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `norm_integral_le_of_norm_le_const'`
`norm_integral_le_of_norm_le_const'` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	`circleIntegral` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `abs` `Real.lattice` `Real.instAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `intervalIntegral.norm_integral_le_of_norm_le_const` `deriv_circleMap` `norm_smul` `NormedSpace.toNormSMulClass` `Complex.norm_mul` `norm_circleMap_zero` `Complex.norm_I` `mul_one` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `circleMap_mem_sphere'` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `sub_zero` `abs_of_pos` `Real.two_pi_pos` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`norm_integral_lt_of_norm_le_const_of_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Set` `Set.instMembership`	`circleIntegral` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `image_circleMap_Ioc` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `intervalIntegral.norm_integral_le_integral_norm` `LT.lt.le` `Real.two_pi_pos` `deriv_circleMap` `norm_smul` `NormedSpace.toNormSMulClass` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_circleMap_zero` `Complex.norm_I` `mul_one` `intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt` `ContinuousOn.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuousOn_const` `ContinuousOn.norm` `ContinuousOn.comp` `Continuous.continuousOn` `continuous_circleMap` `circleMap_mem_sphere` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Set.Ioc_subset_Icc_self` `mul_lt_mul_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `intervalIntegral.integral_const_mul` `intervalIntegral.integral_const` `Real.instCompleteSpace` `sub_zero` `mul_assoc` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.mul_one`
`norm_two_pi_i_inv_smul_integral_le_of_norm_le_const` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedAddCommGroup.toNorm`	`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` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Complex.instInv` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `circleIntegral` `Real.instMul`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_inv_rev` `Complex.inv_I` `neg_mul` `norm_neg` `Complex.norm_mul` `Complex.norm_I` `norm_inv` `Complex.norm_real` `Complex.norm_ofNat` `one_mul` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `Real.instIsOrderedAddMonoid` `LT.lt.le` `Real.pi_pos` `RCLike.charZero_rclike` `norm_smul` `NormedSpace.toNormSMulClass` `div_eq_inv_mul` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Real.two_pi_pos` `mul_comm` `mul_assoc` `norm_integral_le_of_norm_le_const`

---

← Back to Index