Fourier.norm_fourierIntegral_le_integral_norm
theorem Fourier.norm_fourierIntegral_le_integral_norm :
β {π : Type u_1} [inst : CommRing π] [inst_1 : MeasurableSpace π] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
[inst_3 : NormedSpace β E] (e : AddChar π β₯circle) (ΞΌ : MeasureTheory.Measure π) (f : π β E) (w : π),
βFourier.fourierIntegral e ΞΌ f wβ β€ β« (x : π), βf xβ βΞΌ
This theorem states that for any commutative ring `π` equipped with a measurable space structure, and for any normed additive commutative group `E` which is also a complex vector space, the uniform norm of the Fourier transform of a function `f` from `π` to `E` is bounded by the `LΒΉ` norm of `f`. Here, the Fourier transform is defined with respect to a given additive character `e` on `π` and a measure `ΞΌ` on `π`. Specifically, for any `w` in `π`, the norm of the Fourier transform of `f` at `w` is less than or equal to the integral over `π` of the norm of `f` with respect to the measure `ΞΌ`.
More concisely: For any commutative ring `π` with a measurable space structure, any normed additive commutative group `E` that is also a complex vector space, any additive character `e` on `π`, any measure `ΞΌ` on `π`, and any function `f` from `π` to `E`, the uniform norm of the Fourier transform of `f` is bounded by the `LΒΉ` norm of `f`.
|
VectorFourier.fourierIntegral_continuous
theorem VectorFourier.fourierIntegral_continuous :
β {π : Type u_1} [inst : CommRing π] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module π V]
[inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module π W] {E : Type u_4}
[inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace β E] [inst_8 : TopologicalSpace π]
[inst_9 : TopologicalRing π] [inst_10 : TopologicalSpace V] [inst_11 : BorelSpace V]
[inst_12 : TopologicalSpace W] {e : AddChar π β₯circle} {ΞΌ : MeasureTheory.Measure V} {L : V ββ[π] W ββ[π] π}
[inst_13 : FirstCountableTopology W],
Continuous βe β
(Continuous fun p => (L p.1) p.2) β
β {f : V β E}, MeasureTheory.Integrable f ΞΌ β Continuous (VectorFourier.fourierIntegral e ΞΌ L f)
The theorem `VectorFourier.fourierIntegral_continuous` states that for any commutative ring `π`, additive group `V` that is a `π`-module, measurable space `V`, additive group `W` that is also a `π`-module, normed additive commutative group `E` which is a normed space over the complex numbers, provided the space `π`, `V`, and `W` are topological spaces with `π` being a topological ring, `V` being a Borel space, and `W` having a first countable topology, then given an additive character `e` from `π` to the unit circle in the complex plane and a measure `ΞΌ` on `V`, if the function `e` and the bilinear form `L` are continuous, then for any `L^1` integrable function `f` from `V` to `E`, the Fourier transform of `f` is a continuous function.
More concisely: Given a commutative ring π, a topological Borel space (π-module) V, a first countable topological space (π-module) W, a normed space E over complex numbers, a continuous additive character e from π to complex unit circle, a measure ΞΌ on V, a continuous bilinear form L, and an L^1(V,E) function f, the Fourier transform of f is a continuous function.
|
VectorFourier.fourier_integral_convergent_iff
theorem VectorFourier.fourier_integral_convergent_iff :
β {π : Type u_1} [inst : CommRing π] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module π V]
[inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module π W] {E : Type u_4}
[inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace β E] [inst_8 : TopologicalSpace π]
[inst_9 : TopologicalRing π] [inst_10 : TopologicalSpace V] [inst_11 : BorelSpace V]
[inst_12 : TopologicalSpace W] {e : AddChar π β₯circle} {ΞΌ : MeasureTheory.Measure V} {L : V ββ[π] W ββ[π] π},
Continuous βe β
(Continuous fun p => (L p.1) p.2) β
β {f : V β E} (w : W),
MeasureTheory.Integrable (fun v => e (-(L v) w) β’ f v) ΞΌ β MeasureTheory.Integrable f ΞΌ
This theorem, which is an alias of `VectorFourier.fourierIntegral_convergent_iff`, states that for any given `w`, the convergence of the Fourier integral is equivalent to the integrability of the function `f`. More specifically, for any types `π`, `V`, `W` and `E` with the necessary algebraic and topological structures (like being a commutative ring, an additive commutative group, a module, a measurable space, a normed additive commutative group, a normed space, a topological space, a topological ring, and a Borel space), an additive character `e` from `π` to the unit circle in complex numbers, a measure `ΞΌ`, and a linear transformation `L` from `V` to the space of linear transformations from `W` to `π`, if `e` is continuous and the function `p` maps to `L` applied to the first element of `p` and then applied to the second element of `p` is also continuous, then, for any function `f` from `V` to `E` and any `w` in `W`, the function `v` maps to `e` applied to the negation of `L v` applied to `w` scaled by `f v` is integrable with respect to the measure `ΞΌ` if and only if the function `f` is integrable with respect to the measure `ΞΌ`.
More concisely: For any measurable space `(V, ΞΌ)`, commutative ring `π`, additive commutative groups `V`, `W`, normed spaces `E` and `π^(W β π)`, an additive character `e` from `π` to the complex unit circle, a measure `ΞΌ`, a continuous linear transformation `L` from `V` to `π^(W β π)`, and a function `f : V β E`, the Fourier integral of `f` with respect to `e` and `ΞΌ` converges if and only if `f` is integrable with respect to `ΞΌ`.
|
VectorFourier.fourierIntegral_comp_add_right
theorem VectorFourier.fourierIntegral_comp_add_right :
β {π : Type u_1} [inst : CommRing π] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module π V]
[inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module π W] {E : Type u_4}
[inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace β E] [inst_8 : MeasurableAdd V] (e : AddChar π β₯circle)
(ΞΌ : MeasureTheory.Measure V) [inst_9 : ΞΌ.IsAddRightInvariant] (L : V ββ[π] W ββ[π] π) (f : V β E) (vβ : V),
VectorFourier.fourierIntegral e ΞΌ L (f β fun v => v + vβ) = fun w =>
e ((L vβ) w) β’ VectorFourier.fourierIntegral e ΞΌ L f w
The theorem `VectorFourier.fourierIntegral_comp_add_right` states that for any commutative ring `π`, any additively commutative group `V` that forms a `π`-module and is a measurable space, another additively commutative group `W` that also forms a `π`-module, and a normed additively commutative group `E` that forms a `β`-normed space, given an additive character `e` from `π` to the unit circle in `β`, a measure `ΞΌ` on `V` that is invariant under right addition, a `π`-linear map `L` from `V` to `W`-valued `π`-linear functions, a function `f` from `V` to `E`, and an element `vβ` of `V`, the Fourier integral of the function obtained by composing `f` with the function that adds `vβ` to its argument, is equal to the function that takes `w` to `e` evaluated at `(L vβ) w` times the Fourier integral of `f` at `w`. In other words, the Fourier integral transforms right-translation (addition of `vβ`) into scalar multiplication by a phase factor.
More concisely: For a commutative ring `π`, a measurable `π`-module `V` with invariant measure `ΞΌ`, `π`-linear map `L` from `V` to an `β`-normed space `W`, additive character `e` from `π` to the unit circle in `β`, and `π`-linear function `f` from `V` to `E`, the Fourier integrals of `f` and `f β (id + vβ)` are equal, where `vβ` is an element of `V`, and the latter is multiplied by `e(L vβ)`.
|
Fourier.fourierIntegral_comp_add_right
theorem Fourier.fourierIntegral_comp_add_right :
β {π : Type u_1} [inst : CommRing π] [inst_1 : MeasurableSpace π] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
[inst_3 : NormedSpace β E] [inst_4 : MeasurableAdd π] (e : AddChar π β₯circle) (ΞΌ : MeasureTheory.Measure π)
[inst_5 : ΞΌ.IsAddRightInvariant] (f : π β E) (vβ : π),
Fourier.fourierIntegral e ΞΌ (f β fun v => v + vβ) = fun w => e (vβ * w) β’ Fourier.fourierIntegral e ΞΌ f w
This theorem states that the Fourier transform, in a commutative ring with a measure space, converts right-translation into scalar multiplication by a phase factor. Specifically, for any additive character `e` from the ring to the unit circle in the complex numbers, any right-invariant measure `ΞΌ`, and any function `f` from the ring to a normed additive commutative group `E` that is also a normed space over the complex numbers, the Fourier transform of the function obtained by right-translating `f` by a scalar `vβ` in the ring is equal to the function that multiplies the Fourier transform of `f` by the phase factor `e(vβ * w)`. In mathematical terms, if $f : π \to E$ and $e : π \to \mathbb{C}$ is an additive character, then the Fourier transform of $f(v+v_0)$ is equal to $e(v_0w)f(w)$.
More concisely: For any additive character $e$ from a commutative ring to the unit circle in the complex numbers, right-translation of a function $f$ in the ring, with respect to the right-invariant measure $\mu$, in the Fourier transform domain results in scalar multiplication by the phase factor $e(v\_0w)$. In other words, $\mathcal{F}[f(v+v\_0)] = e(v\_0w)\mathcal{F}[f(w)]$, where $\mathcal{F}$ denotes the Fourier transform.
|
VectorFourier.norm_fourierIntegral_le_integral_norm
theorem VectorFourier.norm_fourierIntegral_le_integral_norm :
β {π : Type u_1} [inst : CommRing π] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module π V]
[inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module π W] {E : Type u_4}
[inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace β E] (e : AddChar π β₯circle) (ΞΌ : MeasureTheory.Measure V)
(L : V ββ[π] W ββ[π] π) (f : V β E) (w : W), βVectorFourier.fourierIntegral e ΞΌ L f wβ β€ β« (v : V), βf vβ βΞΌ
This theorem states that for any commutative ring `π`, any vector space `V` over `π` with a measurable space structure, any vector space `W` over `π`, and any normed additive commutative group `E` over the complex numbers β that also has a normed space structure, given an additive character from `π` to the unit circle in β, a measure on `V`, a linear map `L` from `V` to `W` and a function `f` from `V` to `E`, the uniform norm of the Fourier integral of `f` with respect to these structures and variables is bounded by the `LΒΉ` norm of `f`. In other words, the magnitude of the Fourier transformation of `f` is always less than or equal to the integral of the magnitude of `f`.
More concisely: For any commutative ring `π`, vector space `V` over `π` with a measurable space structure, normed additive commutative groups `V`, `W` over `π`, normed space `E` over the complex numbers β, additive character `Ο` from `π` to the unit circle in β, measure `ΞΌ` on `V`, linear map `L` from `V` to `W`, and function `f` from `V` to `E`, the uniform norm of the Fourier integral of `f` is less than or equal to the `LΒΉ` norm of `f`.
|