Theorems · Theorem
FourierInvPair.fourier_fourierInv_eq
∀ {E : Type u_5} {F : Type u_6} {inst : FourierTransform F E} {inst_1 : FourierTransformInv E F}
[self : FourierInvPair E F] (f : E), FourierTransform.fourier (FourierTransformInv.fourierInv f) = f- Defined in
- Mathlib.Analysis.Fourier.Notation
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- FourierInvPair
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FourierTransform.fourierstatement · cited by 130
- FourierTransformInv.fourierInvstatement · cited by 69
- FourierTransformInvstatement and proof · cited by 25
- FourierTransformstatement and proof · cited by 23
- FourierInvPairstatement and proof · cited by 7
Cited by11
Results whose statement or proof uses this declaration.
- TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_applyproof · cited by 5
- FourierTransform.fourierEquivproof · cited by 4
- TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_boundedproof · cited by 3
- SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_applyproof · cited by 2
- SchwartzMap.fourier_convolutionproof · cited by 2
- SchwartzMap.integral_bilin_fourierInv_eqproof · cited by 2
- TemperedDistribution.fourierInv_toTemperedDistributionCLM_eqproof · cited by 1
- TemperedDistribution.fourierMultiplierCLM_constproof · cited by 1
- MeasureTheory.Lp.fourierInv_toTemperedDistribution_eqproof · cited by 1
- SchwartzMap.toLp_fourierInv_eqproof · cited by 0