Documentation Verification Report

Notation

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

Statistics

Metric	Count
Definitions `ContinuousFourier`, `ContinuousFourierInv`, `FourierAdd`, `FourierInvAdd`, `FourierInvModule`, `toFourierTransformInv`, `FourierInvPair`, `FourierInvSMul`, `FourierModule`, `toFourierTransform`, `FourierPair`, `FourierSMul`, `fourier`, `fourierCLE`, `fourierCLM`, `fourierEquiv`, `fourierInvCLM`, `fourierInvₗ`, `fourierₗ`, `term𝓕`, `«term𝓕⁻»`, `FourierTransformInv`, `fourierInv`	23
Theorems `continuous_fourier`, `continuous_fourierInv`, `fourier_add`, `fourierInv_add`, `fourierInv_add`, `fourierInv_smul`, `fourier_fourierInv_eq`, `fourierInv_smul`, `fourier_add`, `fourier_smul`, `fourierInv_fourier_eq`, `fourier_smul`, `fourierCLE_apply`, `fourierCLE_symm_apply`, `fourierCLM_apply`, `fourierEquiv_apply`, `fourierEquiv_symm_apply`, `fourierInvCLM_apply`, `fourierInv_neg`, `fourierInv_sum`, `fourierInv_zero`, `fourierInvₗ_apply`, `fourier_neg`, `fourier_sum`, `fourier_zero`, `fourierₗ_apply`	26
Total	49

ContinuousFourier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_fourier` 📖	mathematical	—	`Continuous` `FourierTransform.fourier`	—	—

ContinuousFourierInv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_fourierInv` 📖	mathematical	—	`Continuous` `FourierTransformInv.fourierInv`	—	—

FourierAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourier_add` 📖	mathematical	—	`FourierTransform.fourier`	—	—

FourierInvAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierInv_add` 📖	mathematical	—	`FourierTransformInv.fourierInv`	—	—

FourierInvModule

Definitions

Name	Category	Theorems
`toFourierTransformInv` 📖	CompOp	2 math math: `fourierInv_add`, `fourierInv_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierInv_add` 📖	mathematical	—	`FourierTransformInv.fourierInv` `toFourierTransformInv`	—	—
`fourierInv_smul` 📖	mathematical	—	`FourierTransformInv.fourierInv` `toFourierTransformInv`	—	—

FourierInvPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourier_fourierInv_eq` 📖	mathematical	—	`FourierTransform.fourier` `FourierTransformInv.fourierInv`	—	—

FourierInvSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierInv_smul` 📖	mathematical	—	`FourierTransformInv.fourierInv`	—	—

FourierModule

Definitions

Name	Category	Theorems
`toFourierTransform` 📖	CompOp	2 math math: `fourier_smul`, `fourier_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourier_add` 📖	mathematical	—	`FourierTransform.fourier` `toFourierTransform`	—	—
`fourier_smul` 📖	mathematical	—	`FourierTransform.fourier` `toFourierTransform`	—	—

FourierPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierInv_fourier_eq` 📖	mathematical	—	`FourierTransformInv.fourierInv` `FourierTransform.fourier`	—	—

FourierSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourier_smul` 📖	mathematical	—	`FourierTransform.fourier`	—	—

FourierTransform

Definitions

