Carleman's inequality

DefinitionGeometric mean of the initial terms of a sequence#✓fully proved

The geometric mean of the first n + 1 terms of a sequence a.

noncomputable def carlemanGeomMean (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  (∏ k ∈ Finset.range (n + 1), a k) ^ ((((n + 1 : ℕ) : ℝ))⁻¹)

Used by 3

Used byStrengthened finite Carleman inequality · Finite Carleman inequality · Carleman's inequality

TheoremStrengthened finite Carleman inequality#✓fully proved

Strengthened finite Carleman inequality: the partial sum of the geometric means plus (M + 1) times the last geometric mean is bounded by e times the partial sum of the terms.

theorem carlemanGeomMean_sum_add_mul_le {a : ℕ → ℝ} (ha : ∀ n, 0 ≤ a n) (M : ℕ) :
    (∑ n ∈ Finset.range (M + 1), carlemanGeomMean a n) +
      ((M : ℝ) + 1) * carlemanGeomMean a M ≤
        Real.exp 1 * ∑ n ∈ Finset.range (M + 1), a n

noncomputable def carlemanGeomMean (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  (∏ k ∈ Finset.range (n + 1), a k) ^ ((((n + 1 : ℕ) : ℝ))⁻¹)

MathlibExt/Analysis/Series/CarlemanInequality.lean:49

Uses 1 · Used by 1

Statement usesGeometric mean of the initial terms of a sequence

Used byFinite Carleman inequality

TheoremFinite Carleman inequality#✓fully proved

Finite Carleman inequality: the partial sum of the geometric means is bounded by e times the partial sum of the terms.

theorem carlemanGeomMean_sum_le {a : ℕ → ℝ} (ha : ∀ n, 0 ≤ a n) (N : ℕ) :
    (∑ n ∈ Finset.range N, carlemanGeomMean a n) ≤
      Real.exp 1 * ∑ n ∈ Finset.range N, a n

noncomputable def carlemanGeomMean (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  (∏ k ∈ Finset.range (n + 1), a k) ^ ((((n + 1 : ℕ) : ℝ))⁻¹)

MathlibExt/Analysis/Series/CarlemanInequality.lean:49

Uses 2 · Used by 1

Statement usesGeometric mean of the initial terms of a sequence

Proof usesStrengthened finite Carleman inequality

Used byCarleman's inequality

TheoremCarleman's inequality#✓fully proved

Carleman's inequality (sharp form): for a summable nonnegative sequence, the series of geometric means of the initial products is summable and bounded by e times the series of the terms.

theorem carleman_inequality {a : ℕ → ℝ} (ha : ∀ n, 0 ≤ a n) (hsumm : Summable a) :
    Summable (carlemanGeomMean a) ∧
      ∑' n, carlemanGeomMean a n ≤ Real.exp 1 * ∑' n, a n

noncomputable def carlemanGeomMean (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  (∏ k ∈ Finset.range (n + 1), a k) ^ ((((n + 1 : ℕ) : ℝ))⁻¹)

MathlibExt/Analysis/Series/CarlemanInequality.lean:49

Uses 2

Statement usesGeometric mean of the initial terms of a sequence

Proof usesFinite Carleman inequality

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.