Circle

📁 Source: Mathlib/Analysis/Complex/Circle.lean

Statistics

Metric	Count
Definitions coeHom, exp, expHom, instCoeOut, instCommGroup, instDistribMulAction, instMetricSpace, instMulAction, instSMul, instUniformSpace, ofConjDivSelf, toUnits, «term𝐞», fourierChar, probChar, instTopologicalSpaceCircle	16
Theorems coeHom_apply, coe_div, coe_eq_one, coe_exp, coe_inj, coe_injective, coe_inv, coe_inv_eq_conj, coe_mul, coe_ne_zero, coe_one, coe_pow, coe_zpow, expHom_apply, exp_add, exp_intCast_mul, exp_natCast_mul, exp_neg, exp_nsmul, exp_pi_ne_one, exp_sub, exp_zero, exp_zsmul, ext, ext_iff, instCompactSpace, instContinuousSMul, instIsScalarTower, instIsTopologicalGroup, instIsUniformGroup, instSMulCommClass_left, instSMulCommClass_right, normSq_coe, norm_coe, norm_smul, ofConjDivSelf_coe, smul_def, starRingEnd_addChar, star_addChar, toUnits_apply, continuous_fourierChar, continuous_probChar, fourierChar_apply, fourierChar_apply', fourierChar_ne_one, probChar_apply, probChar_apply', probChar_ne_one	48
Total	64

Circle

Definitions

