AddCircleMulti

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

Statistics

Metric	Count
Definitions UnitAddTorus, mFourier, mFourierBasis, mFourierCoeff, mFourierLp, mFourierSubalgebra, instMeasureSpaceUnitAddCircle	7
Theorems coeFn_mFourierLp, coe_mFourierBasis, hasSum_mFourier_series_L2, hasSum_mFourier_series_apply_of_summable, hasSum_mFourier_series_of_summable, hasSum_prod_mFourierCoeff, hasSum_sq_mFourierCoeff, instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, mFourierBasis_repr, mFourierCoeff_toLp, mFourierSubalgebra_closure_eq_top, mFourierSubalgebra_coe, mFourierSubalgebra_separatesPoints, mFourier_add, mFourier_neg, mFourier_norm, mFourier_single, mFourier_zero, orthonormal_mFourier, span_mFourierLp_closure_eq_top, span_mFourier_closure_eq_top, instIsAddHaarMeasureUnitAddCircleVolume, instIsProbabilityMeasureUnitAddCircleVolume	23
Total	30

UnitAddTorus

Definitions

Name	Category	Theorems
mFourier 📖	CompOp	10 math math: mFourierSubalgebra_coe, mFourier_add, mFourier_zero, coeFn_mFourierLp, mFourier_neg, mFourier_norm, hasSum_mFourier_series_of_summable, span_mFourier_closure_eq_top, hasSum_mFourier_series_apply_of_summable, mFourier_single
mFourierBasis 📖	CompOp	2 math math: coe_mFourierBasis, mFourierBasis_repr
mFourierCoeff 📖	CompOp	5 math math: mFourierCoeff_toLp, hasSum_mFourier_series_L2, hasSum_prod_mFourierCoeff, mFourierBasis_repr, hasSum_sq_mFourierCoeff
mFourierLp 📖	CompOp	5 math math: coe_mFourierBasis, coeFn_mFourierLp, orthonormal_mFourier, hasSum_mFourier_series_L2, span_mFourierLp_closure_eq_top
mFourierSubalgebra 📖	CompOp	3 math math: mFourierSubalgebra_coe, mFourierSubalgebra_closure_eq_top, mFourierSubalgebra_separatesPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_mFourierLp 📖	mathematical	—	Filter.EventuallyEq UnitAddTorus Complex MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume 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 mFourierLp DFunLike.coe ContinuousMap Pi.topologicalSpace QuotientAddGroup.instTopologicalSpace Real Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike mFourier	—	ContinuousMap.coeFn_toLp Pi.borelSpace Finite.to_countable Finite.of_fintype QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instSecondCountableTopologyReal QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace 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 Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike MeasureTheory.Measure.instIsFiniteMeasureForallVolume MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureUnitAddCircleVolume
coe_mFourierBasis 📖	mathematical	—	DFunLike.coe HilbertBasis Complex Complex.instRCLike MeasureTheory.AEEqFun UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume 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 mFourierBasis mFourierLp	—	fact_one_le_two_ennreal orthonormal_mFourier
hasSum_mFourier_series_L2 📖	mathematical	—	HasSum MeasureTheory.AEEqFun UnitAddTorus Complex MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume 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 mFourierCoeff MeasureTheory.AEEqFun.cast mFourierLp SummationFilter.unconditional	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul RingHomInvPair.ids mFourierBasis_repr HilbertBasis.hasSum_repr
hasSum_mFourier_series_apply_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 mFourierCoeff InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DFunLike.coe ContinuousMap UnitAddTorus Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne ContinuousMap.instFunLike SummationFilter.unconditional	HasSum Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id mFourier	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContinuousLinearMap.hasSum hasSum_mFourier_series_of_summable
hasSum_mFourier_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 mFourierCoeff InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DFunLike.coe ContinuousMap UnitAddTorus Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne 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 mFourier	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Pi.borelSpace Finite.to_countable Finite.of_fintype QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instSecondCountableTopologyReal QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace 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 Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike MeasureTheory.Measure.instIsFiniteMeasureForallVolume MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureUnitAddCircleVolume hasSum_mFourier_series_L2 ContinuousMap.hasSum_of_hasSum_Lp MeasureTheory.Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure instIsAddHaarMeasureUnitAddCircleVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite CompactSpace.sigmaCompact Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Summable.of_norm ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace Complex.instCompleteSpace CompactlyCoherentSpace.of_sequentialSpace FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.instFirstCountableTopologyForallOfCountable QuotientAddGroup.instFirstCountableTopology TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace norm_smul NormedSpace.toNormSMulClass mFourier_norm mul_one Summable.norm FiniteDimensional.rclike_to_real mFourierCoeff_toLp
hasSum_prod_mFourierCoeff 📖	mathematical	—	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing mFourierCoeff InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace MeasureTheory.AEEqFun.cast UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume 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 Real.instRCLike instInnerProductSpaceRealComplex SummationFilter.unconditional	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat mul_comm HasSum.congr_fun fact_one_le_two_ennreal HilbertBasis.hasSum_inner_mul_inner RingHomInvPair.ids NormedSpace.toIsBoundedSMul HilbertBasis.repr_apply_apply inner_conj_symm
hasSum_sq_mFourierCoeff 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm Complex Complex.instNorm mFourierCoeff Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace MeasureTheory.AEEqFun.cast UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume 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 inner_self_eq_norm_sq integral_re MeasureTheory.L2.integrable_inner RCLike.hasSum_re hasSum_prod_mFourierCoeff
instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp 📖	mathematical	—	ContinuousSMul Complex MeasureTheory.AEEqFun UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid MeasureTheory.Lp.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul IsBoundedSMul.continuousSMul MeasureTheory.Lp.instIsBoundedSMul
mFourierBasis_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 UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume 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 mFourierBasis mFourierCoeff 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_mFourierBasis mul_comm MeasureTheory.integral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass coeFn_mFourierLp Filter.univ_mem' mFourier_neg smul_eq_mul
mFourierCoeff_toLp 📖	mathematical	—	mFourierCoeff Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace MeasureTheory.AEEqFun.cast UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume 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 Pi.topologicalSpace QuotientAddGroup.instTopologicalSpace Real Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne 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 Pi.borelSpace Finite.to_countable Finite.of_fintype QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instSecondCountableTopologyReal QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Real.instAddGroup instIsTopologicalAddGroupReal Real.measurableSpace 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 Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike MeasureTheory.Measure.instIsFiniteMeasureForallVolume MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureUnitAddCircleVolume ContinuousMap.instFunLike	—	MeasureTheory.integral_congr_ae Nat.instAtLeastTwoHAddOfNat IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_two_ennreal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Pi.borelSpace Finite.to_countable Finite.of_fintype QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instSecondCountableTopologyReal QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace 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 Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike MeasureTheory.Measure.instIsFiniteMeasureForallVolume MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureUnitAddCircleVolume Filter.EventuallyEq.mul MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_rfl ContinuousMap.coeFn_toAEEqFun PseudoEMetricSpace.pseudoMetrizableSpace
mFourierSubalgebra_closure_eq_top 📖	mathematical	—	StarSubalgebra.topologicalClosure Complex ContinuousMap UnitAddTorus Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne 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 Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace IsTopologicalSemiring.toContinuousAdd Real.normedCommRing instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NormedStarGroup.to_continuousStar ContinuousMap.instSeminormedAddCommGroup Function.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 mFourierSubalgebra 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 Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike mFourierSubalgebra_separatesPoints
mFourierSubalgebra_coe 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Complex ContinuousMap UnitAddTorus Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne 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 mFourierSubalgebra 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 mFourier	—	Algebra.adjoin_eq_span_of_subset IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasSubset.Subset.trans Set.instIsTransSubset Submonoid.closure_induction ContinuousMap.ext Finset.prod_congr fourier_zero Finset.prod_const one_pow AddSubgroup.normal_of_comm fourier_add' Finset.prod_mul_distrib Submodule.subset_span
mFourierSubalgebra_separatesPoints 📖	mathematical	—	Subalgebra.SeparatesPoints UnitAddTorus Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne 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 mFourierSubalgebra	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule Algebra.subset_adjoin mFourier_single fourier_one Mathlib.Tactic.Contrapose.contrapose₄ AddCircle.injective_toCircle one_ne_zero NeZero.charZero_one RCLike.charZero_rclike
mFourier_add 📖	mathematical	—	DFunLike.coe ContinuousMap UnitAddTorus Complex Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike mFourier Pi.instAdd Complex.instMul	—	Finset.prod_congr fourier_add
mFourier_neg 📖	mathematical	—	DFunLike.coe ContinuousMap UnitAddTorus Complex Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike mFourier Pi.instNeg RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	Finset.prod_congr fourier_neg map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
mFourier_norm 📖	mathematical	—	Norm.norm ContinuousMap UnitAddTorus Complex Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instNorm Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing mFourier	—	le_antisymm Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ContinuousMap.norm_le zero_le_one AddSubgroup.normal_of_comm Finset.prod_congr norm_prod NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Circle.norm_coe Finset.prod_const_one LE.le.trans le_of_eq fourier_eval_zero CStarRing.norm_one RCLike.instCStarRing Complex.instNontrivial ContinuousMap.norm_coe_le_norm
mFourier_single 📖	mathematical	—	DFunLike.coe ContinuousMap UnitAddTorus Complex Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instFunLike mFourier Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing AddCircle fourier	—	Finset.prod_mul_prod_compl Finset.prod_congr Pi.single_eq_of_ne Finset.mem_singleton Finset.mem_compl fourier_zero Finset.prod_singleton Finset.prod_const_one mul_one Pi.single_eq_same
mFourier_zero 📖	mathematical	—	mFourier Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing ContinuousMap UnitAddTorus Complex Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instOne Complex.instOne	—	ContinuousMap.ext Finset.prod_congr fourier_zero Finset.prod_const_one
orthonormal_mFourier 📖	mathematical	—	Orthonormal Complex MeasureTheory.AEEqFun UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume 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 mFourierLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal orthonormal_iff_ite IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real MeasureTheory.ContinuousMap.inner_toLp add_neg_cancel mFourier_zero MeasureTheory.probReal_univ MeasureTheory.Measure.instIsProbabilityMeasureForallVolume instIsProbabilityMeasureUnitAddCircleVolume one_smul MeasureTheory.integral_const Complex.instCompleteSpace mFourier.eq_1 MeasureTheory.integral_fintype_prod_volume_eq_prod MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite AddSubgroup.normal_of_comm instIsAddHaarMeasureUnitAddCircleVolume CompactSpace.sigmaCompact AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Function.ne_iff Finset.prod_eq_zero Finset.mem_univ eq_false_intro orthonormal_fourier
span_mFourierLp_closure_eq_top 📖	mathematical	—	Submodule.topologicalClosure Complex MeasureTheory.AEEqFun UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MeasureTheory.MeasureSpace.volume 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 mFourierLp Top.top Submodule Submodule.instTop	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul ContinuousSMul.continuousConstSMul instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul RingHomSurjective.ids secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace Function.compactSpace AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Submodule.topologicalClosure.congr_simp Submodule.map_span Set.image_congr DenseRange.topologicalClosure_map_submodule ContinuousMap.instContinuousSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology ContinuousMap.instContinuousAddOfLocallyCompactSpace Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal ContinuousMap.toLp_denseRange PerfectlyNormalSpace.toNormalSpace T6Space.toPerfectlyNormalSpace instT6SpaceOfMetrizableSpace TopologicalSpace.metrizableSpace_pi Finite.of_fintype EMetricSpace.metrizableSpace MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite TopologicalSpace.pseudoMetrizableSpace_pi PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.instSecondCountableTopologyForallOfCountable Finite.to_countable QuotientAddGroup.instSecondCountableTopology instSecondCountableTopologyReal Pi.borelSpace QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace T6Space.toT0Space instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureUnitAddCircleVolume CompactSpace.sigmaCompact MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts span_mFourier_closure_eq_top
span_mFourier_closure_eq_top 📖	mathematical	—	Submodule.topologicalClosure Complex ContinuousMap UnitAddTorus Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne 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 Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace Real.normedCommRing instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike AddSemigroup.toAdd AddMonoid.toAddSemigroup Submodule.span Set.range mFourier 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 Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Complex.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule mFourierSubalgebra_coe ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace NormedStarGroup.to_continuousStar Function.compactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMap.instNormedStarGroup CStarRing.to_normedStarGroup RCLike.instCStarRing mFourierSubalgebra_closure_eq_top

