Orthogonal systems and general orthogonal series

TheoremBanach's Problem 186: a complete orthonormal system with divergent Fourier series#●ready to prove

There is a sequence \((\varphi_i)_{i \ge 0}\) of square-integrable real functions on \([0, 1]\), with respect to Lebesgue measure, that is orthonormal, \(\int_0^1 \varphi_i \varphi_j \, dx = \delta_{ij}\) for all \(i, j\), and complete, in the sense that every square-integrable \(g\) on \([0, 1]\) with \(\int_0^1 g \varphi_i \, dx = 0\) for all \(i\) vanishes almost everywhere on \([0, 1]\), such that the following holds: for every continuous \(f \colon \mathbb{R} \to \mathbb{R}\) that is not identically zero on \([0, 1]\), with Fourier coefficients \(c_i = \int_0^1 f \varphi_i \, dx\), the partial sums \(\sum_{i < N} c_i \varphi_i(t)\) are unbounded in \(N\) for almost every \(t \in [0, 1]\).

The \(\varphi_i\) are not assumed continuous: the source imposes continuity only on \(f\), and continuity of the \(\varphi_i\) would make the claim false (taking \(f = \varphi_0\) would give Fourier coefficients \(\delta_{0i}\) and bounded partial sums).

MathlibExt.Analysis.FunctionalAnalysis.ScottishBook186Wanted.banach186_orthonormal_system_divergent_ae · 17 lines

theorem_wanted banach186_orthonormal_system_divergent_ae :
    ∃ φ : ℕ → ℝ → ℝ,
      (∀ i, MeasureTheory.AEStronglyMeasurable (φ i)
          (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) ∧
        MeasureTheory.MemLp (φ i) 2
          (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))) ∧
      (∀ i j, ∫ x in Set.Icc (0 : ℝ) 1, φ i x * φ j x ∂MeasureTheory.volume =
        if i = j then 1 else 0) ∧
      (∀ g : ℝ → ℝ, MeasureTheory.MemLp g 2
          (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) →
        (∀ i, ∫ x in Set.Icc (0 : ℝ) 1, g x * φ i x
          ∂MeasureTheory.volume = 0) →
        g =ᵐ[MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)] 0) ∧
      ∀ f : C(ℝ, ℝ), (∃ t ∈ Set.Icc (0 : ℝ) 1, f t ≠ 0) →
        ∀ᵐ t ∂MeasureTheory.volume, t ∈ Set.Icc (0 : ℝ) 1 →
          ∀ M : ℝ, ∃ N : ℕ, M < |∑ i ∈ Finset.range N,
            (∫ x in Set.Icc (0 : ℝ) 1, f x * φ i x ∂MeasureTheory.volume) * φ i t|

Sources

• S. Banach, Problem 186 of the Scottish Book; answered by A. M. Olevskii, "Fourier series with respect to general orthogonal systems" (1975). See the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

DefinitionCountability of orthogonal systems of sequences#✓fully proved

This is the statement that every set \(S\) of real sequences \((f_n)_{n \in \mathbb{N}}\) with the following two properties is at most countable: no member of \(S\) is the zero sequence; and for any two distinct \(f, g \in S\) the series \(\sum_{n} f_n g_n\) converges absolutely and its sum is \(0\).

The zero sequence is excluded because it is orthogonal to everything, so without this it would be a trivial member of every family.

