FourierTransform

📁 Source: Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Statistics

Metric	Count
Definitions FourierTransform, verticalIntegral	2
Theorems integrable_cexp_neg_mul_sq_add_real_mul_I, integrable_cexp_neg_mul_sq_norm_add, integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, integrable_cexp_neg_mul_sum_add, integrable_cexp_neg_sum_mul_add, integral_cexp_neg_mul_sq_add_real_mul_I, integral_cexp_neg_mul_sq_norm, integral_cexp_neg_mul_sq_norm_add, integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, integral_cexp_neg_mul_sum_add, integral_cexp_neg_sum_mul_add, integral_rexp_neg_mul_sq_norm, norm_cexp_neg_mul_sq_add_mul_I, norm_cexp_neg_mul_sq_add_mul_I', tendsto_verticalIntegral, verticalIntegral_norm_le, fourierIntegral_gaussian, fourierIntegral_gaussian_innerProductSpace, fourierIntegral_gaussian_innerProductSpace', fourierIntegral_gaussian_pi, fourierIntegral_gaussian_pi', fourier_gaussian_innerProductSpace, fourier_gaussian_innerProductSpace', fourier_gaussian_pi, fourier_gaussian_pi', integrable_cexp_quadratic, integrable_cexp_quadratic', integral_cexp_quadratic	28
Total	30

GaussianFourier

Definitions

