AddCircle

📁 Source: Mathlib/Analysis/Fourier/AddCircle.lean

Statistics

Metric	Count
Definitions haarAddCircle, instIsAddHaarMeasureRealHaarAddCircle, fourier, fourierBasis, fourierCoeff, fourierCoeffOn, fourierLp, fourierSubalgebra	8
Theorems instIsProbabilityMeasureRealHaarAddCircle, integral_haarAddCircle, volume_eq_smul_haarAddCircle, fourier_smul, haarAddCircle, of_haarAddCircle, memLp_haarAddCircle_iff, coeFn_fourierLp, coe_fourierBasis, fourierBasis_repr, add, const_mul, const_smul, sum, const_mul, const_smul, fourierCoeffOn_congr_ae, fourierCoeffOn_eq_integral, fourierCoeffOn_of_hasDerivAt, fourierCoeffOn_of_hasDerivAt_Ioo, fourierCoeffOn_of_hasDeriv_right, fourierCoeff_congr_ae, fourierCoeff_eq_intervalIntegral, fourierCoeff_fourier, fourierCoeff_liftIco_eq, fourierCoeff_liftIoc_eq, fourierCoeff_toLp, fourierSubalgebra_closure_eq_top, fourierSubalgebra_coe, fourierSubalgebra_separatesPoints, fourier_add, fourier_add', fourier_add_half_inv_index, fourier_apply, fourier_coe_apply, fourier_coe_apply', fourier_eval_zero, fourier_neg, fourier_neg', fourier_norm, fourier_one, fourier_zero, fourier_zero', hasDerivAt_fourier, hasDerivAt_fourier_neg, hasSum_fourier_series_L2, hasSum_fourier_series_of_summable, hasSum_sq_fourierCoeff, hasSum_sq_fourierCoeffOn, has_antideriv_at_fourier_neg, has_pointwise_sum_fourier_series_of_summable, orthonormal_fourier, span_fourierLp_closure_eq_top, span_fourier_closure_eq_top, tsum_sq_fourierCoeff, tsum_sq_fourierCoeffOn	56
Total	64

AddCircle

Definitions

Name	Category	Theorems
haarAddCircle 📖	CompOp	15 math math: volume_eq_smul_haarAddCircle, integral_haarAddCircle, orthonormal_fourier, MeasureTheory.memLp_haarAddCircle_iff, Polynomial.toAddCircle.integrable, hasSum_fourier_series_L2, instIsProbabilityMeasureRealHaarAddCircle, fourierCoeff_toLp, coe_fourierBasis, span_fourierLp_closure_eq_top, MeasureTheory.MemLp.haarAddCircle, hasSum_sq_fourierCoeff, fourierBasis_repr, tsum_sq_fourierCoeff, coeFn_fourierLp
instIsAddHaarMeasureRealHaarAddCircle 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsProbabilityMeasureRealHaarAddCircle 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples haarAddCircle	—	MeasureTheory.Measure.addHaarMeasure_self compactSpace
integral_haarAddCircle 📖	mathematical	—	MeasureTheory.integral AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples haarAddCircle 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume	—	IsScalarTower.right volume_eq_smul_haarAddCircle MeasureTheory.integral_smul_measure ENNReal.toReal_ofReal LT.lt.le Fact.out inv_smul_smul₀ LT.lt.ne'
volume_eq_smul_haarAddCircle 📖	mathematical	—	MeasureTheory.MeasureSpace.volume AddCircle Real Real.instAddCommGroup measureSpace ENNReal MeasureTheory.Measure QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.ofReal haarAddCircle	—	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
memLp_haarAddCircle_iff 📖	mathematical	—	MemLp AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing AddCircle.haarAddCircle MeasureSpace.toMeasurableSpace AddCircle.measureSpace MeasureSpace.volume	—	IsScalarTower.right AddCircle.volume_eq_smul_haarAddCircle Fact.out MemLp.smul_measure ENNReal.ofReal_ne_top ENNReal.Finiteness.inv_ne_top ne_of_gt ENNReal.ofReal_pos one_smul ENNReal.inv_mul_cancel smul_smul

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourier_smul 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples AddCircle.haarAddCircle	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 DFunLike.coe ContinuousMap QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMap.instFunLike fourier	—	bdd_smul NormedSpace.toIsBoundedSMul Continuous.aestronglyMeasurable BorelSpace.opensMeasurable QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right secondCountable_of_proper Complex.instProperSpace ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass fourier_apply Circle.norm_coe le_refl

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
haarAddCircle 📖	mathematical	MeasureTheory.MemLp AddCircle Real Real.instAddCommGroup Complex MeasureTheory.MeasureSpace.toMeasurableSpace AddCircle.measureSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing MeasureTheory.MeasureSpace.volume	QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples AddCircle.haarAddCircle	—	MeasureTheory.memLp_haarAddCircle_iff
of_haarAddCircle 📖	mathematical	MeasureTheory.MemLp AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing AddCircle.haarAddCircle	MeasureTheory.MeasureSpace.toMeasurableSpace AddCircle.measureSpace MeasureTheory.MeasureSpace.volume	—	MeasureTheory.memLp_haarAddCircle_iff

