Titchmarsh convolution theorem
DefinitionThe Volterra-form sub-conjecture of Scottish Book Problem 124#✓fully proved
The statement that for every continuous function \(f : \mathbb{R} \to \mathbb{R}\) with \(f(0) \ne 0\) and every function \(y : \mathbb{R} \to \mathbb{R}\) that is Lebesgue integrable on \([0, 1]\), if \(\int_0^x y(t) f(x - t)\,dt = 0\) for every \(x \in [0, 1]\), then \(y = 0\) almost everywhere on \([0, 1]\).
The Scottish Book typescript prints the upper limit of the integral as \(1\), but the entry's own arguments show that the intended upper limit is \(x\) (Volterra form); with upper limit \(1\) the claim is false, since \(f \equiv 1\) and \(y(t) = t - 1/2\) give a nonzero solution. The typescript does not specify a function class for \(y\); integrability on \([0, 1]\) is motivated by the \(L^2\) context of the entry.
def ScottishBookProblem124Claim : Prop :=
∀ (f : ℝ → ℝ), Continuous f → f 0 ≠ 0 →
∀ (y : ℝ → ℝ),
MeasureTheory.IntegrableOn y (Set.Icc (0 : ℝ) 1) MeasureTheory.volume →
(∀ x ∈ Set.Icc (0 : ℝ) 1, ∫ t in (0 : ℝ)..x, y t * f (x - t) = 0) →
y =ᵐ[MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)] 0
Used by 1
TheoremThe Volterra-form sub-conjecture of Scottish Book Problem 124 holds#●ready to prove
For every continuous function \(f : \mathbb{R} \to \mathbb{R}\) with \(f(0) \ne 0\) and every function \(y : \mathbb{R} \to \mathbb{R}\) that is Lebesgue integrable on \([0, 1]\), if \(\int_0^x y(t) f(x - t)\,dt = 0\) for every \(x \in [0, 1]\), then \(y = 0\) almost everywhere on \([0, 1]\).
theorem_wanted marcinkiewicz124_holds : ScottishBookProblem124Claim
def ScottishBookProblem124Claim : Prop :=
∀ (f : ℝ → ℝ), Continuous f → f 0 ≠ 0 →
∀ (y : ℝ → ℝ),
MeasureTheory.IntegrableOn y (Set.Icc (0 : ℝ) 1) MeasureTheory.volume →
(∀ x ∈ Set.Icc (0 : ℝ) 1, ∫ t in (0 : ℝ)..x, y t * f (x - t) = 0) →
y =ᵐ[MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)] 0
WantedExt/Analysis/ScottishBook124Wanted.lean:35
Sources
- Józef Marcinkiewicz, Problem 124 of the Scottish Book; typescript PDF p.58, printed p.55. TYPESCRIPT TYPO, CORRECTED (Phase 5): the typescript prints the equation as
∫₀¹ y(t) f(x-t) dt = 0, but the intended upper limit isx(Volterra form). The literal∫₀¹reading is false:f ≡ 1,y(t) = t - 1/2is a nonzero solution. Only the Volterra∫₀ˣreading is filed here. Positive by the local Titchmarsh convolution theorem: E. C. Titchmarsh, "The zeros of certain integral functions", Proc. London Math. Soc. s2-25 (1926), 283–302, DOI 10.1112/plms/s2-25.1.283. Sketch: Titchmarsh givesλ, μ ≥ 0withλ + μ ≥ 1such thaty = 0a.e. on(0, λ)andf = 0a.e. on(0, μ). Continuity offat0withf 0 ≠ 0forcesμ = 0(otherwisefwould be a.e. zero on a positive-measure initial interval while being nonzero near0), soλ ≥ 1andy = 0a.e. on[0, 1].
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.