Name	Category	Theorems
verticalIntegral 📖	CompOp	2 math math: tendsto_verticalIntegral, verticalIntegral_norm_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_cexp_neg_mul_sq_add_real_mul_I 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Complex.exp Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd Complex.ofReal Complex.I MeasureTheory.MeasureSpace.volume	—	Continuous.comp_aestronglyMeasurable Continuous.cexp continuous_id' MeasureTheory.AEStronglyMeasurable.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.pow MeasureTheory.AEStronglyMeasurable.add_const IsTopologicalSemiring.toContinuousAdd Continuous.aestronglyMeasurable BorelSpace.opensMeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right secondCountable_of_proper Complex.instProperSpace Complex.continuous_ofReal MeasureTheory.hasFiniteIntegral_norm_iff norm_cexp_neg_mul_sq_add_mul_I' LT.lt.ne' neg_sub sub_eq_add_neg Real.exp_add integrable_exp_neg_mul_sq MeasureTheory.HasFiniteIntegral.const_mul MeasureTheory.Integrable.hasFiniteIntegral MeasureTheory.Integrable.comp_sub_right ContinuousAdd.measurableAdd instIsTopologicalRingReal MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real
integrable_cexp_neg_mul_sq_norm_add 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume	—	RingHomInvPair.ids fact_one_le_two_ennreal WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal MeasureTheory.MeasurePreserving.integrable_comp_emb LinearIsometryEquiv.measurePreserving Homeomorph.measurableEmbedding Finite.to_countable Nat.instAtLeastTwoHAddOfNat neg_mul LinearIsometryEquiv.norm_map LinearIsometryEquiv.inner_map_eq_flip integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace
integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing EuclideanSpace MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.innerProductSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedSpace.toModule FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm PiLp.instNorm Real.norm Inner.inner InnerProductSpace.toInner PiLp.seminormedAddCommGroup Nat.instAtLeastTwoHAddOfNat NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume	—	fact_one_le_two_ennreal WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.MeasurePreserving.integrable_comp_emb PiLp.volume_preserving_toLp MeasurableEquiv.measurableEmbedding neg_mul EuclideanSpace.norm_eq Finset.sum_congr sq_abs conj_trivial instTrivialStarReal Complex.ofReal_sum Complex.ofReal_mul Finset.mul_sum Finset.sum_neg_distrib mul_assoc Real.sq_sqrt Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE even_two_mul Complex.ofReal_pow mul_comm integrable_cexp_neg_mul_sum_add
integrable_cexp_neg_mul_sum_add 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal MeasureTheory.MeasureSpace.volume	—	neg_mul Finset.mul_sum integrable_cexp_neg_sum_mul_add
integrable_cexp_neg_sum_mul_add 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Complex.exp Complex.instAdd Complex.instNeg Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.univ Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal MeasureTheory.MeasureSpace.volume	—	Complex.exp_sum Finset.prod_congr MeasureTheory.Integrable.fintype_prod MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal add_zero integrable_cexp_quadratic
integral_cexp_neg_mul_sq_add_real_mul_I 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume Complex.exp Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd Complex.ofReal Complex.I Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instOne instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	tendsto_nhds_unique Complex.instT2Space Nat.instAtLeastTwoHAddOfNat Filter.atTop_neBot instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean MeasureTheory.intervalIntegral_tendsto_integral instIsCountablyGenerated_atTop instOrderTopologyReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal integrable_cexp_neg_mul_sq_add_real_mul_I Filter.tendsto_neg_atTop_atBot Real.instIsOrderedAddMonoid Filter.tendsto_id Complex.integral_boundary_rect_eq_zero_of_differentiableOn Differentiable.differentiableOn Differentiable.cexp Differentiable.const_mul differentiable_pow neg_zero MulZeroClass.zero_mul add_zero MulZeroClass.mul_zero mul_one tsub_zero AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono zero_add Complex.ofReal_neg intervalIntegral.integral_const_mul intervalIntegral.integral_sub Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.cexp Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_const continuous_id' Continuous.pow Continuous.fun_add IsTopologicalSemiring.toContinuousAdd Complex.continuous_ofReal Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup sq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.pow_zero mul_sub sub_eq_zero Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_constg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.term_add_termg Mathlib.Tactic.Abel.zero_termg integral_gaussian_complex Filter.Tendsto.add integrable_cexp_neg_mul_sq tendsto_verticalIntegral
integral_cexp_neg_mul_sq_norm 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Complex.exp Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instNatCast Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat neg_mul inner_zero_left MulZeroClass.mul_zero add_zero zero_pow Nat.instCharZero norm_zero zero_div Complex.exp_zero mul_one integral_cexp_neg_mul_sq_norm_add
integral_cexp_neg_mul_sq_norm_add 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm Inner.inner InnerProductSpace.toInner Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instNatCast Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	RingHomInvPair.ids fact_one_le_two_ennreal Nat.instAtLeastTwoHAddOfNat WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal MeasureTheory.MeasurePreserving.integral_comp LinearIsometryEquiv.measurePreserving Homeomorph.measurableEmbedding Finite.to_countable LinearIsometryEquiv.norm_map LinearIsometryEquiv.inner_map_eq_flip Fintype.card_fin integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace
integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.integral EuclideanSpace Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.innerProductSpace RCLike.toInnerProductSpaceReal WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedSpace.toModule FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace PiLp.borelSpace Finite.to_countable UniformSpace.toTopologicalSpace Real.borelSpace instSecondCountableTopologyReal MeasureTheory.MeasureSpace.volume Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm PiLp.instNorm Real.norm Inner.inner InnerProductSpace.toInner PiLp.seminormedAddCommGroup Nat.instAtLeastTwoHAddOfNat Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instNatCast Fintype.card	—	fact_one_le_two_ennreal WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.MeasurePreserving.integral_comp PiLp.volume_preserving_toLp MeasurableEquiv.measurableEmbedding neg_mul EuclideanSpace.norm_eq Finset.sum_congr sq_abs IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Nat.cast_zero Real.sq_sqrt Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE even_two_mul conj_trivial instTrivialStarReal Complex.ofReal_sum Complex.ofReal_mul Finset.mul_sum mul_assoc mul_comm mul_pow integral_cexp_neg_mul_sum_add
integral_cexp_neg_mul_sum_add 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace MeasureTheory.MeasureSpace.volume Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instNatCast Fintype.card instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat neg_mul Finset.mul_sum integral_cexp_neg_sum_mul_add Finset.prod_congr one_div Finset.prod_mul_distrib Finset.prod_const Finset.sum_div div_eq_mul_inv Finset.sum_congr
integral_cexp_neg_sum_mul_add 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace MeasureTheory.MeasureSpace.volume Complex.exp Complex.instAdd Complex.instNeg Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.univ Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Finset.prod CommRing.toCommMonoid Complex.commRing Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instOne instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Complex.exp_sum Finset.prod_congr MeasureTheory.integral_fintype_prod_volume_eq_prod MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_mul add_zero one_div neg_neg mul_neg div_neg sub_neg_eq_add zero_add integral_cexp_quadratic
integral_rexp_neg_mul_sq_norm 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Real.exp Real.instMul Real.instNeg Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instPow DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instNatCast Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat LinearIsometry.integral_comp_comm Complex.instCompleteSpace Real.instCompleteSpace Complex.norm_real neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow Complex.ofReal_div Complex.ofReal_cpow le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.pi_pos integral_cexp_neg_mul_sq_norm
norm_cexp_neg_mul_sq_add_mul_I 📖	mathematical	—	Norm.norm Complex Complex.instNorm Complex.exp Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd Complex.ofReal Complex.I Real.exp Real Real.instNeg Real.instSub Real.instMul Complex.re Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.im	—	Nat.instAtLeastTwoHAddOfNat Complex.norm_exp neg_mul Complex.neg_re Complex.re_add_im sq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt
norm_cexp_neg_mul_sq_add_mul_I' 📖	mathematical	—	Norm.norm Complex Complex.instNorm Complex.exp Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd Complex.ofReal Complex.I Real.exp Real Real.instNeg Real.instSub Real.instMul Complex.re Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Complex.im Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero norm_cexp_neg_mul_sq_add_mul_I
tendsto_verticalIntegral 📖	mathematical	Real Real.instLT Real.instZero Complex.re	Filter.Tendsto Complex verticalIntegral Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero	—	tendsto_zero_iff_norm_tendsto_zero tendsto_of_tendsto_of_tendsto_of_le_of_le' instOrderTopologyReal Nat.instAtLeastTwoHAddOfNat tendsto_const_nhds Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.comp Real.tendsto_exp_atBot Filter.tendsto_neg_atTop_atBot Real.instIsOrderedAddMonoid Filter.tendsto_atTop_add_const_right sq Filter.Tendsto.atTop_mul_atTop₀ Real.instIsOrderedRing Filter.tendsto_const_mul_atTop_of_pos Real.instIsStrictOrderedRing Filter.tendsto_id Filter.Eventually.of_forall norm_nonneg Filter.Eventually.mp Filter.eventually_ge_atTop verticalIntegral_norm_le
verticalIntegral_norm_le 📖	mathematical	Real Real.instLT Real.instZero Complex.re Real.instLE	Norm.norm Complex Complex.instNorm verticalIntegral Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat abs Real.lattice Real.instAddGroup Real.exp Real.instNeg Real.instSub Monoid.toNatPow Real.instMonoid Complex.im	—	Nat.instAtLeastTwoHAddOfNat norm_cexp_neg_mul_sq_add_mul_I Real.exp_monotone neg_le_neg Real.instIsOrderedAddMonoid sub_le_sub IsOrderedAddMonoid.toAddLeftMono sub_le_sub_left covariant_swap_add_of_covariant_add mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing mul_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono LE.le.trans le_abs_self abs_mul abs_nonneg le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo sq_le_sq Real.instIsStrictOrderedRing intervalIntegral.norm_integral_le_of_norm_le_const le_or_gt abs_of_nonneg abs_of_pos Set.uIoc_of_le abs_of_neg abs_of_nonpos Set.uIoc_of_ge LT.lt.le neg_le_neg_iff norm_mul NormedDivisionRing.toNormMulClass Complex.norm_I one_mul two_mul norm_sub_le add_le_add neg_mul Complex.ofReal_neg abs_neg sub_zero mul_comm le_refl