Name	Category	Theorems
`fourier` 📖	CompOp	118 math math: `Real.hasDerivAt_fourier`, `Real.fourierInv_eq_fourier_neg`, `mellin_eq_fourier`, `SchwartzMap.integral_sesq_fourier_fourier`, `Real.fourierCoeff_tsum_comp_add`, `Real.fourierIntegral_comp_linearIsometry`, `Real.fderiv_fourierIntegral`, `SchwartzMap.inner_fourier_toL2_eq`, `Real.fourierIntegral_eq`, `Real.fourier_continuousLinearMap_apply`, `SchwartzMap.lineDerivOp_fourier_eq`, `TemperedDistribution.lineDerivOp_fourier_eq`, `fourierIntegral_gaussian_innerProductSpace'`, `fourier_gaussian_pi'`, `Real.fourier_real_eq_integral_exp_smul`, `Real.fourier_deriv`, `fourierEquiv_apply`, `fourier_sum`, `SchwartzMap.integral_bilin_fourierIntegral_eq`, `fourier_gaussian_innerProductSpace`, `Real.fourierIntegral_continuousMultilinearMap_apply`, `SchwartzMap.integral_sesq_fourier_eq`, `Real.fderiv_fourier`, `SchwartzMap.fourier_lineDerivOp_eq`, `Real.fourier_iteratedFDeriv`, `FourierSMul.fourier_smul`, `SchwartzMap.integral_norm_sq_fourier`, `fourierIntegral_gaussian_pi`, `Real.fourierIntegralInv_eq_fourierIntegral_neg`, `Real.fourierIntegral_continuousLinearMap_apply`, `SchwartzMap.norm_fourier_toL2_eq`, `FourierPair.fourierInv_fourier_eq`, `fourier_gaussian_innerProductSpace'`, `Real.fourier_real_eq`, `Real.hasFDerivAt_fourier`, `Real.fourier_comp_linearIsometry`, `SchwartzMap.norm_fourierTransformCLM_toL2_eq`, `Real.fourier_mul_convolution_eq`, `Real.differentiable_fourierIntegral`, `Real.fourierIntegral_iteratedDeriv`, `TemperedDistribution.fourier_toTemperedDistributionCLM_eq`, `SchwartzMap.fourier_inversion`, `Real.pow_mul_norm_iteratedFDeriv_fourier_le`, `Real.zero_at_infty_fourierIntegral`, `SchwartzMap.integral_bilin_fourier_eq`, `SchwartzMap.fourierInv_apply_eq`, `Real.fourierIntegral_real_eq_integral_exp_smul`, `Real.deriv_fourierIntegral`, `MeasureTheory.Lp.norm_fourier_eq`, `fourierCLE_apply`, `SchwartzMap.fourierTransformCLE_apply`, `Real.contDiff_fourierIntegral`, `Real.fourier_fderiv`, `fourierₗ_apply`, `Real.fourier_eq`, `SchwartzMap.fourier_evalCLM_eq`, `TemperedDistribution.fourier_lineDerivOp_eq`, `TemperedDistribution.fourier_delta_zero`, `Real.fourier_iteratedDeriv`, `Real.fourierInv_eq_fourier_comp_neg`, `FourierInvPair.fourier_fourierInv_eq`, `Real.fourier_bilin_convolution_eq`, `Real.fourierIntegralInv_comm`, `mellin_eq_fourierIntegral`, `SchwartzMap.integral_sesq_fourierIntegral_eq`, `Real.fourierIntegral_eq'`, `Real.contDiff_fourier`, `fourierIntegral_gaussian_innerProductSpace`, `Real.iteratedDeriv_fourier`, `TemperedDistribution.fourierTransform_apply`, `Real.fourierIntegral_fderiv`, `SchwartzMap.inner_fourierTransformCLM_toL2_eq`, `Real.zero_at_infty_fourier`, `Real.iteratedFDeriv_fourier`, `SchwartzMap.integral_fourier_mul_eq`, `Real.hasFDerivAt_fourierIntegral`, `SchwartzMap.fourier_coe`, `Real.fourier_bilin_convolution_eq_integral`, `Real.fourierIntegralInv_eq_fourierIntegral_comp_neg`, `FourierAdd.fourier_add`, `SchwartzMap.toLp_fourierTransform_eq`, `SchwartzMap.fourierTransformCLM_apply`, `TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq`, `SchwartzMap.fderivCLM_fourier_eq`, `Real.pow_mul_norm_iteratedFDeriv_fourierIntegral_le`, `TemperedDistribution.fourierTransformCLM_apply`, `Real.fourierInv_comm`, `MeasureTheory.Lp.inner_fourier_eq`, `ContinuousFourier.continuous_fourier`, `SchwartzMap.integral_fourier_smul_eq`, `Real.iteratedFDeriv_fourierIntegral`, `fourier_zero`, `FourierModule.fourier_smul`, `Real.fourier_continuousMultilinearMap_apply`, `SchwartzMap.integral_inner_fourier_fourier`, `SchwartzMap.fourier_fderivCLM_eq`, `SchwartzMap.fourier_convolution_apply`, `Real.iteratedDeriv_fourierIntegral`, `FourierModule.fourier_add`, `fourier_neg`, `TemperedDistribution.fourier_apply`, `Real.hasDerivAt_fourierIntegral`, `SchwartzMap.tsum_eq_tsum_fourierIntegral`, `Real.fourierIntegral_deriv`, `Real.fourierIntegral_real_eq`, `SchwartzMap.fourier_convolution`, `fourierCLM_apply`, `MeasureTheory.Lp.fourier_toTemperedDistribution_eq`, `SchwartzMap.toLp_fourier_eq`, `Real.fourier_eq'`, `Real.differentiable_fourier`, `Real.fourierIntegral_iteratedFDeriv`, `fourier_gaussian_pi`, `Real.fourier_smul_convolution_eq`, `Real.deriv_fourier`, `SchwartzMap.fourier_inversion_inv`, `fourierIntegral_gaussian_pi'`, `SchwartzMap.tsum_eq_tsum_fourier`
`fourierCLE` 📖	CompOp	4 math math: `fourierCLE_apply`, `SchwartzMap.fourierTransformCLE_apply`, `SchwartzMap.fourierTransformCLE_symm_apply`, `fourierCLE_symm_apply`
`fourierCLM` 📖	CompOp	2 math math: `TemperedDistribution.fourierTransformCLM_apply`, `fourierCLM_apply`
`fourierEquiv` 📖	CompOp	2 math math: `fourierEquiv_apply`, `fourierEquiv_symm_apply`
`fourierInvCLM` 📖	CompOp	2 math math: `fourierInvCLM_apply`, `TemperedDistribution.fourierTransformInvCLM_apply`
`fourierInvₗ` 📖	CompOp	1 math math: `fourierInvₗ_apply`
`fourierₗ` 📖	CompOp	1 math math: `fourierₗ_apply`
`term𝓕` 📖	CompOp	—
`«term𝓕⁻»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierCLE_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `fourierCLE` `fourier`	—	`RingHomInvPair.ids`
`fourierCLE_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `fourierCLE` `FourierTransformInv.fourierInv`	—	`RingHomInvPair.ids`
`fourierCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `fourierCLM` `fourier`	—	—
`fourierEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `fourierEquiv` `fourier`	—	`RingHomInvPair.ids`
`fourierEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `fourierEquiv` `FourierTransformInv.fourierInv`	—	`RingHomInvPair.ids`
`fourierInvCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `fourierInvCLM` `FourierTransformInv.fourierInv`	—	—
`fourierInv_neg` 📖	mathematical	—	`FourierTransformInv.fourierInv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass` `FourierInvAdd.fourierInv_add`
`fourierInv_sum` 📖	mathematical	—	`FourierTransformInv.fourierInv` `Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass` `FourierInvAdd.fourierInv_add`
`fourierInv_zero` 📖	mathematical	—	`FourierTransformInv.fourierInv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `FourierInvAdd.fourierInv_add`
`fourierInvₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `fourierInvₗ` `FourierTransformInv.fourierInv`	—	—
`fourier_neg` 📖	mathematical	—	`fourier` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass` `FourierAdd.fourier_add`
`fourier_sum` 📖	mathematical	—	`fourier` `Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass` `FourierAdd.fourier_add`
`fourier_zero` 📖	mathematical	—	`fourier` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `FourierAdd.fourier_add`
`fourierₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `fourierₗ` `fourier`	—	—

