LpSpace

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

Statistics

Metric	Count
Definitions fourierTransformₗᵢ, instFourierTransform, instFourierTransformInv	3
Theorems fourierInv_toTemperedDistribution_eq, fourier_toTemperedDistribution_eq, inner_fourier_eq, instContinuousFourier, instContinuousFourierInv, instFourierAdd, instFourierInvAdd, instFourierInvSMul, instFourierPair, instFourierPairInv, instFourierSMul, norm_fourier_eq, toLp_fourierInv_eq, toLp_fourierTransformInv_eq, toLp_fourierTransform_eq, toLp_fourier_eq	16
Total	19

MeasureTheory.Lp

Definitions

Name	Category	Theorems
fourierTransformₗᵢ 📖	CompOp	—
instFourierTransform 📖	CompOp	10 math math: instFourierPair, norm_fourier_eq, instFourierSMul, instFourierPairInv, SchwartzMap.toLp_fourierTransform_eq, inner_fourier_eq, instContinuousFourier, fourier_toTemperedDistribution_eq, SchwartzMap.toLp_fourier_eq, instFourierAdd
instFourierTransformInv 📖	CompOp	8 math math: SchwartzMap.toLp_fourierTransformInv_eq, instFourierInvSMul, SchwartzMap.toLp_fourierInv_eq, instFourierPair, instContinuousFourierInv, instFourierPairInv, instFourierInvAdd, fourierInv_toTemperedDistribution_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierInv_toTemperedDistribution_eq 📖	mathematical	—	FourierTransformInv.fourierInv TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex Complex.instRCLike TemperedDistribution.instFourierTransformInv toTemperedDistribution MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume fact_one_le_two_ennreal FourierInvPair.fourier_fourierInv_eq instFourierPairInv fourier_toTemperedDistribution_eq FourierPair.fourierInv_fourier_eq TemperedDistribution.instFourierPair
fourier_toTemperedDistribution_eq 📖	mathematical	—	FourierTransform.fourier TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex Complex.instRCLike TemperedDistribution.instFourierTransform toTemperedDistribution MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume fact_one_le_two_ennreal DenseRange.induction_on smulCommClass_self NormedSpace.toIsBoundedSMul BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real SchwartzMap.denseRange_toLpCLM ENNReal.ofNat_ne_top MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts isClosed_eq PointwiseConvergenceCLM.instT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearMap.continuous UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul RingHomCompTriple.ids TemperedDistribution.instFourierAdd TemperedDistribution.instFourierSMul TemperedDistribution.instContinuousFourier instFourierAdd instFourierSMul instContinuousFourier SMulCommClass.complexToReal toTemperedDistribution_toLp_eq TemperedDistribution.fourier_toTemperedDistributionCLM_eq toTemperedDistribution.congr_simp SchwartzMap.toLp_fourier_eq
inner_fourier_eq 📖	mathematical	—	Inner.inner Complex MeasureTheory.AEEqFun MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal Complex.instRCLike FourierTransform.fourier instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat LinearIsometryEquiv.inner_map_map fact_one_le_two_ennreal
instContinuousFourier 📖	mathematical	—	ContinuousFourier MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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 instNormedAddCommGroup fact_one_le_two_ennreal instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal LinearIsometryEquiv.continuous RingHomInvPair.ids NormedSpace.toIsBoundedSMul
instContinuousFourierInv 📖	mathematical	—	ContinuousFourierInv MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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 instNormedAddCommGroup fact_one_le_two_ennreal instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal LinearIsometryEquiv.continuous RingHomInvPair.ids NormedSpace.toIsBoundedSMul
instFourierAdd 📖	mathematical	—	FourierAdd MeasureTheory.AEEqFun MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 AddSubgroup.add instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat LinearIsometryEquiv.map_add RingHomInvPair.ids fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul
instFourierInvAdd 📖	mathematical	—	FourierInvAdd MeasureTheory.AEEqFun MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 AddSubgroup.add instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat LinearIsometryEquiv.map_add RingHomInvPair.ids fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul
instFourierInvSMul 📖	mathematical	—	FourierInvSMul Complex MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instNormedAddCommGroup fact_one_le_two_ennreal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule InnerProductSpace.toNormedSpace Complex.instRCLike NormedSpace.toIsBoundedSMul instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul LinearIsometryEquiv.map_smul RingHomInvPair.ids
instFourierPair 📖	mathematical	—	FourierPair MeasureTheory.AEEqFun MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 instFourierTransform instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat LinearIsometryEquiv.symm_apply_apply RingHomInvPair.ids fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul
instFourierPairInv 📖	mathematical	—	FourierInvPair MeasureTheory.AEEqFun MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 instFourierTransform instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat LinearIsometryEquiv.apply_symm_apply RingHomInvPair.ids fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul
instFourierSMul 📖	mathematical	—	FourierSMul Complex MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instNormedAddCommGroup fact_one_le_two_ennreal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule InnerProductSpace.toNormedSpace Complex.instRCLike NormedSpace.toIsBoundedSMul instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul LinearIsometryEquiv.map_smul
norm_fourier_eq 📖	mathematical	—	Norm.norm MeasureTheory.AEEqFun MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 instNorm FourierTransform.fourier instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat LinearIsometryEquiv.norm_map RingHomInvPair.ids fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul

SchwartzMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLp_fourierInv_eq 📖	mathematical	—	FourierTransformInv.fourierInv MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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.instFourierTransformInv toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal Complex Complex.instRCLike BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap instFourierTransformInv	—	LinearMap.extendOfNorm_eq SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal RingHomInvPair.ids denseRange_toLpCLM ENNReal.ofNat_ne_top MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume one_mul BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth toLp.congr_simp FourierInvPair.fourier_fourierInv_eq instFourierInvPair Eq.le norm_fourier_toL2_eq
toLp_fourierTransformInv_eq 📖	mathematical	—	FourierTransformInv.fourierInv MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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.instFourierTransformInv toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal Complex Complex.instRCLike BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap instFourierTransformInv	—	toLp_fourierInv_eq
toLp_fourierTransform_eq 📖	mathematical	—	FourierTransform.fourier MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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.instFourierTransform toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal Complex Complex.instRCLike BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap instFourierTransform	—	toLp_fourier_eq
toLp_fourier_eq 📖	mathematical	—	FourierTransform.fourier MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace 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.instFourierTransform toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal Complex Complex.instRCLike BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap instFourierTransform	—	LinearMap.extendOfNorm_eq SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal RingHomInvPair.ids denseRange_toLpCLM ENNReal.ofNat_ne_top MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume one_mul Eq.le BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth norm_fourier_toL2_eq

---

← Back to Index