fourierCoeffOn_eq_integral
theorem fourierCoeffOn_eq_integral :
∀ {E : Type} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b),
fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
This theorem states that for any function `f` mapping real numbers to a normed space `E`, and for any integers `n`, the Fourier coefficient of `f` on an interval `[a, b]` (where `a` is less than `b`) is equal to `(1 / (b - a))` times the integral from `a` to `b` of the exponential monomial (associated with `-n`) evaluated at `x` times `f(x)`. This essentially relates the Fourier coefficient of a function on an interval to a weighted integral involving Fourier series components.
More concisely: For any function `f` from real numbers to a normed space `E`, and for any integer `n` and interval `[a, b]` with `a < b`, the Fourier coefficient of `f` on `[a, b]` is equal to `(1 / (b - a)) * ∫[a, b] (e^(-i * n * x) * f(x) dx)`, where `∫` denotes integration.
|
hasSum_fourier_series_of_summable
theorem hasSum_fourier_series_of_summable :
∀ {T : ℝ} [hT : Fact (0 < T)] {f : C(AddCircle T, ℂ)},
Summable (fourierCoeff ⇑f) → HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f
This theorem states that if the sequence of Fourier coefficients of a continuous function `f` from the additive circle `AddCircle T` to the complex numbers is summable, then the Fourier series of `f` converges uniformly to `f`. Here, `T` is a real number greater than zero, `fourierCoeff ⇑f` represents the Fourier coefficients of `f`, and `Summable` implies the existence of a finite sum for the sequence of Fourier coefficients. The function `fourier i` represents the `i-th` exponential monomial, and `HasSum` means the infinite sum of the product of the Fourier coefficients and the exponential monomials is equal to `f`.
More concisely: If the sequence of Fourier coefficients of a continuous `f : AddCircle T → ℂ` is summable, then the Fourier series of `f` uniformly converges to `f`.
|
fourier_coe_apply
theorem fourier_coe_apply : ∀ {T : ℝ} {n : ℤ} {x : ℝ}, (fourier n) ↑x = (2 * ↑Real.pi * Complex.I * ↑n * ↑x / ↑T).exp
This theorem states that for any real number `T` and integer `n`, and any real number `x`, the Fourier series function at `n` evaluated at `x` equals the complex exponential function where the exponent is `2 * pi * i * n * x / T`. Here, `pi` is the mathematical constant Pi, `i` denotes the imaginary unit in complex numbers, and the exponential function is defined through its Taylor series. The division and multiplication operations in the exponent are done in real numbers space, and then the result is coerced to a complex number.
More concisely: The Fourier series coefficient of order `n` for a real-valued function `f` defined on the interval `[0, T]` is equal to `(1 / (T * sqrt(2 * pi)) * ( integrate (f (x) * cos (pi * n * x / T) dw x) from 0 to T) + I * ( integrate (f (x) * sin (pi * n * x / T) dw x) from 0 to T)`, where `I` is the imaginary unit, and the integrals are evaluated as complex numbers using the Cauchy principal value.
This statement is equivalent to the one you provided, but it's more common to express Fourier series coefficients in this form rather than in terms of complex exponentials.
If you want to express the theorem in terms of complex exponentials, then the statement would be:
The value of the Fourier series of a real-valued function `f` defined on the interval `[0, T]` at a point `x` is equal to `(1 / T) * sum (from i in nat, i >= 0) ( (coeff (i) * cos (2 * pi * i * x / T) + coeff'(i) * sin (2 * pi * i * x / T) )`, where `coeff(i)` and `coeff'(i)` are the Fourier coefficients of `f` and its first derivative, respectively.
The complex exponential form of the Fourier series can be derived from the trigonometric form using Euler's formula, which states that `cos(theta) = Re(exp(I * theta))` and `sin(theta) = Im(exp(I * theta))`, where `Re` and `Im` denote the real and imaginary parts of a complex number, and `I` is the imaginary unit.
|
fourier_apply
theorem fourier_apply : ∀ {T : ℝ} {n : ℤ} {x : AddCircle T}, (fourier n) x = ↑(n • x).toCircle
The theorem `fourier_apply` states that for any real number `T`, any integer `n` and any element `x` from the additive circle defined by `T`, the application of the `n`-th Fourier monomial to `x` is equal to the canonical map applied to the `n`-fold multiple of `x` in the additive circle defined by `T`. In mathematical terms, this states that for every point on the additive circle, its projection onto the complex plane under the Fourier transform corresponds to its projection under the canonical map.
More concisely: For any real number T, integer n, and additive circle element x, the n-th Fourier monomial applied to x equals the canonical map of the n-fold multiplication of x in the additive circle T.
|
fourierCoeff_eq_intervalIntegral
theorem fourierCoeff_eq_intervalIntegral :
∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
(f : AddCircle T → E) (n : ℤ) (a : ℝ),
fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x
The theorem `fourierCoeff_eq_intervalIntegral` states that for any real number `T` greater than 0, any complete normed complex vector space `E`, any function `f` on the additive circle `AddCircle T`, any integer `n`, and any real number `a`, the `n`-th Fourier coefficient of `f` can be computed as an integral over the interval `[a, a + T]`. Specifically, it is equal to `1/T` times the integral from `a` to `a + T` of `fourier (-n)` applied to `x` scaled by `f` applied to `x`. Here, `fourier (-n)` is the exponential monomial function defined as `exp (2 π i n x / T)`.
More concisely: For any real number T > 0, complete normed complex vector space E, function f on AddCircle T, integer n, and real number a, the n-th Fourier coefficient of f is equal to 1/T * ∫[a, a+T] (fourier (-n) x) dx, where fourier (-n) is the exponential monomial function exp (2πi n x/T).
|
fourier_zero
theorem fourier_zero : ∀ {T : ℝ} {x : AddCircle T}, (fourier 0) x = 1
The `fourier_zero` theorem states that, for any real number `T` and any point `x` on the additive circle `AddCircle T`, the Fourier series at the zeroth term, i.e., `(fourier 0)`, evaluates to 1. In other words, the zeroth Fourier monomial, which can be considered as an exponential function of the form `exp (2 π i n x / T)`, is equal to 1 for all `x` in the additive circle. This can be understood as a mathematical statement: "For every real number T and for every x in the quotient space of R by the integer multiples of T (denoted as AddCircle T), the value of the Fourier series at the zero'th coefficient is always 1."
More concisely: For any real number T and every x in the additive circle T, the zeroth Fourier coefficient's corresponding term in the Fourier series equals 1.
|
has_pointwise_sum_fourier_series_of_summable
theorem has_pointwise_sum_fourier_series_of_summable :
∀ {T : ℝ} [hT : Fact (0 < T)] {f : C(AddCircle T, ℂ)},
Summable (fourierCoeff ⇑f) → ∀ (x : AddCircle T), HasSum (fun i => fourierCoeff (⇑f) i • (fourier i) x) (f x)
This theorem states that for any real number `T` greater than zero and any continuous function `f` from the additive circle of `T` to the complex numbers (`C(AddCircle T, ℂ)`), if the sequence of Fourier coefficients of `f` is summable (meaning that the infinite sum of the Fourier coefficients exists), then the Fourier series of `f` converges pointwise to `f` everywhere. This is to say, for every point `x` in the additive circle of `T`, the sum of the terms `fourierCoeff (⇑f) i • (fourier i) x` (which represent the Fourier series of `f`) is equal to the function value `f x` at that point.
More concisely: If a continuous real-valued function `f` on the circle of radius `T` with Fourier coefficients that are summable converges pointwise to `f` as the order `i` goes to infinity, then the Fourier series of `f` equals `f` everywhere on the circle.
|
hasSum_fourier_series_L2
theorem hasSum_fourier_series_L2 :
∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)),
HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
The theorem `hasSum_fourier_series_L2` states that for any real number `T` greater than 0, and for any function `f` in the L² space of `AddCircle T` (a space of square-integrable functions on the additive circle with respect to the Haar measure), the series formed by the weighted sum of the `i`-th Fourier coefficient of `f` and the `i`-th monomial `fourierLp 2 i` (considered as elements in the L² space) converges to `f`. In other words, it is stating the completeness of the L² space with respect to Fourier series: any function in the L² space can be represented as a sum of its Fourier series.
More concisely: For any `T > 0` and `f` in the L² space of `AddCircle T`, the Fourier series of `f`, i.e., the sum of the weighted Fourier coefficients and their corresponding monomials, converges to `f` in the L² norm.
|
fourierBasis_repr
theorem fourierBasis_repr :
∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (i : ℤ),
↑(fourierBasis.repr f) i = fourierCoeff (↑↑f) i
This theorem states that under the isometric isomorphism `fourierBasis`, which maps the complex Hilbert space `$L^2$` measured with the Haar measure on the additive circle to the sequence space `$\ell^2(\mathbb{Z}, \mathbb{C})$, the `$i$`-th coefficient is equal to the `$i$`-th Fourier coefficient of the function `$f$`. This Fourier coefficient is computed as the integral over the additive circle of the product of the `$i$`-th Fourier basis element and the function `$f$`, with respect to the normalized Haar measure.
More concisely: Under the isometric isomorphism `fourierBasis`, the `$i$-th coefficient of a function `$f$` in `$L^2$` with respect to the Fourier basis equals the `$i$-th Fourier coefficient of `$f$`, computed as the integral of the product of `$f$` and the `$i$-th Fourier basis element with respect to the normalized Haar measure on the additive circle.
|
tsum_sq_fourierCoeff
theorem tsum_sq_fourierCoeff :
∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)),
∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle
This is the statement of Parseval's identity for the additive circle. Given a function `f` that belongs to the `L²` space (defined over the additive circle `AddCircle T` with the Haar measure), the theorem states that the sum of the squares of the norms of the Fourier coefficients of `f` equals the `L²` norm of `f` itself. In other words, the total energy in the frequency domain (the sum of the squares of the Fourier coefficients) equals the total energy in the time domain (the `L²` norm of the function), for an `L²` function defined on the additive circle.
More concisely: The sum of the squares of the Fourier coefficients of an `L²` function `f` on the additive circle equals the `L²` norm of `f` squared.
|
fourierSubalgebra_separatesPoints
theorem fourierSubalgebra_separatesPoints : ∀ {T : ℝ} [hT : Fact (0 < T)], fourierSubalgebra.SeparatesPoints
The theorem `fourierSubalgebra_separatesPoints` states that for any real number `T` that is greater than zero, the subalgebra of `C(AddCircle T, ℂ)` that is generated by the `fourier n` function (where `n` is an integer) separates points. Separation of points is a property in functional analysis which intuitively means that distinct points can be mapped to distinct values. Here, it is stating that within the context of an algebra of complex-valued continuous functions on the additive circle of `T`, the Fourier functions form a subalgebra that uniquely identifies every point.
More concisely: For any positive real number T, the subalgebra of C(AddCircle T, ℂ) generated by the Fourier functions separates distinct points on AddCircle T.
|
span_fourier_closure_eq_top
theorem span_fourier_closure_eq_top :
∀ {T : ℝ} [hT : Fact (0 < T)], (Submodule.span ℂ (Set.range fourier)).topologicalClosure = ⊤
This theorem states that for any real number `T` greater than zero, the linear span of the monomial functions `fourier n` (which are parametrized by `n` in the set of integers and are considered as continuous functions from the additive circle `ℝ / ℤ • T` to the complex numbers `ℂ`) is dense in the space of all continuous functions from `ℝ / ℤ • T` to `ℂ`. In other words, for every continuous function on this circle to the complex numbers, there is a sequence of linear combinations of these monomial functions that converges to that function.
More concisely: For any continuous function from the circle `ℝ / ℤ • T` to the complex numbers, there exists a sequence of linear combinations of Fourier monomial functions that converges to it.
|
fourierSubalgebra_closure_eq_top
theorem fourierSubalgebra_closure_eq_top : ∀ {T : ℝ} [hT : Fact (0 < T)], fourierSubalgebra.topologicalClosure = ⊤ := by
sorry
This theorem states that for any real number `T` greater than zero, the closure of the subalgebra of the set of continuous complex-valued functions on the additive circle of `T` generated by the Fourier series `fourier n` for every integer `n`, is dense. In other words, every element of the set of continuous complex-valued functions on the additive circle of `T` can be approximated arbitrarily closely by a linear combination of terms of the Fourier series `fourier n`.
More concisely: The closure of the subalgebra generated by the Fourier series of continuous complex-valued functions on the additive circle of a positive real number `T` is dense in the set of all continuous complex-valued functions on that circle.
|
span_fourierLp_closure_eq_top
theorem span_fourierLp_closure_eq_top :
∀ {T : ℝ} [hT : Fact (0 < T)] {p : ENNReal} [inst : Fact (1 ≤ p)],
p ≠ ⊤ → (Submodule.span ℂ (Set.range (fourierLp p))).topologicalClosure = ⊤
The theorem `span_fourierLp_closure_eq_top` states that for every real number `T` where `T` is greater than zero and every extended nonnegative real number `p`, such that `1` is less than or equal to `p` and `p` is less than infinity, the topological closure of the linear span of the set of all monomials `fourier n` in the complex `Lp` space with respect to the Haar measure on the additive circle equals the whole `Lp` space. In other words, this theorem is asserting that the monomials `fourier n` are dense in the `Lp` space for each `1 ≤ p < ∞`.
More concisely: For every real number T > 0 and extended real number p with 1 ≤ p < ∞, the linear span of the Fourier monomials is dense in the Lp space with respect to the Haar measure on the additive circle.
|
coe_fourierBasis
theorem coe_fourierBasis :
∀ {T : ℝ} [hT : Fact (0 < T)], (fun i => fourierBasis.repr.symm (lp.single 2 i 1)) = fourierLp 2
This theorem states that for all real numbers `T` greater than zero, the elements of the Hilbert basis `fourierBasis` are equivalent to the functions `fourierLp 2`. In other words, the functions `fourierLp 2`, which represent the monomials `fourier n` on the circle considered as elements of the `L²` space (the space of square-integrable functions), can be obtained from the Hilbert basis `fourierBasis` by applying the inverse of its representation function (`repr.symm`) to the single point masses at each integer index (`lp.single 2 i 1`).
More concisely: For all real numbers T > 0, the functions `fourierLp 2` on the circle are equal to the images of single point masses at integer indices under the inverse representation function of the Hilbert basis `fourierBasis`.
|
fourierSubalgebra_coe
theorem fourierSubalgebra_coe :
∀ {T : ℝ}, Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = Submodule.span ℂ (Set.range fourier)
The theorem `fourierSubalgebra_coe` states that for any real number `T`, the star subalgebra of the set of continuous complex-valued functions on the circle group `AddCircle T` generated by the Fourier functions `fourier n` for `n` in the set of integers, when viewed as a submodule, is identical to the smallest submodule (known as the linear span) of these functions. This means that the set of all possible linear combinations of these Fourier functions forms the same space when considered as a subalgebra or as a submodule.
More concisely: The star subalgebra of the Fourier functions on the circle group generated by the Fourier series coefficients is equal to their linear span.
|
fourierCoeffOn_of_hasDerivAt
theorem fourierCoeffOn_of_hasDerivAt :
∀ {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ},
n ≠ 0 →
(∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
IntervalIntegrable f' MeasureTheory.volume a b →
fourierCoeffOn hab f n =
1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
This theorem states that for any two real numbers `a` and `b` where `a < b`, and any function `f` with derivative `f'` mapping real numbers to complex numbers, and any integer `n` that is not equal to zero, if at all points in the closed interval between `a` and `b`, `f` has derivative `f'` at `x`, and `f'` is interval-integrable with respect to the Lebesgue measure on the interval `a..b`, then the Fourier coefficient of `f` on the interval `a, b` is equal to `1 / (-2 * π * i * n)` times the sum of the Fourier series of `-n` at `a` multiplied by the difference of `f` at `b` and `a`, and the difference of `b` and `a` multiplied by the Fourier coefficient of `f'` on the interval `a, b` at `n`. This relates the Fourier coefficients of a function on an interval to those of its derivative.
More concisely: For real numbers `a` < `b`, function `f` with derivative `f'` mapping real numbers to complex numbers, and integer `n ≠ 0`, if `f'` is interval-integrable on `[a, b]` and `f'` has derivative `f''` at every point in `[a, b]`, then the Fourier coefficient of `f` at `n` is equal to `1 / (-2 * π * i * n) * ( (-f'(b) + (-f'(a)) * (b - a) : complex) + (n * (f(b) - f(a)) : complex) * FourierCoefficientOf(f'')(n))`.
|
fourier_add_half_inv_index
theorem fourier_add_half_inv_index :
∀ {T : ℝ} {n : ℤ}, n ≠ 0 → 0 < T → ∀ (x : AddCircle T), (fourier n) (x + ↑(T / 2 / ↑n)) = -(fourier n) x
The theorem `fourier_add_half_inv_index` states that for any real number `T` that is greater than `0` and any integer `n` that is not equal to `0`, and for any point `x` on the additive circle `AddCircle T`, if we translate `x` by the amount `T / 2 / n` on the additive circle, the value of the `n`-th Fourier function at the translated point is equal to the negation of the value of the `n`-th Fourier function at the original point. In other words, translating the input of the `n`-th Fourier function by `T / 2 / n` negates the function, given `n` is not equal to `0`.
More concisely: For any real number T > 0 and integer n ≠ 0, translating a point x on the additive circle by T / 2 / n negates the value of the n-th Fourier function.
|
orthonormal_fourier
theorem orthonormal_fourier : ∀ {T : ℝ} [hT : Fact (0 < T)], Orthonormal ℂ (fourierLp 2)
The theorem `orthonormal_fourier` states that for all real numbers `T` such that `T` is greater than 0, the monomials defined by the function `fourier n` form an orthonormal set with respect to the normalised Haar measure. Here, orthonormality is defined in the context of an inner product space: each monomial has a norm equal to 1, and the inner product of any two distinct monomials is zero. The monomials are considered as elements of the `Lp` space of functions from the additive group circle to the complex numbers, where `p` equals 2.
More concisely: For all positive real numbers T, the Fourier monomials defined by the function `fourier` form an orthonormal set with respect to the normalized Haar measure in the L2 space of functions from the additive group circle to the complex numbers.
|