Hilbert's inequality

DefinitionHilbert kernel#✓fully proved

The Hilbert kernel with 0-based indices: 1 / ((m + 1) + (n + 1)).

noncomputable def hilbertKernel (m n : ℕ) : ℝ := ((m : ℝ) + n + 2)⁻¹

Used by 6

Used byHilbert's inequality · Finite Hilbert inequality · Nonnegativity of the Hilbert kernel · Row sum bound for the Hilbert kernel · Symmetry of the Hilbert kernel · Summability of the Hilbert double series

DefinitionRow integrand for the Hilbert kernel#✓fully proved

The row integrand x ↦ 1 / ((M + x) * √x) used to bound the row sums of the Hilbert kernel by an integral.

noncomputable def hilbertKernelRow (M : ℝ) (x : ℝ) : ℝ := ((M + x) * Real.sqrt x)⁻¹

Used by 11

Used byDerivative of the arctangent antiderivative of the row integrand · Hilbert row integrand is decreasing on (1, ∞) · Continuity of the Hilbert row integrand · Nonnegativity of the Hilbert row integrand · Terms of the Hilbert row series · Row sum bound for the Hilbert kernel · Integrability of the Hilbert row integrand on (1, ∞) · Improper integral of the Hilbert row integrand · Finite integral of the Hilbert row integrand · Summability of the Hilbert row series in unfolded form · Summability of the Hilbert row series

TheoremNonnegativity of the Hilbert kernel#✓fully proved

The Hilbert kernel is nonnegative.

theorem hilbertKernel_nonneg (m n : ℕ) : 0 ≤ hilbertKernel m n

Uses 1 · Used by 3

Statement usesHilbert kernel

Used byHilbert's inequality · Finite Hilbert inequality · Summability of the Hilbert double series

TheoremNonnegativity of the Hilbert row integrand#✓fully proved

The row integrand is nonnegative on (0, ∞) when M > 0.

theorem hilbertKernelRow_nonneg {M : ℝ} (hM : 0 < M) {x : ℝ} (hx : 0 < x) :
    0 ≤ hilbertKernelRow M x

Uses 1 · Used by 3

Statement usesRow integrand for the Hilbert kernel

Used byRow sum bound for the Hilbert kernel · Integrability of the Hilbert row integrand on (1, ∞) · Summability of the Hilbert row series

TheoremContinuity of the Hilbert row integrand#✓fully proved

The row integrand is continuous on (0, ∞) when M > 0.

theorem hilbertKernelRow_continuousOn {M : ℝ} (hM : 0 < M) :
    ContinuousOn (hilbertKernelRow M) (Set.Ioi 0)

Uses 1 · Used by 2

Statement usesRow integrand for the Hilbert kernel

Used byIntegrability of the Hilbert row integrand on (1, ∞) · Finite integral of the Hilbert row integrand

TheoremHilbert row integrand is decreasing on (1, ∞)#✓fully proved

The row integrand is antitone on [1, ∞) when M > 0.

theorem hilbertKernelRow_antitoneOn {M : ℝ} (hM : 0 < M) :
    AntitoneOn (hilbertKernelRow M) (Set.Ici 1)

Uses 1 · Used by 2

Statement usesRow integrand for the Hilbert kernel

Used byRow sum bound for the Hilbert kernel · Summability of the Hilbert row series

TheoremDerivative of the arctangent antiderivative of the row integrand#✓fully proved

The derivative of the antiderivative (2 / √M) * arctan √(x / M).

theorem hasDerivAt_hilbertAntideriv {M : ℝ} (hM : 0 < M) {x : ℝ} (hx : 0 < x) :
    HasDerivAt (fun x => (2 / Real.sqrt M) * Real.arctan (Real.sqrt (x / M)))
      (hilbertKernelRow M x) x

Uses 1 · Used by 1

Statement usesRow integrand for the Hilbert kernel

Used byFinite integral of the Hilbert row integrand

TheoremFinite integral of the Hilbert row integrand#✓fully proved

The finite integral of the row integrand, via its antiderivative.

theorem intervalIntegral_hilbertKernelRow {M : ℝ} (hM : 0 < M) {B : ℝ} (hB : 1 ≤ B) :
    ∫ x in (1:ℝ)..B, hilbertKernelRow M x =
      (2 / Real.sqrt M) *
        (Real.arctan (Real.sqrt (B / M)) - Real.arctan (Real.sqrt (1 / M)))