(root)

Definitions

Name	Category	Theorems
FourierTransform 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierIntegral_gaussian 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume Complex.instMul Complex.exp Complex.I Complex.ofReal Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instOne instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Complex.exp_add add_comm add_zero integral_cexp_quadratic Complex.neg_re neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_neg zero_sub mul_neg div_neg mul_pow Complex.I_sq neg_one_mul mul_comm
fourierIntegral_gaussian_innerProductSpace 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.exp Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instNatCast Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Real.instRCLike instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	fourier_gaussian_innerProductSpace
fourierIntegral_gaussian_innerProductSpace' 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.I Inner.inner InnerProductSpace.toInner Real.instRCLike Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	fourier_gaussian_innerProductSpace'
fourierIntegral_gaussian_pi 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real Complex.exp Complex.instMul Complex.instNeg Complex.ofReal Real.pi Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	fourier_gaussian_pi
fourierIntegral_gaussian_pi' 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Complex.ofReal Real.pi Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow Complex.I	—	fourier_gaussian_pi'
fourier_gaussian_innerProductSpace 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.exp Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instNatCast Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Real.instRCLike instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat neg_mul inner_zero_left MulZeroClass.mul_zero add_zero zero_sub norm_neg fourier_gaussian_innerProductSpace'
fourier_gaussian_innerProductSpace' 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.I Inner.inner InnerProductSpace.toInner Real.instRCLike Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat neg_mul Real.fourier_eq' real_inner_comm Complex.ofReal_neg Complex.ofReal_mul inner_sub_left Complex.ofReal_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Contrapose.contrapose₃ Complex.zero_re le_refl mul_pow Complex.I_sq mul_neg mul_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz GaussianFourier.integral_cexp_neg_mul_sq_norm_add
fourier_gaussian_pi 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real Complex.exp Complex.instMul Complex.instNeg Complex.ofReal Real.pi Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Real.borelSpace FiniteDimensional.rclike_to_real Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero MulZeroClass.zero_mul add_zero fourier_gaussian_pi'
fourier_gaussian_pi' 📖	mathematical	Real Real.instLT Real.instZero Complex.re	FourierTransform.fourier Real.instFourierTransform Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Complex.ofReal Real.pi Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow Complex.I	—	neg_mul Complex.re_ofReal_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.pi_pos Real.borelSpace FiniteDimensional.rclike_to_real Nat.instAtLeastTwoHAddOfNat Real.fourier_real_eq_integral_exp_smul Complex.ofReal_mul Complex.ofReal_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero integral_cexp_quadratic neg_neg div_div div_self Complex.ofReal_ne_zero Real.pi_ne_zero one_div Complex.inv_cpow Complex.arg_eq_pi_iff not_and_or not_lt LT.lt.le Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.Contrapose.contrapose₃ Complex.zero_re le_refl Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one mul_neg div_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.zpow'_ofNat neg_div Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.sub_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.RingNF.add_neg Complex.I_sq Nat.cast_one
integrable_cexp_quadratic 📖	mathematical	Real Real.instLT Real.instZero Complex.re	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Complex.exp Complex.instAdd Complex.instMul Complex.instNeg Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal MeasureTheory.MeasureSpace.volume	—	IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid integrable_cexp_quadratic'
integrable_cexp_quadratic' 📖	mathematical	Real Real.instLT Complex.re Real.instZero	MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Complex.exp Complex.instAdd Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal MeasureTheory.MeasureSpace.volume	—	Mathlib.Tactic.Contrapose.contrapose₃ Complex.zero_re le_refl Nat.instAtLeastTwoHAddOfNat MeasureTheory.integral_undef one_div NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero integral_cexp_quadratic
integral_cexp_quadratic 📖	mathematical	Real Real.instLT Complex.re Real.instZero	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume Complex.exp Complex.instAdd Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Complex.instPow DivInvMonoid.toDiv Complex.instDivInvMonoid Real.pi Complex.instNeg Complex.instOne instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instSub	—	Mathlib.Tactic.Contrapose.contrapose₃ Complex.zero_re le_refl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.zpow'_ofNat neg_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add MeasureTheory.integral_mul_const Complex.re_add_im MeasureTheory.integral_add_right_eq_self ContinuousAdd.measurableAdd Real.borelSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Complex.neg_re

---

← Back to Index