Name	Category	Theorems
coeHom 📖	CompOp	1 math math: coeHom_apply
exp 📖	CompOp	38 math math: periodic_exp, exp_arg, AddCircle.homeomorphCircle'_apply_mk, exp_natCast_mul, isAddQuotientCoveringMap_exp, exp_eq_exp, exp_two_pi_mul_int, AddCircle.scaled_exp_map_periodic, exp_two_pi, exp_sub, exp_neg, exp_inj, exp_add_two_pi, invOn_arg_exp, Real.Angle.toCircle_coe, exp_add, leftInverse_exp_arg, argEquiv_symm_apply, AddCircle.toCircle_apply_mk, Real.probChar_apply', exp_zero, exp_int_mul_two_pi, surjOn_exp_neg_pi_pi, exp_intCast_mul, Real.fourierChar_apply', isLocalHomeomorph_circleExp, expHom_apply, arg_exp, coe_exp, exp_zsmul, exp_eq_one, isCoveringMap_exp, AddChar.zmod_intCast, exp_sub_two_pi, argPartialEquiv_symm_apply, ZMod.toCircle_eq_circleExp, exp_nsmul, contMDiff_circleExp
expHom 📖	CompOp	1 math math: expHom_apply
instCoeOut 📖	CompOp	—
instCommGroup 📖	CompOp	108 math math: Real.hasFDerivAt_fourierChar_neg_bilinear_left, Complex.UnitDisc.instIsScalarTower_circle, Real.fourierIntegral_eq, Real.Angle.toCircle_add, Real.fderiv_fourierChar_neg_bilinear_right_apply, exp_natCast_mul, AddCircle.toCircle_add, Complex.UnitDisc.instSMulCommClass_closedBall_circle, rotation_injective, starRingEnd_addChar, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, rotation_apply, toMatrix_rotation, exp_two_pi_mul_int, Complex.UnitDisc.coe_smul_circle, Complex.UnitDisc.instIsScalarTower_circle_circle, Complex.UnitDisc.instSMulCommClass_circle_left, AddChar.zmod_add, tendsto_integral_exp_smul_cocompact, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, Real.fourier_real_eq, exp_two_pi, Real.fourierIntegral_convergent_iff', Real.Angle.toCircle_zero, exp_sub, isQuotientCoveringMap_zpow, Real.continuous_probChar, exp_neg, instIsTopologicalGroup, coe_inv_eq_conj, coe_mul, coe_pow, fourierIntegral_eq_half_sub_half_period_translate, linear_isometry_complex, star_addChar, rotationOf_rotation, bijective_rootsOfUnityAddChar, Real.fourier_eq, AddCircle.toCircle_zero, exp_add, tendsto_integral_exp_smul_cocompact_of_inner_product, AddCircle.toCircle_zsmul, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, instIsUniformGroup, isQuotientCoveringMap_npow, rotation_trans, instHasEnoughRootsOfUnityCircle, Real.probChar_apply', exp_zero, Complex.UnitDisc.instSMulCommClass_circle_right, Real.fourierIntegral_convergent_iff, Real.hasDerivAt_fourierChar, linearEquiv_det_rotation, coe_eq_one, Real.fourierChar_apply, Real.fourier_bilin_convolution_eq_integral, exp_int_mul_two_pi, Real.tendsto_integral_exp_smul_cocompact, fourierIntegral_half_period_translate, coe_inv, exp_intCast_mul, Real.Angle.toCircle_neg, Real.fourierChar_apply', Real.differentiable_fourierChar, Real.continuous_fourierChar, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, ZMod.toCircle_intCast, ZMod.toCircle_natCast, Real.deriv_fourierChar, Complex.UnitDisc.instSMulCommClass_circle_closedBall, Real.differentiable_fourierChar_neg_bilinear_right, ZMod.injective_toCircle, coeHom_apply, rootsOfUnityCircleEquiv_apply, VectorFourier.fourierIntegral_comp_add_right, AddChar.zmod_zero, tendsto_integral_exp_inner_smul_cocompact, det_rotation, Fourier.fourierIntegral_def, expHom_apply, rotation_symm, Real.hasFDerivAt_fourierChar_neg_bilinear_right, ZMod.toCircle_apply, Real.differentiable_fourierChar_neg_bilinear_left, exp_zsmul, exp_eq_one, toUnits_apply, Real.fourierInv_eq, Real.probChar_apply, AddChar.zmod_intCast, AddCircle.toCircle_nsmul, coe_zpow, VectorFourier.hasFDerivAt_fourierChar_smul, Real.fourierIntegral_real_eq, AddChar.zmodAddEquiv_apply, coe_div, coe_one, AddChar.zmod_injective, Real.fourierIntegralInv_eq, Real.fderiv_fourierChar_neg_bilinear_left_apply, AddCircle.toCircle_neg, Fourier.fourierIntegral_comp_add_right, ZMod.rootsOfUnityAddChar_val, ZMod.toCircle_eq_circleExp, exp_nsmul, Complex.UnitDisc.coe_circle_smul, ZMod.stdAddChar_apply, MeasureTheory.charFun_eq_integral_probChar
instDistribMulAction 📖	CompOp	—
instMetricSpace 📖	CompOp	—
instMulAction 📖	CompOp	—
instSMul 📖	CompOp	28 math math: Real.fourierIntegral_eq, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, instIsScalarTower, tendsto_integral_exp_smul_cocompact, Real.fourier_real_eq, smul_def, Real.fourierIntegral_convergent_iff', instSMulCommClass_left, VectorFourier.fourierIntegral_convergent_iff, fourierIntegral_eq_half_sub_half_period_translate, instSMulCommClass_right, instContinuousSMul, VectorFourier.integral_fourierIntegral_swap, Real.fourier_eq, tendsto_integral_exp_smul_cocompact_of_inner_product, Real.fourierIntegral_convergent_iff, Real.fourier_bilin_convolution_eq_integral, Real.tendsto_integral_exp_smul_cocompact, fourierIntegral_half_period_translate, VectorFourier.fourierIntegral_comp_add_right, tendsto_integral_exp_inner_smul_cocompact, Fourier.fourierIntegral_def, Real.fourierInv_eq, VectorFourier.hasFDerivAt_fourierChar_smul, Real.fourierIntegral_real_eq, Real.fourierIntegralInv_eq, Fourier.fourierIntegral_comp_add_right, norm_smul
instUniformSpace 📖	CompOp	1 math math: instIsUniformGroup
ofConjDivSelf 📖	CompOp	1 math math: ofConjDivSelf_coe
toUnits 📖	CompOp	1 math math: toUnits_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Circle Complex MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring MonoidHom.instFunLike coeHom Submonoid Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere	—	—
coe_div 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Circle DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup instCommGroup Complex.instDivInvMonoid	—	—
coe_eq_one 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Complex.instOne Circle InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	coe_one
coe_exp 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp Complex.exp Complex.instMul Complex.ofReal Complex.I	—	—
coe_inj 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere	—	coe_injective
coe_injective 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere	—	ext
coe_inv 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Circle InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup Complex.instInv	—	—
coe_inv_eq_conj 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Circle InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup DFunLike.coe RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	coe_inv Complex.inv_def normSq_coe inv_one Complex.ofReal_one mul_one
coe_mul 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Circle MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup Complex.instMul	—	—
coe_ne_zero 📖	—	—	—	—	ne_zero_of_mem_unit_sphere
coe_one 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Circle InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup Complex.instOne	—	—
coe_pow 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Circle Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring	—	—
coe_zpow 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Circle DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup instCommGroup Complex.instDivInvMonoid	—	—
expHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Real Additive Circle AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup AddMonoidHom.instFunLike expHom Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp	—	—
exp_add 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp Real.instAdd MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	Complex.ofReal_add add_mul Distrib.rightDistribClass Complex.exp_add
exp_intCast_mul 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp Real.instMul Real.instIntCast DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	zsmul_eq_mul exp_zsmul
exp_natCast_mul 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp Real.instMul Real.instNatCast Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	nsmul_eq_mul exp_nsmul
exp_neg 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp Real.instNeg InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	AddMonoidHom.map_neg
exp_nsmul 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp AddMonoid.toNatSMul Real.instAddMonoid Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	AddMonoidHom.map_nsmul
exp_pi_ne_one 📖	—	—	—	—	Mathlib.Meta.NormNum.isInt_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Complex.exp_pi_mul_I coe_exp
exp_sub 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp Real.instSub DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	AddMonoidHom.map_sub
exp_zero 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp Real.instZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	coe_exp Complex.ofReal_zero MulZeroClass.zero_mul Complex.exp_zero coe_one
exp_zsmul 📖	mathematical	—	DFunLike.coe ContinuousMap Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike exp SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Real.instAddGroup DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	AddMonoidHom.map_zsmul
ext 📖	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere	—	—	—
ext_iff 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere	—	ext
instCompactSpace 📖	mathematical	—	CompactSpace Circle instTopologicalSpaceCircle	—	Metric.sphere.compactSpace Complex.instProperSpace
instContinuousSMul 📖	mathematical	—	ContinuousSMul Circle instSMul SemigroupAction.toSMul Complex Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring MulAction.toSemigroupAction instTopologicalSpaceCircle	—	Submonoid.continuousSMul
instIsScalarTower 📖	mathematical	—	IsScalarTower Circle instSMul	—	Submonoid.isScalarTower
instIsTopologicalGroup 📖	mathematical	—	IsTopologicalGroup Circle instTopologicalSpaceCircle CommGroup.toGroup instCommGroup	—	Metric.sphere.instIsTopologicalGroup
instIsUniformGroup 📖	mathematical	—	IsUniformGroup Circle instUniformSpace CommGroup.toGroup instCommGroup	—	IsUniformGroup.of_compactSpace IsTopologicalGroup.to_continuousDiv instIsTopologicalGroup instCompactSpace
instSMulCommClass_left 📖	mathematical	—	SMulCommClass Circle instSMul	—	Submonoid.smulCommClass_left
instSMulCommClass_right 📖	mathematical	—	SMulCommClass Circle instSMul	—	Submonoid.smulCommClass_right
normSq_coe 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Complex Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq Submonoid MulZeroOneClass.toMulOneClass Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Real.instOne	—	Complex.normSq_eq_norm_sq norm_eq_of_mem_sphere one_pow
norm_coe 📖	mathematical	—	Norm.norm Complex Complex.instNorm Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere Real Real.instOne	—	mem_sphere_zero_iff_norm
norm_smul 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm Circle instSMul SMulZeroClass.toSMul Complex AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex.instNormedField	—	Submonoid.smul_def norm_smul NormedSpace.toNormSMulClass norm_eq_of_mem_sphere one_mul
ofConjDivSelf_coe 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere ofConjDivSelf DivInvMonoid.toDiv Complex.instDivInvMonoid DFunLike.coe RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	—
smul_def 📖	mathematical	—	Circle instSMul Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere	—	—
starRingEnd_addChar 📖	mathematical	—	DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere AddChar Real Real.instAddMonoid Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup AddChar.instFunLike Real.instNeg	—	star_addChar
star_addChar 📖	mathematical	—	Star.star Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instNormedField StarRing.toStarAddMonoid Complex.instStarRing Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere DFunLike.coe AddChar Real Real.instAddMonoid Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup AddChar.instFunLike Real.instNeg	—	coe_inv_eq_conj Subtype.coe_eta AddChar.map_neg_eq_inv
toUnits_apply 📖	mathematical	—	DFunLike.coe MonoidHom Circle Units Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup Units.instMulOneClass MonoidHom.instFunLike toUnits DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield Complex.instField Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere coe_ne_zero	—	—

