Integral, multiplication and diagonal operators

Volterra and kernel integral operators, Cesàro and Hilbert operators, multiplication operators on C(X) and L², diagonal operators, Schur tests, L^p bounds for integral operators.

• Cesàro operator
• Diagonal operators
• Integral operators with continuous kernels
• Multiplication operators on L²
• Multiplication operators on spaces of continuous functions
• Schur test
• Titchmarsh convolution theorem
• Volterra operator

TheoremAn \(L^p\) bound for Hilbert's integral operator#●ready to prove

Let \(p\) be a real number with \(p > 1\) and let \(T\) be the operator on functions \(g : \mathbb{R} \to \mathbb{R}\) given by

\[Tg(x) = \int_0^\infty \frac{g(y)}{x+y}\,dy \qquad (x \in \mathbb{R}).\]

Let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([0,\infty)\), compactly supported and zero outside \([0,\infty)\), and put

\[C_p = \int_0^\infty \frac{dx}{x^{1/p}(1+x)}.\]

Then

\[\|Tf\|_{L^p([0,\infty))} \le C_p \, \|f\|_{L^p([0,\infty))},\]

where both norms are taken in \([0,\infty]\).

public theorem_wanted eLpNorm_hilbertIntegralOperator_le
    (p : ℝ) (hp : 1 < p) (T : (ℝ → ℝ) → (ℝ → ℝ))
  (hT : ∀ g : ℝ → ℝ, ∀ x : ℝ, T g x = ∫ y in Set.Ici (0 : ℝ), g y / (x + y))
  (f : ℝ → ℝ) (hf_cont : ContinuousOn f (Set.Ici (0 : ℝ)))
  (hf_cpt : HasCompactSupport f)
  (hf_support : Function.support f ⊆ Set.Ici (0 : ℝ))
  (Cp : ℝ) (hCp : Cp = ∫ x in Set.Ici (0 : ℝ), 1 / (x ^ (1 / p) * (1 + x))) :
  eLpNorm (T f) (ENNReal.ofReal p) (volume.restrict (Set.Ici (0 : ℝ))) ≤
    ENNReal.ofReal Cp * eLpNorm f (ENNReal.ofReal p) (volume.restrict (Set.Ici (0 : ℝ)))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Integral, integro-differential, and pseudodifferential operators), problem ma_proofbench_l2_29.

TheoremIntegral operators with an \(L^p\) kernel map \(L^q\) to \(L^p\)#●ready to prove

Let \(1 < p < \infty\) and let \(q \ge 1\) be the dual exponent, \(p^{-1} + q^{-1} = 1\). Let \(K : \mathbb{R}^2 \to \mathbb{R}\) lie in \(L^p((0,1)^2)\), where \(L^p((0,1)^2)\), \(L^p(0,1)\) and \(L^q(0,1)\) are spaces of real functions for Lebesgue measure. Then for every \(f \in L^q(0,1)\) the function \(y \mapsto K(x,y)f(y)\) is integrable on \((0,1)\) for almost every \(x \in (0,1)\), and there is a bounded linear operator \(A : L^q(0,1) \to L^p(0,1)\) such that for every \(f \in L^q(0,1)\),

\[(Af)(x) = \int_0^1 K(x,y) f(y)\,dy \quad \text{for almost every } x \in (0,1).\]

MathlibExt.Analysis.OperatorTheory.LpKernelIntegralOperatorBoundedWanted.integrable_kernel_mul_and_exists_clm_integral_operator · 20 lines

public theorem_wanted integrable_kernel_mul_and_exists_clm_integral_operator
  (p q : ENNReal)
  [Fact (1 ≤ p)]
  [Fact (1 ≤ q)]
  (hp_ne_top : p ≠ ⊤)
  (hp_gt_one : 1 < p)
  (hq : 1 / p + 1 / q = 1)
  (K : ℝ × ℝ → ℝ)
  (hK : MemLp K p
    ((Measure.restrict volume (Set.Ioo (0 : ℝ) 1)).prod
      (Measure.restrict volume (Set.Ioo (0 : ℝ) 1)))) :
  (∀ f : Lp ℝ q (Measure.restrict volume (Set.Ioo (0 : ℝ) 1)),
      ∀ᵐ x ∂(Measure.restrict volume (Set.Ioo (0 : ℝ) 1)),
        Integrable (fun y => K (x, y) * f y) (Measure.restrict volume (Set.Ioo (0 : ℝ) 1))) ∧
    (∃ A :
      Lp ℝ q (Measure.restrict volume (Set.Ioo (0 : ℝ) 1)) →L[ℝ]
        Lp ℝ p (Measure.restrict volume (Set.Ioo (0 : ℝ) 1)),
      ∀ f : Lp ℝ q (Measure.restrict volume (Set.Ioo (0 : ℝ) 1)),
        ∀ᵐ x ∂(Measure.restrict volume (Set.Ioo (0 : ℝ) 1)),
          A f x = ∫ y, K (x, y) * f y ∂(Measure.restrict volume (Set.Ioo (0 : ℝ) 1)))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Integral, integro-differential, and pseudodifferential operators), problem ma_proofbench_l2_87.

TheoremThe Laplace transform is bounded on \(L^p((0,\infty))\) exactly when \(p = 2\)#●ready to prove

For a real function \(f\) on \(\mathbb{R}\) let

\[Lf(s) = \int_0^\infty e^{-xs} f(x)\,dx \qquad (s \in \mathbb{R}).\]

Let \(p \in [1,\infty]\). Then \(p = 2\) if and only if there is a constant \(C\) with \(0 < C < \infty\) such that every real function \(f \in L^p([0,\infty))\) satisfies \(Lf \in L^p([0,\infty))\) and \(\|Lf\|_{L^p([0,\infty))} \le C\,\|f\|_{L^p([0,\infty))}\).

public theorem_wanted laplaceTransform_bounded_on_Lp_iff_eq_two (p : ENNReal) (hp : 1 ≤ p) :
  (∃ C : ENNReal, 0 < C ∧ C < ⊤ ∧ ∀ f : ℝ → ℝ,
  MemLp f p (volume.restrict (Set.Ici (0 : ℝ))) →
  MemLp (fun s : ℝ => ∫ x in Set.Ici (0 : ℝ), Real.exp (-x * s) * f x) p
    (volume.restrict (Set.Ici (0 : ℝ))) ∧
  eLpNorm (fun s : ℝ => ∫ x in Set.Ici (0 : ℝ), Real.exp (-x * s) * f x) p
    (volume.restrict (Set.Ici (0 : ℝ))) ≤
  C * eLpNorm f p (volume.restrict (Set.Ici (0 : ℝ)))) ↔
  p = 2

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Integral, integro-differential, and pseudodifferential operators), problem ma_proofbench_l2_31.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.