AddCircleMulti

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

Statistics

Metric	Count
Definitions UnitAddTorus, mFourier, mFourierBasis, mFourierCoeff, mFourierLp, mFourierSubalgebra, measurableEquivPiIoc, instMeasureSpaceUnitAddCircle	8
Theorems coeFn_mFourierLp, coe_mFourierBasis, coe_measurableEquivPiIoc, coe_measurableEquivPiIoc_apply, coe_symm_measurableEquivPiIoc, coe_symm_measurableEquivPiIoc_apply, hasSum_mFourier_series_L2, hasSum_mFourier_series_apply_of_summable, hasSum_mFourier_series_of_summable, hasSum_prod_mFourierCoeff, hasSum_sq_mFourierCoeff, instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, integral_preimage, lintegral_preimage, mFourierBasis_repr, mFourierCoeff_eq_integral, mFourierCoeff_toLp, mFourierSubalgebra_closure_eq_top, mFourierSubalgebra_coe, mFourierSubalgebra_separatesPoints, mFourier_add, mFourier_neg, mFourier_norm, mFourier_single, mFourier_zero, measurePreserving_equivPiIoc, orthonormal_mFourier, span_mFourierLp_closure_eq_top, span_mFourier_closure_eq_top, instIsAddHaarMeasureUnitAddCircleVolume, instIsProbabilityMeasureUnitAddCircleVolume	31
Total	39

UnitAddTorus

Definitions