FourierTransform

Definitions

Name	Category	Theorems
«term𝐞» 📖	CompOp	—

Real

Definitions

Name	Category	Theorems
fourierChar 📖	CompOp	46 math math: MeasureTheory.charFun_eq_fourierIntegral', hasFDerivAt_fourierChar_neg_bilinear_left, fourierIntegral_eq, fderiv_fourierChar_neg_bilinear_right_apply, vector_fourierIntegral_eq_integral_exp_smul, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, VectorFourier.hasFDerivAt_fourierIntegral, VectorFourier.fourierIntegral_iteratedFDeriv, tendsto_integral_exp_smul_cocompact, fourier_real_eq, VectorFourier.differentiable_fourierIntegral, fourierIntegral_convergent_iff', VectorFourier.iteratedFDeriv_fourierIntegral, fourierIntegral_eq_half_sub_half_period_translate, VectorFourier.fderiv_fourierIntegral, fourier_eq, tendsto_integral_exp_smul_cocompact_of_inner_product, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', VectorFourier.contDiff_fourierIntegral, fourierIntegral_convergent_iff, hasDerivAt_fourierChar, fourierChar_apply, fourier_bilin_convolution_eq_integral, tendsto_integral_exp_smul_cocompact, fourierIntegral_half_period_translate, fourierChar_apply', fourierIntegral_continuousLinearMap_apply', differentiable_fourierChar, continuous_fourierChar, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, deriv_fourierChar, differentiable_fourierChar_neg_bilinear_right, tendsto_integral_exp_inner_smul_cocompact, hasFDerivAt_fourierChar_neg_bilinear_right, differentiable_fourierChar_neg_bilinear_left, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, fourierInv_eq, zero_at_infty_vector_fourierIntegral, VectorFourier.hasFDerivAt_fourierChar_smul, fourierIntegral_real_eq, VectorFourier.fourierIntegral_fderiv, fourierIntegralInv_eq, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, fderiv_fourierChar_neg_bilinear_left_apply, fourierIntegral_continuousMultilinearMap_apply'
probChar 📖	CompOp	6 math math: MeasureTheory.charFun_eq_fourierIntegral, continuous_probChar, probChar_apply', VectorFourier.fourierIntegral_probChar, probChar_apply, MeasureTheory.charFun_eq_integral_probChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_fourierChar 📖	mathematical	—	Continuous Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instTopologicalSpaceCircle DFunLike.coe AddChar instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar	—	Continuous.comp ContinuousMap.continuous continuous_mul_left IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
continuous_probChar 📖	mathematical	—	Continuous Real Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instTopologicalSpaceCircle DFunLike.coe AddChar instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike probChar	—	ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass
fourierChar_apply 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere DFunLike.coe AddChar Real instAddMonoid Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar Complex.exp Complex.instMul Complex.ofReal instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi Complex.I	—	—
fourierChar_apply' 📖	mathematical	—	DFunLike.coe AddChar Real instAddMonoid Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike Circle.exp instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi	—	—
fourierChar_ne_one 📖	—	—	—	—	DFunLike.ne_iff Nat.instAtLeastTwoHAddOfNat mul_comm mul_assoc inv_mul_cancel₀ ne_of_gt Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo one_mul Circle.exp_pi_ne_one
probChar_apply 📖	mathematical	—	Complex Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere DFunLike.coe AddChar Real instAddMonoid Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike probChar Complex.exp Complex.instMul Complex.ofReal Complex.I	—	—
probChar_apply' 📖	mathematical	—	DFunLike.coe AddChar Real instAddMonoid Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike probChar ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike Circle.exp	—	—
probChar_ne_one 📖	—	—	—	—	DFunLike.ne_iff Circle.exp_pi_ne_one