Uses 3 · Used by 2

Statement usesRow integrand for the Hilbert kernel

Proof usesDerivative of the arctangent antiderivative of the row integrand · Continuity of the Hilbert row integrand

Used byIntegrability of the Hilbert row integrand on (1, ∞) · Improper integral of the Hilbert row integrand

TheoremIntegrability of the Hilbert row integrand on (1, ∞)#✓fully proved

The row integrand is integrable on (1, ∞), with a uniform bound on the interval integrals.

theorem integrableOn_Ioi_hilbertKernelRow {M : ℝ} (hM : 0 < M) :
    IntegrableOn (hilbertKernelRow M) (Set.Ioi 1)

Uses 4 · Used by 3

Statement usesRow integrand for the Hilbert kernel

Proof usesContinuity of the Hilbert row integrand · Nonnegativity of the Hilbert row integrand · Finite integral of the Hilbert row integrand

Used byRow sum bound for the Hilbert kernel · Improper integral of the Hilbert row integrand · Summability of the Hilbert row series

TheoremImproper integral of the Hilbert row integrand#✓fully proved

The improper integral of the row integrand over (1, ∞).

theorem integral_Ioi_hilbertKernelRow {M : ℝ} (hM : 0 < M) :
    ∫ x in Set.Ioi (1:ℝ), hilbertKernelRow M x =
      (2 / Real.sqrt M) * (Real.pi / 2 - Real.arctan (Real.sqrt (1 / M)))

Uses 3 · Used by 1

Statement usesRow integrand for the Hilbert kernel

Proof usesIntegrability of the Hilbert row integrand on (1, ∞) · Finite integral of the Hilbert row integrand

Used byRow sum bound for the Hilbert kernel

TheoremLower bound for the arctangent#✓fully proved

A lower bound for arctan: t / (1 + t ^ 2) ≤ arctan t for t ≥ 0.

theorem div_one_add_sq_le_arctan {t : ℝ} (ht : 0 ≤ t) :
    t / (1 + t ^ 2) ≤ Real.arctan t

Used by 1

Used byRow sum bound for the Hilbert kernel

DefinitionTerms of the Hilbert row series#✓fully proved

The n-th term of the row series, 1 / ((M + (n + 1)) * √((n + 1))), as a function of n : ℕ.

noncomputable def hilbertKernelRowSeq (M : ℝ) (n : ℕ) : ℝ :=
  hilbertKernelRow M ((n : ℝ) + 1)

Uses 1 · Used by 3

Statement usesRow integrand for the Hilbert kernel

Used byRow sum bound for the Hilbert kernel · Summability of the Hilbert row series in unfolded form · Summability of the Hilbert row series

TheoremSummability of the Hilbert row series#✓fully proved

Summability of the row series.

theorem summable_hilbertKernelRowSeq {M : ℝ} (hM : 0 < M) :
    Summable (hilbertKernelRowSeq M)

Uses 5 · Used by 2

Statement usesTerms of the Hilbert row series

Proof usesRow integrand for the Hilbert kernel · Hilbert row integrand is decreasing on (1, ∞) · Nonnegativity of the Hilbert row integrand · Integrability of the Hilbert row integrand on (1, ∞)

Used byRow sum bound for the Hilbert kernel · Summability of the Hilbert row series in unfolded form

TheoremSummability of the Hilbert row series in unfolded form#✓fully proved

Summability of the row series in unfurled form.

theorem summable_hilbertKernelRow {M : ℝ} (hM : 0 < M) :
    Summable (fun n : ℕ => ((M + ((n:ℝ) + 1)) * Real.sqrt ((n:ℝ) + 1))⁻¹)

Uses 3 · Used by 1

Proof usesRow integrand for the Hilbert kernel · Terms of the Hilbert row series · Summability of the Hilbert row series

Used byFinite Hilbert inequality

TheoremRow sum bound for the Hilbert kernel#✓fully proved

The row sum of the Hilbert kernel is at most π / √(m + 1).

theorem hilbertKernel_row_sum_le (m : ℕ) :
    ∑' (n : ℕ), hilbertKernel m n * (Real.sqrt ((n:ℝ) + 1))⁻¹ ≤
      Real.pi / Real.sqrt ((m:ℝ) + 1)

Uses 9 · Used by 1

Statement usesHilbert kernel