(root)

Definitions

Name	Category	Theorems
fourier 📖	CompOp	41 math math: Real.tsum_eq_tsum_fourier, has_pointwise_sum_fourier_series_of_summable, span_fourier_closure_eq_top, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, hasSum_one_div_nat_pow_mul_fourier, Polynomial.toAddCircle_X_pow_eq_fourier, fourier_norm, fourier_one, fourier_zero, fourier_neg', Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, fourier_coe_apply, has_antideriv_at_fourier_neg, hasDerivAt_fourier_neg, fourier_eval_zero, hasDerivAt_fourier, fourier_apply, fourierSubalgebra_coe, Polynomial.toAddCircle_monomial_eq_smul_fourier, fourierCoeff_eq_intervalIntegral, fourierCoeffOn_of_hasDerivAt_Ioo, fourier_neg, Real.tsum_eq_tsum_fourier_of_rpow_decay, hasSum_fourier_series_of_summable, fourierCoeffOn_eq_integral, UnitAddTorus.mFourier_single, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, fourier_add', MeasureTheory.Integrable.fourier_smul, Polynomial.toAddCircle_X_eq_fourier_one, fourier_add_half_inv_index, fourierCoeffOn_of_hasDerivAt, Real.tsum_eq_tsum_fourierIntegral, SchwartzMap.tsum_eq_tsum_fourierIntegral, fourier_add, Polynomial.toAddCircle_C_eq_smul_fourier_zero, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, fourierCoeffOn_of_hasDeriv_right, coeFn_fourierLp, SchwartzMap.tsum_eq_tsum_fourier, fourierCoeff_fourier
fourierBasis 📖	CompOp	2 math math: coe_fourierBasis, fourierBasis_repr
fourierCoeff 📖	CompOp	19 math math: Real.fourierCoeff_tsum_comp_add, fourierCoeff.sum, fourierCoeff_bernoulli_eq, hasSum_fourier_series_L2, fourierCoeff.const_smul, fourierCoeff_toLp, fourierCoeff_eq_intervalIntegral, Polynomial.fourierCoeff_toAddCircle_natCast, fourierCoeff.add, fourierCoeff.const_mul, hasSum_sq_fourierCoeff, fourierBasis_repr, fourierCoeff_congr_ae, fourierCoeff_liftIoc_eq, tsum_sq_fourierCoeff, Polynomial.fourierCoeff_toAddCircle, fourierCoeff_liftIco_eq, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, fourierCoeff_fourier
fourierCoeffOn 📖	CompOp	11 math math: fourierCoeffOn.const_mul, fourierCoeffOn_congr_ae, hasSum_sq_fourierCoeffOn, fourierCoeffOn_of_hasDerivAt_Ioo, tsum_sq_fourierCoeffOn, fourierCoeffOn_eq_integral, fourierCoeff_liftIoc_eq, fourierCoeffOn_of_hasDerivAt, fourierCoeffOn.const_smul, fourierCoeffOn_of_hasDeriv_right, fourierCoeff_liftIco_eq
fourierLp 📖	CompOp	5 math math: orthonormal_fourier, hasSum_fourier_series_L2, coe_fourierBasis, span_fourierLp_closure_eq_top, coeFn_fourierLp
fourierSubalgebra 📖	CompOp	3 math math: fourierSubalgebra_separatesPoints, fourierSubalgebra_coe, fourierSubalgebra_closure_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_fourierLp 📖	mathematical	—	Filter.EventuallyEq AddCircle Real Real.instAddCommGroup Complex MeasureTheory.ae MeasureTheory.Measure QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass AddCircle.haarAddCircle MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp fourierLp DFunLike.coe ContinuousMap QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier	—	ContinuousMap.coeFn_toLp QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable secondCountable_of_proper Complex.instProperSpace AddCircle.compactSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AddCircle.instIsProbabilityMeasureRealHaarAddCircle
coe_fourierBasis 📖	mathematical	—	DFunLike.coe HilbertBasis Complex Complex.instRCLike MeasureTheory.AEEqFun AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup AddCircle.haarAddCircle AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal MeasureTheory.L2.innerProductSpace RCLike.innerProductSpace HilbertBasis.instFunLike fourierBasis fourierLp	—	fact_one_le_two_ennreal orthonormal_fourier
fourierBasis_repr 📖	mathematical	—	PreLp Complex NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Complex.instRCLike AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MeasureTheory.AEEqFun AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace Real.measurableSpace AddSubgroup.zmultiples UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup AddCircle.haarAddCircle MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal lp.normedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace MeasureTheory.L2.innerProductSpace RCLike.innerProductSpace lp.instModuleSubtypePreLpMemAddSubgroup NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedSpace.toIsBoundedSMul EquivLike.toFunLike LinearIsometryEquiv.instEquivLike HilbertBasis.repr fourierBasis fourierCoeff MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul HilbertBasis.repr_apply_apply MeasureTheory.L2.inner_def coe_fourierBasis RCLike.inner_apply' MeasureTheory.integral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass coeFn_fourierLp Filter.univ_mem' fourier_neg smul_eq_mul
fourierCoeffOn_congr_ae 📖	mathematical	Real Real.instLT Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder	fourierCoeffOn	—	MeasureTheory.Measure.instOuterMeasureClass fourierCoeffOn_eq_integral intervalIntegral.integral_congr_ae_restrict MeasureTheory.ae.congr_simp Set.uIoc_of_le LT.lt.le Filter.mp_mem Filter.univ_mem'
fourierCoeffOn_eq_integral 📖	mathematical	Real Real.instLT	fourierCoeffOn 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NormedSpace.complexToReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instSub intervalIntegral Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNormedField DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMap.instFunLike fourier MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Real.instIsOrderedAddMonoid Real.instArchimedean fourierCoeffOn.eq_1 fourierCoeff_eq_intervalIntegral add_sub add_sub_cancel_left intervalIntegral.integral_of_le LT.lt.le MeasureTheory.setIntegral_congr_fun measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal AddCircle.liftIoc_coe_apply
fourierCoeffOn_of_hasDerivAt 📖	mathematical	Real Real.instLT HasDerivAt 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 IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	fourierCoeffOn Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Complex.instSub DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup Real.instSub QuotientAddGroup.instTopologicalSpace AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul fourierCoeffOn_of_hasDerivAt_Ioo ContinuousAt.continuousWithinAt HasDerivAt.continuousAt Set.mem_Icc_of_Ioo
fourierCoeffOn_of_hasDerivAt_Ioo 📖	mathematical	Real Real.instLT ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set.uIcc Real.lattice HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Complex.addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex IsBoundedSMul.continuousSMul 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 IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	fourierCoeffOn Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Complex.instSub DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup Real.instSub QuotientAddGroup.instTopologicalSpace AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul fourierCoeffOn_of_hasDeriv_right HasDerivAt.hasDerivWithinAt
fourierCoeffOn_of_hasDeriv_right 📖	mathematical	Real Real.instLT ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set.uIcc Real.lattice HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Complex.addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex IsBoundedSMul.continuousSMul 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 Set.Ioi Real.instPreorder IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	fourierCoeffOn Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Complex.instSub DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup Real.instSub QuotientAddGroup.instTopologicalSpace AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat Complex.ofReal_sub lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le fourierCoeffOn_eq_integral Complex.ofReal_div mul_comm intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right Complex.instCompleteSpace ContinuousAt.continuousWithinAt HasDerivAt.continuousAt has_antideriv_at_fourier_neg HasDerivAt.hasDerivWithinAt Continuous.intervalIntegrable Real.locallyFinite_volume AddSubgroup.normal_of_comm Continuous.comp ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass AddCircle.continuous_mk' Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_inv_neg Mathlib.Meta.NormNum.IsInt.to_isRat Nat.cast_one add_sub_cancel AddCircle.coe_add_period intervalIntegral.integral_const_mul sub_mul mul_sub mul_div mul_one div_eq_iff Complex.ofReal_ne_zero LT.lt.ne' Fact.out Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz
fourierCoeff_congr_ae 📖	mathematical	Filter.EventuallyEq AddCircle Real Real.instAddCommGroup MeasureTheory.ae MeasureTheory.Measure QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass AddCircle.haarAddCircle	fourierCoeff	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integral_congr_ae Filter.EventuallyEq.smul Filter.EventuallyEq.refl
fourierCoeff_eq_intervalIntegral 📖	mathematical	—	fourierCoeff Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NormedSpace.complexToReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne intervalIntegral Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNormedField DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMap.instFunLike fourier Real.instAdd MeasureTheory.MeasureSpace.volume Real.measureSpace	—	fourierCoeff.eq_1 AddCircle.intervalIntegral_preimage IsScalarTower.right AddCircle.volume_eq_smul_haarAddCircle MeasureTheory.integral_smul_measure ENNReal.toReal_ofReal LT.lt.le Fact.out smul_assoc IsScalarTower.left smul_eq_mul one_div_mul_cancel LT.lt.ne' one_smul
fourierCoeff_fourier 📖	mathematical	—	fourierCoeff Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier Pi.single Complex.instZero Complex.instOne	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal fourierCoeff_congr_ae coeFn_fourierLp RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul fourierBasis_repr HilbertBasis.repr_apply_apply coe_fourierBasis eq_or_ne inner_self_eq_norm_sq_to_K orthonormal_fourier one_pow Pi.single_eq_same Pi.single_eq_of_ne
fourierCoeff_liftIco_eq 📖	mathematical	—	fourierCoeff Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace AddCircle.liftIco Real Real.instAddCommGroup Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean fourierCoeffOn AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid lt_add_of_pos_right Real.instLT IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Real.instAddLeftCancelSemigroup Real.partialOrder IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Fact.out Real.instZero	—	Real.instIsOrderedAddMonoid Real.instArchimedean lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Fact.out fourierCoeffOn_eq_integral fourierCoeff_eq_intervalIntegral add_sub_cancel_left intervalIntegral.integral_of_le LT.lt.le MeasureTheory.integral_Ioc_eq_integral_Ioo Real.noAtoms_volume MeasureTheory.setIntegral_congr_fun measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal AddCircle.liftIco_coe_apply Set.Ioo_subset_Ico_self
fourierCoeff_liftIoc_eq 📖	mathematical	—	fourierCoeff Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace AddCircle.liftIoc Real Real.instAddCommGroup Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean fourierCoeffOn AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid lt_add_of_pos_right Real.instLT IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Real.instAddLeftCancelSemigroup Real.partialOrder IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Fact.out Real.instZero	—	Real.instIsOrderedAddMonoid Real.instArchimedean lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Fact.out fourierCoeffOn_eq_integral fourierCoeff_eq_intervalIntegral add_sub_cancel_left intervalIntegral.integral_congr_ae MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass AddCircle.liftIoc_coe_apply Set.uIoc_of_le LT.lt.le
fourierCoeff_toLp 📖	mathematical	—	fourierCoeff Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace MeasureTheory.AEEqFun.cast AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples AddCircle.haarAddCircle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousMap QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal ContinuousMap.module Complex.instModuleSelf UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing MeasureTheory.Lp.instModule ContinuousLinearMap.funLike ContinuousMap.toLp QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable SeminormedCommRing.toSeminormedRing NormedField.toMetricSpace secondCountable_of_proper Complex.instProperSpace AddCircle.compactSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AddCircle.instIsProbabilityMeasureRealHaarAddCircle ContinuousMap.instFunLike	—	MeasureTheory.integral_congr_ae Nat.instAtLeastTwoHAddOfNat IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_two_ennreal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable secondCountable_of_proper Complex.instProperSpace AddCircle.compactSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AddCircle.instIsProbabilityMeasureRealHaarAddCircle Filter.EventuallyEq.mul MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.of_forall ContinuousMap.coeFn_toAEEqFun PseudoEMetricSpace.pseudoMetrizableSpace
fourierSubalgebra_closure_eq_top 📖	mathematical	—	StarSubalgebra.topologicalClosure Complex ContinuousMap AddCircle Real Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instCommSemiring Complex.instStarRing ContinuousMap.compactOpen ContinuousMap.instSemiringOfIsTopologicalSemiring Complex.instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.algebra Algebra.id ContinuousMap.instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Complex.instContinuousStar ContinuousMap.instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid Complex.commRing StarRing.toStarMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace QuotientAddGroup.instLocallyCompactSpace IsTopologicalSemiring.toContinuousAdd Real.normedCommRing instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NormedStarGroup.to_continuousStar ContinuousMap.instSeminormedAddCommGroup AddCircle.compactSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousMap.starAddMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMap.instNormedStarGroup CStarRing.to_normedStarGroup NonUnitalNormedCommRing.toNonUnitalNormedRing RCLike.instCStarRing Complex.instRCLike fourierSubalgebra Top.top StarSubalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice StarSubalgebra.completeLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints AddCircle.compactSpace fourierSubalgebra_separatesPoints
fourierSubalgebra_coe 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Complex ContinuousMap AddCircle Real Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instCommSemiring ContinuousMap.instSemiringOfIsTopologicalSemiring Complex.instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.algebra Algebra.id Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule StarSubalgebra.toSubalgebra Complex.instStarRing ContinuousMap.instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Complex.instContinuousStar ContinuousMap.instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid Complex.commRing StarRing.toStarMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring fourierSubalgebra Submodule.span ContinuousMap.instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup IsTopologicalSemiring.toContinuousAdd ContinuousMap.module Complex.instModuleSelf UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass 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 Set.range fourier	—	Algebra.adjoin_eq_span_of_subset IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Set.Subset.trans Submonoid.closure_induction ContinuousMap.ext fourier_zero fourier_add Submodule.subset_span
fourierSubalgebra_separatesPoints 📖	mathematical	—	Subalgebra.SeparatesPoints AddCircle Real Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples Complex Complex.instCommSemiring SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instSemiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing StarSubalgebra.toSubalgebra ContinuousMap Complex.instStarRing ContinuousMap.instSemiringOfIsTopologicalSemiring ContinuousMap.instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Complex.instContinuousStar ContinuousMap.algebra ContinuousMap.instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid Complex.commRing StarRing.toStarMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring fourierSubalgebra	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule Algebra.subset_adjoin fourier_one Mathlib.Tactic.Contrapose.contrapose₄ AddCircle.injective_toCircle LT.lt.ne' Fact.elim
fourier_add 📖	mathematical	—	DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier Complex.instMul	—	AddSubgroup.normal_of_comm add_zsmul AddCircle.toCircle_add
fourier_add' 📖	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 AddCircle.toCircle AddCircle Real Real.instAddCommGroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm Complex.instMul DFunLike.coe ContinuousMap QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace ContinuousMap.instFunLike fourier	—	AddSubgroup.normal_of_comm fourier_apply fourier_add
fourier_add_half_inv_index 📖	mathematical	Real Real.instLT Real.instZero	DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCircle.instNormedAddCommGroupReal DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instIntCast Complex.instNeg	—	Nat.instAtLeastTwoHAddOfNat AddSubgroup.normal_of_comm fourier_apply zsmul_add QuotientAddGroup.mk_zsmul AddCircle.toCircle_add NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Metric.unitSphere.coe_mul zsmul_eq_mul AddCircle.scaled_exp_map_periodic AddCircle.toCircle.eq_1 Function.Periodic.lift_coe Circle.coe_exp Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero ne_of_gt Int.cast_ne_zero Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Complex.exp_pi_mul_I mul_neg
fourier_apply 📖	mathematical	—	DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere AddCircle.toCircle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm	—	—
fourier_coe_apply 📖	mathematical	—	DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier Complex.exp DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast	—	Nat.instAtLeastTwoHAddOfNat AddSubgroup.normal_of_comm fourier_apply QuotientAddGroup.mk_zsmul AddCircle.scaled_exp_map_periodic AddCircle.toCircle.eq_1 Function.Periodic.lift_coe Circle.coe_exp Complex.ofReal_mul Complex.ofReal_div zsmul_eq_mul Complex.ofReal_intCast Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left
fourier_coe_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 AddCircle.toCircle HasQuotient.Quotient Real AddSubgroup AddCommGroup.toAddGroup Real.instAddCommGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm Complex.exp DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast	—	AddSubgroup.normal_of_comm Nat.instAtLeastTwoHAddOfNat fourier_apply fourier_coe_apply
fourier_eval_zero 📖	mathematical	—	DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Complex.instOne	—	AddSubgroup.normal_of_comm QuotientAddGroup.mk_zero Nat.instAtLeastTwoHAddOfNat fourier_coe_apply Complex.ofReal_zero MulZeroClass.mul_zero zero_div Complex.exp_zero
fourier_neg 📖	mathematical	—	DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	QuotientAddGroup.induction_on AddSubgroup.normal_of_comm AddCircle.scaled_exp_map_periodic QuotientAddGroup.mk_zsmul neg_smul mul_neg
fourier_neg' 📖	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 AddCircle.toCircle AddCircle Real Real.instAddCommGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm DFunLike.coe RingHom CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing ContinuousMap QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace ContinuousMap.instFunLike fourier	—	AddSubgroup.normal_of_comm neg_smul fourier_apply fourier_neg
fourier_norm 📖	mathematical	—	Norm.norm ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instNorm AddCircle.compactSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing fourier Real.instOne	—	AddCircle.compactSpace ContinuousMap.norm_eq_iSup_norm Circle.norm_coe ciSup_const
fourier_one 📖	mathematical	—	DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing SetLike.instMembership Submonoid.instSetLike Submonoid.unitSphere AddCircle.toCircle	—	AddSubgroup.normal_of_comm fourier_apply one_zsmul
fourier_zero 📖	mathematical	—	DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike fourier Complex.instOne	—	AddSubgroup.normal_of_comm zero_smul AddCircle.toCircle_zero
fourier_zero' 📖	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 AddCircle.toCircle AddCircle Real Real.instAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Complex.instOne	—	AddCircle.toCircle_zero
hasDerivAt_fourier 📖	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 DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace AddSubgroup.zmultiples ContinuousMap.instFunLike fourier Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat HasDerivAt.congr_simp fourier_coe_apply HasDerivAt.comp_ofReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul HasDerivAt.comp Complex.hasDerivAt_exp ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw hasDerivAt_mul_const
hasDerivAt_fourier_neg 📖	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 DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace AddSubgroup.zmultiples ContinuousMap.instFunLike fourier Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat HasDerivAt.congr_simp AddSubgroup.normal_of_comm neg_smul fourier_neg' fourier_coe_apply' neg_mul Int.cast_neg mul_neg hasDerivAt_fourier
hasSum_fourier_series_L2 📖	mathematical	—	HasSum MeasureTheory.AEEqFun AddCircle Real Real.instAddCommGroup Complex QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup AddCircle.haarAddCircle AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat ESeminormedAddCommMonoid.toAddCommMonoid MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing Complex.instNormedField Complex.instModuleSelf NormedSpace.toIsBoundedSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace fourierCoeff MeasureTheory.AEEqFun.cast fourierLp SummationFilter.unconditional	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul RingHomInvPair.ids coe_fourierBasis HilbertBasis.hasSum_repr
hasSum_fourier_series_of_summable 📖	mathematical	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup fourierCoeff InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike SummationFilter.unconditional	HasSum ContinuousMap.instAddCommMonoidOfContinuousAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.compactOpen ContinuousMap.instSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul Complex.instRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing fourier	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable secondCountable_of_proper Complex.instProperSpace AddCircle.compactSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AddCircle.instIsProbabilityMeasureRealHaarAddCircle hasSum_fourier_series_L2 ContinuousMap.hasSum_of_hasSum_Lp MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Summable.of_norm ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace Complex.instCompleteSpace CompactlyCoherentSpace.of_sequentialSpace FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace QuotientAddGroup.instFirstCountableTopology IsTopologicalSemiring.toContinuousAdd instIsTopologicalRingReal TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace norm_smul NormedSpace.toNormSMulClass fourier_norm mul_one Summable.norm FiniteDimensional.rclike_to_real fourierCoeff_toLp
hasSum_sq_fourierCoeff 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm Complex Complex.instNorm fourierCoeff Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace MeasureTheory.AEEqFun.cast AddCircle Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples AddCircle.haarAddCircle SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.integral Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal SummationFilter.unconditional	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul ENNReal.toReal_natCast Real.rpow_natCast lp.hasSum_norm ENNReal.toReal_ofNat Real.instIsOrderedRing Real.instNontrivial LinearIsometryEquiv.norm_map MeasureTheory.L2.inner_def integral_re MeasureTheory.L2.integrable_inner
hasSum_sq_fourierCoeffOn 📖	mathematical	Real Real.instLT MeasureTheory.MemLp Complex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder	HasSum Real.instAddCommMonoid Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm Complex.instNorm fourierCoeffOn Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv Real.instSub intervalIntegral Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Real.instIsOrderedAddMonoid lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instArchimedean MeasureTheory.MemLp.haarAddCircle MeasureTheory.MemLp.memLp_liftIoc add_sub_cancel lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Fact.out SeminormedAddCommGroup.toIsTopologicalAddGroup fourierCoeff_congr_ae MeasureTheory.MemLp.coeFn_toLp fourierCoeff_liftIoc_eq fourierCoeffOn.congr_simp AddCircle.integral_liftIoc_eq_intervalIntegral MeasureTheory.integral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem' hasSum_sq_fourierCoeff
has_antideriv_at_fourier_neg 📖	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 Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.ofReal Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.I Complex.instIntCast DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat div_div_eq_mul_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_inv_neg Complex.instCharZero Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.one_mul AddSubgroup.normal_of_comm neg_smul fourier_neg' fourier_coe_apply' neg_mul mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne' Real.pi_pos Fact.out HasDerivAt.div_const hasDerivAt_fourier_neg
has_pointwise_sum_fourier_series_of_summable 📖	mathematical	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup fourierCoeff InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DFunLike.coe ContinuousMap AddCircle Real Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike SummationFilter.unconditional	HasSum Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id fourier	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.hasSum hasSum_fourier_series_of_summable
orthonormal_fourier 📖	mathematical	—	Orthonormal Complex MeasureTheory.AEEqFun AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup AddCircle.haarAddCircle AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Complex.instRCLike MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal MeasureTheory.L2.innerProductSpace RCLike.innerProductSpace fourierLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal orthonormal_iff_ite IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable secondCountable_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real AddCircle.compactSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AddCircle.instIsProbabilityMeasureRealHaarAddCircle MeasureTheory.ContinuousMap.inner_toLp add_neg_cancel fourier_zero MeasureTheory.integral_const Complex.instCompleteSpace MeasureTheory.probReal_univ Complex.real_smul Complex.ofReal_one mul_one sub_ne_zero MeasureTheory.integral_eq_zero_of_add_right_eq_neg ContinuousAdd.measurableAdd QuotientAddGroup.instIsTopologicalAddGroup MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant fourier_add_half_inv_index Fact.elim
span_fourierLp_closure_eq_top 📖	mathematical	—	Submodule.topologicalClosure Complex MeasureTheory.AEEqFun AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup AddCircle.haarAddCircle AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Complex.instSemiring MeasureTheory.Lp.instNormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing Complex.instNormedField Complex.instModuleSelf NormedSpace.toIsBoundedSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Complex.instZero AddSubgroup.zero MeasureTheory.Lp.instIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd AddSubgroup.toAddGroup Submodule.span Set.range fourierLp Top.top Submodule Submodule.instTop	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul MeasureTheory.Lp.instIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd ContinuousSMul.continuousConstSMul IsBoundedSMul.continuousSMul RingHomSurjective.ids QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable secondCountable_of_proper Complex.instProperSpace AddCircle.compactSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AddCircle.instIsProbabilityMeasureRealHaarAddCircle IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Submodule.map_span Set.range_comp' Set.image_congr DenseRange.topologicalClosure_map_submodule ContinuousMap.instContinuousSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology ContinuousMap.instContinuousAddOfLocallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal ContinuousMap.toLp_denseRange PerfectlyNormalSpace.toNormalSpace T6Space.toPerfectlyNormalSpace MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite PseudoEMetricSpace.pseudoMetrizableSpace QuotientAddGroup.instSecondCountableTopology MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts span_fourier_closure_eq_top
span_fourier_closure_eq_top 📖	mathematical	—	Submodule.topologicalClosure Complex ContinuousMap AddCircle Real Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instSemiring ContinuousMap.compactOpen ContinuousMap.instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.module Complex.instModuleSelf 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 ContinuousMap.instContinuousConstSMul ContinuousMap.instContinuousAddOfLocallyCompactSpace QuotientAddGroup.instLocallyCompactSpace Real.normedCommRing instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal AddSemigroup.toAdd AddMonoid.toAddSemigroup Submodule.span Set.range fourier Top.top Submodule Submodule.instTop	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousMap.instContinuousConstSMul ContinuousMap.instContinuousAddOfLocallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal Complex.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule fourierSubalgebra_coe ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace NormedStarGroup.to_continuousStar AddCircle.compactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMap.instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing fourierSubalgebra_closure_eq_top
tsum_sq_fourierCoeff 📖	mathematical	—	tsum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm Complex Complex.instNorm fourierCoeff Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace MeasureTheory.AEEqFun.cast AddCircle Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples AddCircle.haarAddCircle SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat SummationFilter.unconditional MeasureTheory.integral Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_sq_fourierCoeff
tsum_sq_fourierCoeffOn 📖	mathematical	Real Real.instLT MeasureTheory.MemLp Complex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder	tsum Real.instAddCommMonoid Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm Complex.instNorm fourierCoeffOn Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SummationFilter.unconditional Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv Real.instSub intervalIntegral Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal	—	Nat.instAtLeastTwoHAddOfNat HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_sq_fourierCoeffOn

fourierCoeff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples AddCircle.haarAddCircle	fourierCoeff Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	smul_add MeasureTheory.integral_add MeasureTheory.Integrable.fourier_smul
const_mul 📖	mathematical	—	fourierCoeff Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul	—	const_smul
const_smul 📖	mathematical	—	fourierCoeff Complex Function.hasSMul AddCircle Real Real.instAddCommGroup 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	—	IsScalarTower.left mul_comm smul_assoc MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal smulCommClass_self
sum 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples AddCircle.haarAddCircle	fourierCoeff Finset.sum Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Finset.induction_on AddSubgroup.normal_of_comm neg_smul fourier_neg' Finset.sum_apply smul_zero MeasureTheory.integral_zero Finset.sum_congr Finset.sum_insert add MeasureTheory.integrable_finset_sum' IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup

fourierCoeffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_mul 📖	mathematical	Real Real.instLT	fourierCoeffOn Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul	—	const_smul
const_smul 📖	mathematical	Real Real.instLT	fourierCoeffOn Complex Function.hasSMul 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	—	fourierCoeff.const_smul Real.instIsOrderedAddMonoid Real.instArchimedean

---

← Back to Index