FourierTransformInv

Definitions

Name	Category	Theorems
`fourierInv` 📖	CompOp	59 math math: `TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq`, `Real.fourierInv_eq_fourier_neg`, `SchwartzMap.toLp_fourierTransformInv_eq`, `Real.fourierIntegralInv_eq'`, `MeasureTheory.Integrable.fourierInv_fourier_eq`, `SchwartzMap.integral_bilin_fourierInv_eq`, `SchwartzMap.integral_fourierInv_smul_eq`, `SchwartzMap.toLp_fourierInv_eq`, `FourierTransform.fourierInv_sum`, `SchwartzMap.integral_sesq_fourier_eq`, `TemperedDistribution.fourierInv_lineDerivOp_eq`, `Real.fourierIntegralInv_eq_fourierIntegral_neg`, `mellinInv_eq_fourierIntegralInv`, `Real.fourierIntegralInv_comp_linearIsometry`, `FourierPair.fourierInv_fourier_eq`, `mellinInv_eq_fourierInv`, `FourierTransform.fourierInvCLM_apply`, `FourierTransform.fourierInv_neg`, `Real.fourierInv_comp_linearIsometry`, `SchwartzMap.fourier_inversion`, `TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq`, `SchwartzMap.fourierInv_apply_eq`, `FourierInvAdd.fourierInv_add`, `Continuous.fourierInv_fourier_eq`, `FourierTransform.fourierInvₗ_apply`, `FourierTransform.fourierEquiv_symm_apply`, `SchwartzMap.fourierInv_lineDerivOp_eq`, `ContinuousFourierInv.continuous_fourierInv`, `Real.fourierInv_eq_fourier_comp_neg`, `FourierInvPair.fourier_fourierInv_eq`, `FourierInvModule.fourierInv_add`, `Real.fourierIntegralInv_comm`, `SchwartzMap.integral_sesq_fourierIntegral_eq`, `SchwartzMap.fourierTransformCLE_symm_apply`, `SchwartzMap.lineDerivOp_fourierInv_eq`, `SchwartzMap.fourierInv_coe`, `Real.fourierIntegralInv_eq_fourierIntegral_comp_neg`, `MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq`, `FourierInvSMul.fourierInv_smul`, `TemperedDistribution.fourierInv_apply`, `Continuous.fourier_inversion_inv`, `Real.fourierInv_comm`, `MeasureTheory.Integrable.fourier_inversion`, `SchwartzMap.integral_fourierInv_mul_eq`, `FourierTransform.fourierCLE_symm_apply`, `Continuous.fourier_inversion`, `Real.tendsto_integral_gaussian_smul`, `MeasureTheory.Integrable.fourier_inversion_inv`, `Continuous.fourier_fourierInv_eq`, `TemperedDistribution.lineDerivOp_fourierInv_eq`, `FourierTransform.fourierInv_zero`, `Real.fourierInv_eq`, `TemperedDistribution.fourierTransformInv_apply`, `Real.fourierInv_eq'`, `Real.fourierIntegralInv_eq`, `TemperedDistribution.fourierTransformInvCLM_apply`, `FourierInvModule.fourierInv_smul`, `SchwartzMap.fourier_inversion_inv`, `MeasureTheory.Integrable.fourier_fourierInv_eq`