def SequenceSystemsAreCountable : Prop :=
  ∀ S : Set (ℕ → ℝ),
    (∀ f ∈ S, f ≠ 0) →
    (∀ f ∈ S, ∀ g ∈ S, f ≠ g →
      Summable (fun n => f n * g n) ∧ ∑' n, f n * g n = 0) →
    S.Countable

Used by 1

Used byOrthogonal systems need not be countable

DefinitionCountability of orthogonal systems of functions#✓fully proved

Let \(\lambda\) be Lebesgue measure on \([0, 1]\). This is the statement that every set \(S\) of functions \([0, 1] \to \mathbb{R}\) with the following three properties is at most countable: no member of \(S\) is \(\lambda\)-almost everywhere equal to \(0\); any two members of \(S\) that are equal \(\lambda\)-almost everywhere are equal; and any two members \(f, g\) of \(S\) that are not equal \(\lambda\)-almost everywhere are measurable, have \(\lambda\)-integrable product \(fg\), and satisfy \(\int_{[0, 1]} f g \, d\lambda = 0\).

No square-integrability is assumed. Without the second property, uncountably many almost-everywhere-equal copies of one function would satisfy the orthogonality condition vacuously. The first property excludes the indicator functions of single points, each of which is zero almost everywhere.

def FunctionSystemsAreCountable : Prop :=
  ∀ S : Set (↥(Set.Icc (0 : ℝ) 1) → ℝ),
    (∀ f ∈ S, ¬ (f =ᵐ[MeasureTheory.volume] 0)) →
    (∀ f ∈ S, ∀ g ∈ S, f =ᵐ[MeasureTheory.volume] g → f = g) →
    (∀ f ∈ S, ∀ g ∈ S, ¬ (f =ᵐ[MeasureTheory.volume] g) →
      Measurable f ∧ Measurable g ∧
      MeasureTheory.Integrable (fun x : ↥(Set.Icc (0 : ℝ) 1) => f x * g x) ∧
      MeasureTheory.integral MeasureTheory.volume
        (fun x : ↥(Set.Icc (0 : ℝ) 1) => f x * g x) = 0) →
    S.Countable

Used by 1

Used byOrthogonal systems need not be countable

TheoremOrthogonal systems need not be countable#●ready to prove

Both of the following statements are false. (a) Every set \(S\) of real sequences \((f_n)_{n \in \mathbb{N}}\) in which no member is the zero sequence, and in which for any two distinct \(f, g \in S\) the series \(\sum_n f_n g_n\) converges absolutely with sum \(0\), is at most countable. (b) Let \(\lambda\) be Lebesgue measure on \([0, 1]\). Every set \(S\) of functions \([0, 1] \to \mathbb{R}\) in which no member is \(\lambda\)-almost everywhere equal to \(0\), no two distinct members are equal \(\lambda\)-almost everywhere, and any two members \(f, g\) that are not equal \(\lambda\)-almost everywhere are measurable with \(fg\) \(\lambda\)-integrable and \(\int_{[0, 1]} f g \, d\lambda = 0\), is at most countable.

This answers both parts of Mazur's Problem 51 of the Scottish Book in the negative: Plichko and Razenkov construct a continuum-sized pairwise-orthogonal family of sequences, and from it an uncountable orthogonal system of functions on an interval. No square-integrability is assumed; in \(\ell^2\) or \(L^2\) an orthogonal family is at most countable, since those spaces are separable Hilbert spaces.

theorem_wanted orthogonal_systems_not_necessarily_countable :
    ¬ SequenceSystemsAreCountable ∧ ¬ FunctionSystemsAreCountable

Sources

• S. Mazur, Problem 51 of the Scottish Book; A. M. Plichko and V. Razenkov, On three problems from the Scottish Book connected with orthogonal systems, Colloq. Math. 70 (1996), 227-234, Section 3; see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

Uses 2

Statement usesCountability of orthogonal systems of functions · Countability of orthogonal systems of sequences

DefinitionLebesgue measure on the unit interval (Scottish Book Problem 86)#✓fully proved

Lebesgue measure on \(\mathbb{R}\) restricted to the unit interval \([0, 1]\), the ambient measure for Problem 86.

noncomputable def scottishBook86Measure : MeasureTheory.Measure ℝ :=
  MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)

Used by 1

Used byScottish Book Problem 86 (Banach)

DefinitionScottish Book Problem 86 (Banach)#✓fully proved