Name	Category	Theorems
mFourier 📖	CompOp	11 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, mFourierCoeff_eq_integral
mFourierBasis 📖	CompOp	2 math math: coe_mFourierBasis, mFourierBasis_repr
mFourierCoeff 📖	CompOp	8 math math: mFourierCoeff_toLp, hasSum_mFourier_series_L2, hasSum_mFourier_series_of_summable, hasSum_prod_mFourierCoeff, mFourierBasis_repr, hasSum_mFourier_series_apply_of_summable, hasSum_sq_mFourierCoeff, mFourierCoeff_eq_integral
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
measurableEquivPiIoc 📖	CompOp	5 math math: coe_symm_measurableEquivPiIoc, measurePreserving_equivPiIoc, coe_measurableEquivPiIoc_apply, coe_measurableEquivPiIoc, coe_symm_measurableEquivPiIoc_apply

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 instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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
coe_measurableEquivPiIoc 📖	mathematical	—	DFunLike.coe MeasurableEquiv UnitAddTorus MeasurableSpace.pi UnitAddCircle QuotientAddGroup.measurableSpace Real AddCommGroup.toAddGroup Real.instAddCommGroup Real.measurableSpace AddSubgroup.zmultiples Real.instOne Subtype.instMeasurableSpace EquivLike.toFunLike MeasurableEquiv.instEquivLike measurableEquivPiIoc Set Set.instMembership Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.linearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Equiv AddCircle Set.Elem Equiv.instEquivLike AddCircle.equivIoc Real.instIsOrderedAddMonoid ZeroLEOneClass.factZeroLtOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike Real.instArchimedean	—	—
coe_measurableEquivPiIoc_apply 📖	mathematical	—	DFunLike.coe MeasurableEquiv UnitAddTorus MeasurableSpace.pi UnitAddCircle QuotientAddGroup.measurableSpace Real AddCommGroup.toAddGroup Real.instAddCommGroup Real.measurableSpace AddSubgroup.zmultiples Real.instOne Subtype.instMeasurableSpace EquivLike.toFunLike MeasurableEquiv.instEquivLike measurableEquivPiIoc Set Set.instMembership Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.linearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Equiv AddCircle Set.Elem Equiv.instEquivLike AddCircle.equivIoc Real.instIsOrderedAddMonoid ZeroLEOneClass.factZeroLtOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike Real.instArchimedean	—	—
coe_symm_measurableEquivPiIoc 📖	mathematical	—	DFunLike.coe MeasurableEquiv UnitAddTorus Subtype.instMeasurableSpace MeasurableSpace.pi Real Real.measurableSpace UnitAddCircle QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm measurableEquivPiIoc	—	—
coe_symm_measurableEquivPiIoc_apply 📖	mathematical	—	DFunLike.coe MeasurableEquiv UnitAddTorus Subtype.instMeasurableSpace MeasurableSpace.pi Real Real.measurableSpace UnitAddCircle QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm measurableEquivPiIoc	—	—
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 Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id 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 mFourier SummationFilter.unconditional	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 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.instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.compactOpen ContinuousMap.instSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsSemitopologicalSemiring.toSeparatelyContinuousMul mFourierCoeff InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DFunLike.coe ContinuousMap.instFunLike mFourier SummationFilter.unconditional	—	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 instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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.toPow 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
integral_preimage 📖	mathematical	—	MeasureTheory.integral UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume Real Real.measureSpace MeasureTheory.Measure.restrict setOf AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne	—	MeasureTheory.MeasurePreserving.map_eq MeasureTheory.MeasurePreserving.symm measurePreserving_equivPiIoc MeasureTheory.integral_subtype_comap MeasurableSet.univ_pi' Finite.to_countable Finite.of_fintype measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.integral_map_equiv
lintegral_preimage 📖	mathematical	—	MeasureTheory.lintegral UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume Real Real.measureSpace MeasureTheory.Measure.restrict setOf AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne	—	MeasureTheory.MeasurePreserving.map_eq MeasureTheory.MeasurePreserving.symm measurePreserving_equivPiIoc MeasureTheory.lintegral_subtype_comap MeasurableSet.univ_pi' Finite.to_countable Finite.of_fintype measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.lintegral_map_equiv
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_eq_integral 📖	mathematical	—	mFourierCoeff MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume setOf Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField DFunLike.coe ContinuousMap UnitAddTorus Pi.topologicalSpace UnitAddCircle QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMap.instFunLike mFourier Pi.instNeg	—	integral_preimage
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 instSeparatelyContinuousAddOfContinuousAdd AddZero.toAdd SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring 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 IsSemitopologicalRing.toIsSemitopologicalSemiring ContinuousMap.instNonUnitalNonAssocRingOfIsTopologicalRing IsTopologicalRing.toIsSemitopologicalRing ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instSeparatelyContinuousAddOfContinuousAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid IsSemitopologicalSemiring.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 NonUnitalNormedRing.toNonUnitalRing NonUnitalNormedCommRing.toNonUnitalNormedRing 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 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Complex.instContinuousStar ContinuousMap.instStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Algebra.toSMul StarMul.toStarModule CommRing.toCommMonoid Complex.commRing StarRing.toStarMul mFourierSubalgebra Submodule.span ContinuousMap.instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMap.module Complex.instModuleSelf SeparatelyContinuousMul.to_continuousSMul Complex.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring 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 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
measurePreserving_equivPiIoc 📖	mathematical	—	MeasureTheory.MeasurePreserving UnitAddTorus MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi UnitAddCircle instMeasureSpaceUnitAddCircle Subtype.instMeasurableSpace MeasurableSpace.pi Real Real.measurableSpace DFunLike.coe MeasurableEquiv QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne EquivLike.toFunLike MeasurableEquiv.instEquivLike measurableEquivPiIoc MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.comap Real.measureSpace	—	MeasureTheory.MeasurePreserving.symm MeasurableEquiv.measurable symm IsEquiv.toSymm eq_isEquiv MeasureTheory.Measure.map_map measurable_pi_lambda Measurable.comp AddCircle.measurable_mk' measurable_pi_apply measurable_subtype_coe ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike AddCircle.compactSpace ENNReal.ofReal_one one_smul IsScalarTower.right MeasureTheory.Measure.restrict_pi_pi MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal map_comap_subtype_coe MeasurableSet.univ_pi' Finite.to_countable Finite.of_fintype measurableSet_Ioc BorelSpace.opensMeasurable instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.MeasurePreserving.map_eq MeasureTheory.measurePreserving_pi AddSubgroup.normal_of_comm AddCircle.instIsAddHaarMeasureRealVolume CompactSpace.sigmaCompact
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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Submodule.topologicalClosure.congr_simp Submodule.map_span Set.image_congr DenseRange.topologicalClosure_map_submodule ContinuousMap.instContinuousSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring ContinuousMap.instContinuousAddOfLocallyCompactSpace Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instSeparatelyContinuousAddOfContinuousAdd 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.module Complex.instModuleSelf SeparatelyContinuousMul.to_continuousSMul Complex.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousMap.instContinuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ContinuousMap.instContinuousAddOfLocallyCompactSpace Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instSeparatelyContinuousAddOfContinuousAdd AddZero.toAdd SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid 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	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousMap.instContinuousConstSMul ContinuousMap.instContinuousAddOfLocallyCompactSpace Function.locallyCompactSpace QuotientAddGroup.instLocallyCompactSpace instSeparatelyContinuousAddOfContinuousAdd instIsTopologicalRingReal locallyCompact_of_proper instProperSpaceReal AddCircle.compactSpace ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsTopologicalRing.toIsTopologicalSemiring Complex.instContinuousStar ContinuousMap.instStarModule StarMul.toStarModule mFourierSubalgebra_coe ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace 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	29 math math: UnitAddTorus.integral_preimage, UnitAddTorus.coe_mFourierBasis, UnitAddTorus.mFourierSubalgebra_coe, UnitAddTorus.mFourierSubalgebra_closure_eq_top, UnitAddTorus.coe_symm_measurableEquivPiIoc, UnitAddTorus.mFourierCoeff_toLp, UnitAddTorus.mFourier_add, UnitAddTorus.mFourier_zero, UnitAddTorus.coeFn_mFourierLp, UnitAddTorus.lintegral_preimage, UnitAddTorus.mFourier_neg, UnitAddTorus.measurePreserving_equivPiIoc, UnitAddTorus.mFourier_norm, UnitAddTorus.orthonormal_mFourier, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, UnitAddTorus.hasSum_mFourier_series_L2, UnitAddTorus.hasSum_mFourier_series_of_summable, UnitAddTorus.mFourierSubalgebra_separatesPoints, UnitAddTorus.coe_measurableEquivPiIoc_apply, UnitAddTorus.coe_measurableEquivPiIoc, UnitAddTorus.hasSum_prod_mFourierCoeff, UnitAddTorus.mFourierBasis_repr, UnitAddTorus.span_mFourier_closure_eq_top, UnitAddTorus.hasSum_mFourier_series_apply_of_summable, UnitAddTorus.hasSum_sq_mFourierCoeff, UnitAddTorus.mFourier_single, UnitAddTorus.mFourierCoeff_eq_integral, UnitAddTorus.span_mFourierLp_closure_eq_top, UnitAddTorus.coe_symm_measurableEquivPiIoc_apply
instMeasureSpaceUnitAddCircle 📖	CompOp	15 math math: UnitAddTorus.integral_preimage, UnitAddTorus.coe_mFourierBasis, UnitAddTorus.mFourierCoeff_toLp, UnitAddTorus.coeFn_mFourierLp, UnitAddTorus.lintegral_preimage, UnitAddTorus.measurePreserving_equivPiIoc, 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	—	—
instIsProbabilityMeasureUnitAddCircleVolume 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure UnitAddCircle MeasureTheory.MeasureSpace.toMeasurableSpace instMeasureSpaceUnitAddCircle MeasureTheory.MeasureSpace.volume	—	—

---

← Back to Index