Convolutions and translates on the circle
AbbreviationThe circle \(\mathbb{R}/2\pi\mathbb{Z}\)#✓fully proved
The circle \(T = \mathbb{R}/2\pi\mathbb{Z}\), the quotient of the additive group \(\mathbb{R}\) by its subgroup \(2\pi\mathbb{Z}\).
TheoremConvolutions and linear combinations of translates have the same closure#●ready to prove
Let \(T = \mathbb{R}/2\pi\mathbb{Z}\) with the measure induced by Lebesgue measure on \([0, 2\pi)\), and let \(L^1(T)\) be the space of real-valued integrable functions on \(T\) modulo equality almost everywhere. Fix a real-valued integrable \(f\) on \(T\). Let \(B_f \subseteq L^1(T)\) be the set of classes of the finite linear combinations of translates \(x \mapsto \sum_{i=1}^N a_i f(x - \tau_i)\) with \(N \in \mathbb{N}\), \(a_i \in \mathbb{R}\) and \(\tau_i \in T\), and let \(M_f \subseteq L^1(T)\) be the set of classes of the convolutions \((f * g)(x) = \int_T f(y)\, g(x - y)\,dy\) with \(g\) real-valued and integrable on \(T\). Then \(M_f\) and \(B_f\) have the same closure in \(L^1(T)\).
public theorem_wanted closure_convolution_set_eq_closure_translate_span
(f : T → ℝ)
(hf : MemLp f 1 (volume : Measure T))
(Bf Mf : Set (Lp ℝ 1 (volume : Measure T)))
(hBf : Bf =
{u : Lp ℝ 1 (volume : Measure T) | ∃ N : ℕ, ∃ a : Fin N → ℝ, ∃ τ : Fin N → T,
(u : T → ℝ) =ᵐ[(volume : Measure T)]
(fun x : T => ∑ i : Fin N, a i * f (x - τ i))})
(hMf : Mf =
{u : Lp ℝ 1 (volume : Measure T) | ∃ g : T → ℝ, MemLp g 1 (volume : Measure T) ∧
(u : T → ℝ) =ᵐ[(volume : Measure T)] (f ⋆ g)}) :
closure Mf = closure Bfabbrev T := AddCircle (2 * Real.pi)WantedExt/Analysis/Fourier/ConvolutionTranslateClosureCircleWanted.lean:51
Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Commutative Banach algebras and commutative topological algebras), problem
ma_proofbench_l2_12.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.