Proof usesLower bound for the arctangent · Row integrand for the Hilbert kernel · Terms of the Hilbert row series · Hilbert row integrand is decreasing on (1, ∞) · Nonnegativity of the Hilbert row integrand · Integrability of the Hilbert row integrand on (1, ∞) · Improper integral of the Hilbert row integrand · Summability of the Hilbert row series

Used byFinite Hilbert inequality

TheoremSymmetry of the Hilbert kernel#✓fully proved

The Hilbert kernel is symmetric.

theorem hilbertKernel_symm (m n : ℕ) : hilbertKernel m n = hilbertKernel n m

Uses 1 · Used by 1

Statement usesHilbert kernel

Used byFinite Hilbert inequality

TheoremSchur test for finite bilinear forms#✓fully proved

The Schur test for finite bilinear forms: a weighted row/column bound implies a bound on the bilinear form with constant √(α * β).

theorem schurTest_finite {N : ℕ} {A : ℕ → ℕ → ℝ} {a b r c : ℕ → ℝ} {α β : ℝ}
    (hA : ∀ m n, 0 ≤ A m n) (ha : ∀ n, 0 ≤ a n) (hb : ∀ n, 0 ≤ b n)
    (hr : ∀ n, 0 < r n) (hc : ∀ n, 0 < c n) (hα : 0 ≤ α) (hβ : 0 ≤ β)
    (hrow : ∀ m, ∑ n ∈ Finset.range N, A m n * r n ≤ α * c m)
    (hcol : ∀ n, ∑ m ∈ Finset.range N, A m n * c m ≤ β * r n) :
    ∑ m ∈ Finset.range N, ∑ n ∈ Finset.range N, A m n * a m * b n ≤
      Real.sqrt (α * β) * Real.sqrt (∑ m ∈ Finset.range N, (a m) ^ 2) *
        Real.sqrt (∑ n ∈ Finset.range N, (b n) ^ 2)

Used by 1

Used byFinite Hilbert inequality

TheoremFinite Hilbert inequality#✓fully proved

The finite form of Hilbert's inequality, from the Schur test with the weights r n = 1 / √(n + 1) and the row bound hilbertKernel_row_sum_le.

theorem hilbert_inequality_finite {N : ℕ} {a b : ℕ → ℝ}
    (ha : ∀ n, 0 ≤ a n) (hb : ∀ n, 0 ≤ b n) :
    ∑ m ∈ Finset.range N, ∑ n ∈ Finset.range N,
      a m * b n / ((m:ℝ) + n + 2) ≤
      Real.pi * Real.sqrt (∑ m ∈ Finset.range N, (a m) ^ 2) *
        Real.sqrt (∑ n ∈ Finset.range N, (b n) ^ 2)

Uses 6 · Used by 2

Proof usesHilbert kernel · Nonnegativity of the Hilbert kernel · Row sum bound for the Hilbert kernel · Symmetry of the Hilbert kernel · Schur test for finite bilinear forms · Summability of the Hilbert row series in unfolded form

Used byHilbert's inequality · Summability of the Hilbert double series

TheoremSummability of the Hilbert double series#✓fully proved

The nonnegative Hilbert double series is summable for square-summable inputs.

theorem summable_hilbert_terms {a b : ℕ → ℝ}
    (ha : Summable (fun n => (a n) ^ 2)) (hb : Summable (fun n => (b n) ^ 2)) :
    Summable (fun p : ℕ × ℕ => |a p.1 * b p.2| * hilbertKernel p.1 p.2)

Uses 3

Statement usesHilbert kernel

Proof usesNonnegativity of the Hilbert kernel · Finite Hilbert inequality

TheoremHilbert's inequality#✓fully proved

Hilbert's inequality for square-summable real sequences.

theorem hilbert_inequality {a b : ℕ → ℝ}
    (ha : Summable (fun n => (a n) ^ 2)) (hb : Summable (fun n => (b n) ^ 2)) :
    ∑' (p : ℕ × ℕ), |a p.1 * b p.2| * hilbertKernel p.1 p.2 ≤
      Real.pi * Real.sqrt (∑' (n : ℕ), (a n) ^ 2) *
        Real.sqrt (∑' (n : ℕ), (b n) ^ 2)

Uses 3

Statement usesHilbert kernel

Proof usesNonnegativity of the Hilbert kernel · Finite Hilbert inequality

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.