The claim that for every real \(M > 0\) and every sequence \((\varphi_n)_{n \in \mathbb{N}}\) of functions \(\mathbb{R} \to \mathbb{R}\) that are almost everywhere measurable on \([0, 1]\), orthonormal in \(L^2[0, 1]\) (that is, \(\int_0^1 \varphi_n \varphi_m \, dt\) is \(1\) if \(n = m\) and \(0\) otherwise) and satisfy \(|\varphi_n(t)| \le M\) for all \(n\) and all \(t \in [0, 1]\), there is a sequence \((\psi_n)_{n \in \mathbb{N}}\) of functions \(\mathbb{R} \to \mathbb{R}\), almost everywhere measurable on \([0, 1]\), orthonormal in the same sense and with \(|\psi_n(t)| \le M\) for all \(n\) and all \(t \in [0, 1]\), such that every \(\varphi_n\) equals some \(\psi_m\) and \((\psi_n)\) is complete: every \(g \in L^2[0, 1]\) with \(\int_0^1 \psi_n g \, dt = 0\) for all \(n\) vanishes almost everywhere on \([0, 1]\).

The case of interest in the original problem is when infinitely many functions are necessary for the completion.

MathlibExt.Analysis.FunctionalAnalysis.ScottishBook86Wanted.ScottishBookProblem86Claim · 15 lines

def ScottishBookProblem86Claim : Prop :=
  ∀ (M : ℝ) (φ : ℕ → ℝ → ℝ), 0 < M →
    (∀ n, AEStronglyMeasurable (φ n) scottishBook86Measure) →
    (∀ n m, ∫ t, φ n t * φ m t ∂scottishBook86Measure =
      if n = m then 1 else 0) →
    (∀ n t, t ∈ Set.Icc (0 : ℝ) 1 → |φ n t| ≤ M) →
    ∃ ψ : ℕ → ℝ → ℝ,
      (∀ n, AEStronglyMeasurable (ψ n) scottishBook86Measure) ∧
      (∀ n m, ∫ t, ψ n t * ψ m t ∂scottishBook86Measure =
        if n = m then 1 else 0) ∧
      (∀ n t, t ∈ Set.Icc (0 : ℝ) 1 → |ψ n t| ≤ M) ∧
      (∀ n, ∃ m, ψ m = φ n) ∧
      ∀ g : ℝ → ℝ, MemLp g 2 scottishBook86Measure →
        (∀ n, ∫ t, ψ n t * g t ∂scottishBook86Measure = 0) →
        g =ᵐ[scottishBook86Measure] 0

Uses 1 · Used by 1

Statement usesLebesgue measure on the unit interval (Scottish Book Problem 86)

Used byBanach's Scottish Book Problem 86 fails

TheoremBanach's Scottish Book Problem 86 fails#●ready to prove

The Scottish Book Problem 86 claim is false: there are a real \(M > 0\) and a sequence \((\varphi_n)_{n \in \mathbb{N}}\) of functions \(\mathbb{R} \to \mathbb{R}\), almost everywhere measurable on \([0, 1]\), orthonormal in \(L^2[0, 1]\) and with \(|\varphi_n(t)| \le M\) for all \(n\) and all \(t \in [0, 1]\), such that there is no sequence \((\psi_n)_{n \in \mathbb{N}}\) of functions \(\mathbb{R} \to \mathbb{R}\), almost everywhere measurable on \([0, 1]\), orthonormal in \(L^2[0, 1]\) and with \(|\psi_n(t)| \le M\) for all \(n\) and all \(t \in [0, 1]\), that has every \(\varphi_n\) as one of its terms and is complete: every \(g \in L^2[0, 1]\) with \(\int_0^1 \psi_n g \, dt = 0\) for all \(n\) vanishes almost everywhere on \([0, 1]\).

theorem_wanted banach86_refuted : ¬ ScottishBookProblem86Claim

Sources

• S. Banach, Problem 86 of the Scottish Book; negative answer via A. Plichko and A. Razenkov, "On three problems from the Scottish Book connected with orthogonal systems", Colloq. Math. 70 (1996), 227–234, Proposition 3, which constructs a bounded orthogonal sequence in a Banach space densely and non-compactly embedded in a Hilbert space that admits no extension to a fundamental orthogonal sequence using elements of the Banach space. Earlier work on the problem includes S. Kaczmarz (1936) and K. S. Kazarian ("On a problem of S. Banach from the Scottish Book", Proc. Amer. Math. Soc. 110 (1990), 881–887).

Uses 1

Statement usesScottish Book Problem 86 (Banach)

4 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.