Fourier
Results named in Tau Ceti's TauCeti.Analysis.Fourier modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremBrown–Halmos theorem#
A bounded operator T on Hardy space is a Toeplitz operator T_a
for a unique essentially bounded symbol a if and only if S† T S = T, where S = T_z is the
forward shift.
TauCeti.existsUnique_toeplitz_eq_iff_adjoint_comp_comp_eq
(T : TauCeti.HardySpace →L[ℂ] TauCeti.HardySpace) :
(∃! a, TauCeti.toeplitz a = T) ↔
ContinuousLinearMap.adjoint (TauCeti.toeplitz (fourierLp ⊤ 1)) ∘SL
T ∘SL TauCeti.toeplitz (fourierLp ⊤ 1) =
T
Lean
Formalized in Tau Ceti as TauCeti.existsUnique_toeplitz_eq_iff_adjoint_comp_comp_eq.
Sources
TheoremClassical Toeplitz product identity#
The product defect is minus the product of the classical Hankel operator of the left symbol and that of the reflected right symbol.
TauCeti.toeplitz_comp_sub_toeplitz_eq_neg_classicalHankel_comp_classicalHankel
(a b : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) :
TauCeti.toeplitz a ∘SL TauCeti.toeplitz b - TauCeti.toeplitz (a * b) =
-TauCeti.classicalHankel a ∘SL
TauCeti.classicalHankel ((MeasureTheory.Lp.compMeasurePreserving (fun t => -t) ⋯) b)
Lean
Formalized in Tau Ceti as TauCeti.toeplitz_comp_sub_toeplitz_eq_neg_classicalHankel_comp_classicalHankel.
Sources
TheoremCoburn's alternative#
For a nonzero essentially bounded symbol a, either the Toeplitz
operator T_a or its adjoint has trivial kernel.
TauCeti.ker_toeplitz_eq_bot_or_ker_adjoint_toeplitz_eq_bot
{a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)} (ha : a ≠ 0) :
(↑(TauCeti.toeplitz a)).ker = ⊥ ∨ (↑(ContinuousLinearMap.adjoint (TauCeti.toeplitz a))).ker = ⊥
Lean
Formalized in Tau Ceti as TauCeti.ker_toeplitz_eq_bot_or_ker_adjoint_toeplitz_eq_bot.
Sources
Uses 2
TheoremThe convolution theorem for the inverse Fourier transform#
The inverse Fourier transform of the convolution of two integrable functions is the product of their inverse Fourier transforms.
Real.fourierInv_mul_convolution_eq.{u_1, u_2} {E : Type u_1} {R : Type u_2} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedRing R]
[NormedSpace ℂ R] [IsScalarTower ℂ R R] [SMulCommClass ℂ R R] [CompleteSpace R] {f₁ f₂ : E → R}
(hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume)
(hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (x : E) :
FourierTransformInv.fourierInv
(MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.mul ℂ R) MeasureTheory.volume) x =
FourierTransformInv.fourierInv f₁ x * FourierTransformInv.fourierInv f₂ x
TheoremEquality in Wirtinger's inequality#
Equality holds exactly when, on [a, b], the function
is its mean plus a first harmonic cos (2π t / (b - a)) • u + sin (2π t / (b - a)) • v.
TauCeti.integral_norm_sub_average_sq_eq_iff.{u_1} {a b : ℝ} {V : Type u_1} [NormedAddCommGroup V]
[InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {f f' : ℝ → V} (hab : a < b)
(hf : AbsolutelyContinuousOnInterval f a b)
(hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b)
(hf' : MeasureTheory.MemLp f' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) :
∫ (x : ℝ) in a..b, ‖f x - ⨍ (y : ℝ) in a..b, f y‖ ^ 2 =
((b - a) / (2 * Real.pi)) ^ 2 * ∫ (x : ℝ) in a..b, ‖f' x‖ ^ 2 ↔
∃ u v,
∀ t ∈ Set.Icc a b,
f t - ⨍ (y : ℝ) in a..b, f y =
Real.cos (2 * Real.pi * t / (b - a)) • u + Real.sin (2 * Real.pi * t / (b - a)) • v
Uses 1
TheoremThe exterior reciprocal Fourier identity#
For |x| ≥ 1, the Fourier integral of the
Haagerup–Zsidó kernel is ∫ e^{itx} k(t) dt = 1 / x.
TauCeti.HaagerupZsido.integral_exp_mul_I_mul_reciprocalKernel {x : ℝ} (hx : 1 ≤ |x|) :
∫ (t : ℝ), Complex.exp (↑x * ↑t * Complex.I) * TauCeti.HaagerupZsido.reciprocalKernel t = (↑x)⁻¹
Lean
Formalized in Tau Ceti as TauCeti.HaagerupZsido.integral_exp_mul_I_mul_reciprocalKernel.
Sources
Used by 1
TheoremKronecker's theorem for linear flows on tori#
A line t ↦ θ + t ν in the torus
(ℝ / pℤ)^ι is dense exactly when its velocity ν is nonresonant: ∑ i, k i * ν i ≠ 0 for every
nonzero integer vector k.
TauCeti.AddCircle.denseRange_coe_add_mul_iff.{u_1} {ι : Type u_1} [Fintype ι] {p : ℝ} (hp : p ≠ 0)
(θ ν : ι → ℝ) :
(DenseRange fun t i => ↑(θ i + ν i * t)) ↔ ∀ (k : ι → ℤ), ∑ i, ↑(k i) * ν i = 0 → k = 0
Uses 1
TheoremParseval's energy identity#
Parseval's energy identity for an absolutely continuous closed complex curve with square-integrable derivative. Each frequency contributes its squared frequency times the squared norm of the corresponding Fourier coefficient.
TauCeti.hasSum_sq_frequency_mul_sq_fourierCoeffOn {a b : ℝ} {f f' : ℝ → ℂ} (hab : a < b)
(hf : AbsolutelyContinuousOnInterval f a b)
(hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b)
(hf' : MeasureTheory.MemLp f' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) :
HasSum (fun n => (2 * Real.pi * ↑n / (b - a)) ^ 2 * ‖fourierCoeffOn hab f n‖ ^ 2)
((b - a)⁻¹ * ∫ (t : ℝ) in a..b, ‖f' t‖ ^ 2)
Lean
Formalized in Tau Ceti as TauCeti.hasSum_sq_frequency_mul_sq_fourierCoeffOn.
Sources
TheoremPlancherel bound for Fourier multipliers#
‖T_m‖ ≤ ‖m‖_∞.
MeasureTheory.Lp.norm_fourierMultiplierCLM_le.{u_1, u_2} {E : Type u_1} {F : Type u_2}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
(m : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) :
‖MeasureTheory.Lp.fourierMultiplierCLM F m‖ ≤ ‖m‖
Used by 1
TheoremReal Cauchy Poisson identity#
For y > 0, the sum over integers of
exp (-2π y |n|) equals the sum of y / (π (y² + n²)).
TauCeti.tsum_exp_neg_mul_abs_int_eq_tsum_div {y : ℝ} (hy : 0 < y) :
∑' (n : ℤ), Real.exp (-(2 * Real.pi * y * |↑n|)) = ∑' (n : ℤ), y / (Real.pi * (y ^ 2 + ↑n ^ 2))
TheoremRiemann--Lebesgue on a vertical line#
the integral of f against the oscillating factor
x ^ (i t) tends to 0 as x → ∞.
No hypothesis is needed on f. A limit along atTop only sees x > 0, and there the factor
x ^ (i t) has modulus 1, so the integrand is integrable exactly when f is; when f is not
integrable both the left-hand side and the limit are 0. (For x ≤ 0 the equivalence fails —
at x = 0 the integrand vanishes almost everywhere, and for x < 0 the branch of the complex
power contributes a factor of modulus exp (-π t) — but those scales are irrelevant here.)
TauCeti.tendsto_integral_cpow_mul_I_smul_atTop.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℂ E] (f : ℝ → E) :
Filter.Tendsto (fun x => ∫ (t : ℝ), ↑x ^ (↑t * Complex.I) • f t) Filter.atTop (nhds 0)
Used by 2
TheoremSpectral theorem for strongly continuous unitary representations, cyclic form#
For a
strongly continuous unitary representation π of a locally compact abelian group G on a
Hilbert space H and a vector ξ, the matrix coefficient g ↦ ⟪ξ, π(g) ξ⟫ is the
Fourier–Stieltjes transform of a finite inner regular measure on the Pontryagin dual of G.
ContRepresentation.exists_pontryaginMeasureTransform_eq_inner.{u_1, u_2} {G : Type u_1}
[AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G]
[MeasurableSpace (PontryaginDual (Multiplicative G))]
[BorelSpace (PontryaginDual (Multiplicative G))] {H : Type u_2} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H)
(hcont : ∀ (v : H), Continuous fun g => (π (Multiplicative.ofAdd g)) v) (hπ : π.IsUnitary)
(ξ : H) :
∃ μ,
(↑μ).InnerRegular ∧
∀ (g : G), μ.pontryaginMeasureTransform g = inner ℂ ξ ((π (Multiplicative.ofAdd g)) ξ)
Lean
Formalized in Tau Ceti as ContRepresentation.exists_pontryaginMeasureTransform_eq_inner.
Sources
Used by 1
TheoremWeyl's equidistribution theorem for linear flows#
If the velocity ν is nonresonant, that
is ⟪k, ν⟫ ≠ 0 for every nonzero k ∈ ℤ^d, then along every line t ↦ θ + t ν of the unit
torus the time averages T⁻¹ ∫₀ᵀ f (θ + t ν) dt of a continuous function f tend to its space
average ∫ f.
TauCeti.UnitAddTorus.tendsto_inv_smul_intervalIntegral.{u_1} {d : Type u_1} [Fintype d] {ν : d → ℝ}
(hν : ∀ (k : d → ℤ), ∑ i, ↑(k i) * ν i = 0 → k = 0) (θ : d → ℝ) (f : C(UnitAddTorus d, ℂ)) :
Filter.Tendsto (fun T => T⁻¹ • ∫ (t : ℝ) in 0..T, f fun i => ↑(θ i + ν i * t)) Filter.atTop
(nhds (∫ (x : UnitAddTorus d), f x))
Lean
Formalized in Tau Ceti as TauCeti.UnitAddTorus.tendsto_inv_smul_intervalIntegral.
Sources
Used by 1
TheoremWirtinger's inequality#
An absolutely continuous function on [a, b] with f a = f b,
valued in a finite-dimensional real inner product space and with square-integrable
almost-everywhere derivative, deviates from its mean in L² by at most (b - a) / (2π) times
the L² norm of its derivative.
TauCeti.integral_norm_sub_average_sq_le.{u_1} {a b : ℝ} {V : Type u_1} [NormedAddCommGroup V]
[InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {f f' : ℝ → V} (hab : a < b)
(hf : AbsolutelyContinuousOnInterval f a b)
(hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b)
(hf' : MeasureTheory.MemLp f' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) :
∫ (x : ℝ) in a..b, ‖f x - ⨍ (y : ℝ) in a..b, f y‖ ^ 2 ≤
((b - a) / (2 * Real.pi)) ^ 2 * ∫ (x : ℝ) in a..b, ‖f' x‖ ^ 2
Uses 1 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.