(root)

Definitions

Name	Category	Theorems
`ContinuousFourier` 📖	CompData	3 math math: `TemperedDistribution.instContinuousFourier`, `SchwartzMap.instContinuousFourier`, `MeasureTheory.Lp.instContinuousFourier`
`ContinuousFourierInv` 📖	CompData	3 math math: `SchwartzMap.instContinuousFourierInv`, `MeasureTheory.Lp.instContinuousFourierInv`, `TemperedDistribution.instContinuousFourierInv`
`FourierAdd` 📖	CompData	3 math math: `TemperedDistribution.instFourierAdd`, `SchwartzMap.instFourierAdd`, `MeasureTheory.Lp.instFourierAdd`
`FourierInvAdd` 📖	CompData	3 math math: `MeasureTheory.Lp.instFourierInvAdd`, `TemperedDistribution.instFourierInvAdd`, `SchwartzMap.instFourierInvAdd`
`FourierInvModule` 📖	CompData	—
`FourierInvPair` 📖	CompData	3 math math: `TemperedDistribution.instFourierPairInv`, `MeasureTheory.Lp.instFourierPairInv`, `SchwartzMap.instFourierInvPair`
`FourierInvSMul` 📖	CompData	3 math math: `MeasureTheory.Lp.instFourierInvSMul`, `TemperedDistribution.instFourierInvSMul`, `SchwartzMap.instFourierInvSMul`
`FourierModule` 📖	CompData	—
`FourierPair` 📖	CompData	3 math math: `TemperedDistribution.instFourierPair`, `SchwartzMap.instFourierPair`, `MeasureTheory.Lp.instFourierPair`
`FourierSMul` 📖	CompData	3 math math: `TemperedDistribution.instFourierSMul`, `MeasureTheory.Lp.instFourierSMul`, `SchwartzMap.instFourierSMul`
`FourierTransformInv` 📖	CompData	—

---

← Back to Index