Theorems · Inductive type
FourierAdd
(E : Type u_5) → (F : outParam (Type u_6)) → [Add E] → [Add F] → [FourierTransform E F] → Prop
A FourierAdd is a function space on which the Fourier transform is additive.
- Defined in
- Mathlib.Analysis.Fourier.Notation
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- AddAddFourierTransform
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FourierTransformstatement · cited by 23
Cited by22
Results whose statement or proof uses this declaration.
- FourierTransform.fourierCLEstatement and proof · cited by 4
- FourierTransform.fourierCLMstatement and proof · cited by 4
- FourierTransform.fourierEquivstatement and proof · cited by 4
- FourierTransform.fourier_negstatement and proof · cited by 3
- FourierAdd.fourier_addstatement and proof · cited by 3
- FourierTransform.fourierCLE_applystatement and proof · cited by 1
- FourierTransform.fourierCLE_symm_applystatement and proof · cited by 1
- FourierTransform.fourierCLM_applystatement and proof · cited by 1
- FourierTransform.fourier_sumstatement and proof · cited by 1
- FourierTransform.fourierₗstatement and proof · cited by 1
- TemperedDistribution.fourierTransformCLMstatement · cited by 0
- TemperedDistribution.fourierTransformCLM_applystatement · cited by 0