(root)

Definitions

Name	Category	Theorems
instTopologicalSpaceCircle 📖	CompOp	51 math math: Circle.periodic_exp, Circle.exp_arg, AddCircle.homeomorphCircle'_apply_mk, Circle.exp_natCast_mul, AddCircle.homeomorphCircle'_symm_apply, Circle.isAddQuotientCoveringMap_exp, Circle.exp_eq_exp, Circle.exp_two_pi_mul_int, AddCircle.scaled_exp_map_periodic, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, Circle.exp_two_pi, Circle.exp_sub, Circle.isQuotientCoveringMap_zpow, Real.continuous_probChar, Circle.exp_neg, Circle.instIsTopologicalGroup, Circle.exp_inj, Circle.exp_add_two_pi, Circle.invOn_arg_exp, Circle.instContinuousSMul, Real.Angle.toCircle_coe, AddCircle.continuous_toCircle, Circle.exp_add, Circle.leftInverse_exp_arg, Circle.argEquiv_symm_apply, AddCircle.toCircle_apply_mk, Circle.isQuotientCoveringMap_npow, Real.probChar_apply', Circle.instCompactSpace, Circle.exp_zero, Circle.exp_int_mul_two_pi, Circle.surjOn_exp_neg_pi_pi, Circle.exp_intCast_mul, Real.fourierChar_apply', Real.continuous_fourierChar, isLocalHomeomorph_circleExp, Circle.expHom_apply, Circle.arg_exp, Circle.coe_exp, Circle.exp_zsmul, Circle.exp_eq_one, Circle.isCoveringMap_exp, AddChar.zmod_intCast, AddCircle.homeomorphCircle'_apply, AddCircle.homeomorphCircle_apply, Circle.exp_sub_two_pi, Circle.argPartialEquiv_symm_apply, ZMod.toCircle_eq_circleExp, Circle.exp_nsmul, contMDiff_circleExp

---

← Back to Index