(root)

Definitions

Name	Category	Theorems
UnitAddTorus 📖	CompOp	19 math math: UnitAddTorus.coe_mFourierBasis, UnitAddTorus.mFourierSubalgebra_coe, UnitAddTorus.mFourierSubalgebra_closure_eq_top, UnitAddTorus.mFourierCoeff_toLp, UnitAddTorus.mFourier_add, UnitAddTorus.mFourier_zero, UnitAddTorus.coeFn_mFourierLp, UnitAddTorus.mFourier_neg, UnitAddTorus.mFourier_norm, UnitAddTorus.orthonormal_mFourier, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, UnitAddTorus.hasSum_mFourier_series_L2, UnitAddTorus.mFourierSubalgebra_separatesPoints, UnitAddTorus.hasSum_prod_mFourierCoeff, UnitAddTorus.mFourierBasis_repr, UnitAddTorus.span_mFourier_closure_eq_top, UnitAddTorus.hasSum_sq_mFourierCoeff, UnitAddTorus.mFourier_single, UnitAddTorus.span_mFourierLp_closure_eq_top
instMeasureSpaceUnitAddCircle 📖	CompOp	12 math math: UnitAddTorus.coe_mFourierBasis, UnitAddTorus.mFourierCoeff_toLp, UnitAddTorus.coeFn_mFourierLp, UnitAddTorus.orthonormal_mFourier, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, UnitAddTorus.hasSum_mFourier_series_L2, UnitAddTorus.hasSum_prod_mFourierCoeff, instIsProbabilityMeasureUnitAddCircleVolume, UnitAddTorus.mFourierBasis_repr, UnitAddTorus.hasSum_sq_mFourierCoeff, instIsAddHaarMeasureUnitAddCircleVolume, UnitAddTorus.span_mFourierLp_closure_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAddHaarMeasureUnitAddCircleVolume 📖	mathematical	—	MeasureTheory.Measure.IsAddHaarMeasure UnitAddCircle QuotientAddGroup.Quotient.addGroup Real AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne AddSubgroup.normal_of_comm QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume	—	AddSubgroup.normal_of_comm
instIsProbabilityMeasureUnitAddCircleVolume 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure UnitAddCircle MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume	—	AddCircle.instIsProbabilityMeasureRealHaarAddCircle

---

← Back to Index