Kaluza's theorem on reciprocal power series

DefinitionPositive log-convex coefficients#✓fully proved

A real formal power series \(f = \sum_n a_n X^n\) has positive log-convex coefficients if \(a_n > 0\) for every natural number \(n\) and \(a_{n+1}^2 \le a_n a_{n+2}\) for every natural number \(n\). This is the hypothesis of Kaluza's bounds for the coefficients of the reciprocal series.

def HasPositiveLogConvexCoefficients (f : PowerSeries ℝ) : Prop :=
  0 < PowerSeries.coeff 0 f ∧
    ∀ n : ℕ, 0 < PowerSeries.coeff (n + 1) f ∧
      (PowerSeries.coeff (n + 1) f) ^ 2 ≤
        PowerSeries.coeff n f * PowerSeries.coeff (n + 2) f
Sources
Used by 3
Used byCoefficients of a positive log-convex series are positive · Kaluza's bounds for the coefficients of a reciprocal power series · Log-convexity of the coefficients

TheoremCoefficients of a positive log-convex series are positive#✓fully proved

If a real formal power series \(f\) has positive log-convex coefficients, then the coefficient of \(X^n\) in \(f\) is strictly positive for every natural number \(n\).

theorem HasPositiveLogConvexCoefficients.coeff_pos {f : PowerSeries ℝ}
    (hf : HasPositiveLogConvexCoefficients f) (n : ℕ) : 0 < PowerSeries.coeff n f
Uses 1 · Used by 1
Statement usesPositive log-convex coefficients
Used byKaluza's bounds for the coefficients of a reciprocal power series

TheoremLog-convexity of the coefficients#✓fully proved

If a real formal power series \(f = \sum_n a_n X^n\) has positive log-convex coefficients, then \(a_{n+1}^2 \le a_n a_{n+2}\) for every natural number \(n\).

theorem HasPositiveLogConvexCoefficients.sq_coeff_succ_le {f : PowerSeries ℝ}
    (hf : HasPositiveLogConvexCoefficients f) (n : ℕ) :
    (PowerSeries.coeff (n + 1) f) ^ 2 ≤ PowerSeries.coeff n f * PowerSeries.coeff (n + 2) f
Uses 1 · Used by 1
Statement usesPositive log-convex coefficients
Used byKaluza's bounds for the coefficients of a reciprocal power series

TheoremKaluza's bounds for the coefficients of a reciprocal power series#✓fully proved

Let \(f = \sum_n a_n X^n\) be a real formal power series with positive log-convex coefficients, and let \(f^{-1} = \sum_n b_n X^n\) be its reciprocal in the ring of formal power series. Then \(b_0 = a_0^{-1}\), \(b_0 > 0\), and \(-a_n / a_0^2 \le b_n \le 0\) for every \(n \ge 1\).

The reciprocal is formal; no convergence is assumed.

theorem kaluza_coeff_inv_bounds (f : PowerSeries ℝ)
    (hf : HasPositiveLogConvexCoefficients f) :
    PowerSeries.coeff 0 (f⁻¹) = (PowerSeries.coeff 0 f)⁻¹ ∧
      0 < PowerSeries.coeff 0 (f⁻¹) ∧
        ∀ n : ℕ, 1 ≤ n →
          -(PowerSeries.coeff n f) / (PowerSeries.coeff 0 f) ^ 2 ≤
            PowerSeries.coeff n (f⁻¹) ∧
          PowerSeries.coeff n (f⁻¹) ≤ 0
Sources
Uses 3
Statement usesPositive log-convex coefficients
Proof usesCoefficients of a positive log-convex series are positive · Log-convexity of the coefficients
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.