isBigO_norm_Icc_restrict_atTop
theorem isBigO_norm_Icc_restrict_atTop :
β {E : Type u_1} [inst : NormedAddCommGroup E] {f : C(β, E)} {b : β},
0 < b β
(βf =O[Filter.atTop] fun x => |x| ^ (-b)) β
β (R S : β),
(fun x => βContinuousMap.restrict (Set.Icc (x + R) (x + S)) fβ) =O[Filter.atTop] fun x => |x| ^ (-b)
This theorem states that if a continuous function `f` from real numbers to a normed additive commutative group `E` is of order `O(x ^ (-b))` at infinity, where `b` is a positive real number, then the function that assigns to each real number `x` the norm of the restriction of `f` to the closed interval from `x + R` to `x + S` is also of order `O(x ^ (-b))` at infinity, for any real numbers `R` and `S`. In other words, if `f` grows no faster than `x ^ (-b)` as `x` approaches infinity, the same holds for the norm of the restriction of `f` to any closed interval shifted by `x`.
More concisely: If `f` is a continuous function from real numbers to a normed additive commutative group of order `O(x ^ (-b))` at infinity, then the function that maps `x` to the norm of the restriction of `f` to the closed interval from `x + R` to `x + S` is also of order `O(x ^ (-b))` at infinity for any fixed `R` and `S`.
|
Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable
theorem Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable :
β {f : β β β},
Continuous f β
β {b : β},
1 < b β
(f =O[Filter.cocompact β] fun x => |x| ^ (-b)) β
(Summable fun n => Real.fourierIntegral f βn) β
β (x : β), β' (n : β€), f (x + βn) = β' (n : β€), Real.fourierIntegral f βn * (fourier n) βx
**Poisson's summation formula** theorem states that, given a complex function `f` from real numbers to complex numbers that is continuous and decays as `|x| ^ (-b)` for some real value `b > 1`, and if the Fourier transform of `f` is summable, then for any real number `x`, the infinite sum over integers `n` of `f(x + n)` is equal to the infinite sum over integers `n` of the product of the Fourier transform of `f` at `n` and the `n`th Fourier monomial evaluated at `x`. The decay of `f` is measured with respect to the cocompact filter on real numbers, which is generated by the complements of compact sets.
More concisely: Given a continuous complex-valued function `f` on the real numbers that decays faster than `|x|^(-b)` for some `b > 1` and has a summable Fourier transform, the Poisson summation formula states that the sum of `f(x + n)` over all integers `n` equals the sum of the products of the Fourier transform of `f` at `n` and the `n`th Fourier monomial evaluated at `x`.
|
SchwartzMap.tsum_eq_tsum_fourierIntegral
theorem SchwartzMap.tsum_eq_tsum_fourierIntegral :
β (f g : SchwartzMap β β),
Real.fourierIntegral βf = βg β β (x : β), β' (n : β€), f (x + βn) = β' (n : β€), g βn * (fourier n) βx
**Poisson's Summation Formula for Schwartz Functions**: This theorem states that for any two Schwartz functions `f` and `g` (smooth complex-valued functions on the real line that rapidly decrease along with all their derivatives), if the Fourier integral of `f` is equal to `g`, then for any real number `x`, the series sum over all integers `n` of `f` evaluated at `x + n` is equal to the series sum over all integers `n` of `g` evaluated at `n` times the exponential monomial `fourier n` evaluated at `x` (where `fourier n` is a function of the form `exp(2 Ο i n x / T)` for some real `T`).
More concisely: For any Schwartz functions `f` and `g` with equal Fourier integrals, their sum of series over integer shifts equals the product of their series over integer indices and their corresponding Fourier monomials evaluated at `x`.
|
Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay
theorem Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay :
β {f : β β β},
Continuous f β
β {b : β},
1 < b β
(f =O[Filter.cocompact β] fun x => |x| ^ (-b)) β
(Real.fourierIntegral f =O[Filter.cocompact β] fun x => |x| ^ (-b)) β
β (x : β), β' (n : β€), f (x + βn) = β' (n : β€), Real.fourierIntegral f βn * (fourier n) βx
This theorem is a statement of the Poisson's summation formula in the context of Fourier analysis. Specifically, it asserts that for a continuous complex-valued function `f` on the real numbers, if both `f` and its Fourier transform decay as `|x| ^ (-b)` for some real number `b` greater than 1, then the sum of `f(x + n)` over all integer `n` equals the sum of the product of the Fourier transform of `f` at `n` and the `n`-th Fourier series component at `x`, over all integer `n`. This is a one-dimensional version of Corollary VII.2.6 from Stein and Weiss's *Introduction to Fourier Analysis on Euclidean Spaces*. The decay condition is expressed using the notion of a function being "big-O" of another with respect to the filter of complements to compact sets.
More concisely: For a continuous complex-valued function `f` on the real numbers decaying faster than `|x|^(-b)` for some `b > 1, the Poisson's summation formula states that the sum of `f(x + n)` over all integers `n` equals the sum of the product of the Fourier transform of `f` at `n` and the `n`-th Fourier series component at `x`.
|
Real.fourierCoeff_tsum_comp_add
theorem Real.fourierCoeff_tsum_comp_add :
β {f : C(β, β)},
(β (K : TopologicalSpace.Compacts β),
Summable fun n => βContinuousMap.restrict (βK) (f.comp (ContinuousMap.addRight βn))β) β
β (m : β€), fourierCoeff β―.lift m = Real.fourierIntegral βf βm
The theorem `Real.fourierCoeff_tsum_comp_add` establishes a key insight for the Poisson summation formula: it states that for every continuous function `f` mapping from the real numbers to the complex numbers, if for every compact subset `K` of the real numbers, the series sum of the norm of the restriction of the function composition of `f` and the continuous map that adds an integer `n` to its argument (restricted to the subset `K`), is summable, then for every integer `m`, the `m`-th Fourier coefficient of the periodic sum function `β' n : β€, f (x + n)` equals the value at `m` of the Fourier transform of `f`. In simpler terms, this theorem connects the Fourier coefficients of a periodic sum function with the Fourier transform of the original function.
More concisely: If a continuous real-valued function `f` has absolutely summable Fourier coefficients for its periodic sum, then the `m`-th Fourier coefficient of the periodic sum equals the `m`-th Fourier transform coefficient of `f`.
|
Real.tsum_eq_tsum_fourierIntegral
theorem Real.tsum_eq_tsum_fourierIntegral :
β {f : C(β, β)},
(β (K : TopologicalSpace.Compacts β),
Summable fun n => βContinuousMap.restrict (βK) (f.comp (ContinuousMap.addRight βn))β) β
(Summable fun n => Real.fourierIntegral βf βn) β
β (x : β), β' (n : β€), f (x + βn) = β' (n : β€), Real.fourierIntegral βf βn * (fourier n) βx
This is the most general form of **Poisson's summation formula**. For any continuous complex-valued function `f` on the real line, if for any compact subset `K` of the real line, the sum of the norms of `f` composed with the continuous map `fun y => y + n` (for `n` an integer) restricted to `K`, is summable, and if the sum of the Fourier integrals of `f` is summable, then for every real number `x`, the sum over all integers `n` of `f(x + n)` equals the sum over all integers `n` of the Fourier integral of `f` times an exponential monomial `exp(2 Ο i n x/T)`, where `T` is a period of `f`.
More concisely: If a continuous complex-valued function `f` on the real line satisfies the summability condition for translations over compact sets and the summability of its Fourier integrals, then for every real number `x`, the sum over all integers `n` of `f(x + n)` equals the sum over all integers `n` of the Fourier transform of `f` multiplied by an exponential monomial `exp(2Οinx/T)`, where `T` is a period of `f`.
|