Bounded sequences satisfying a doubling Cauchy–Schwarz inequality

A real sequence b with 0 ≤ b 0 that is bounded above and satisfies the inequality b n ^ 2 ≤ b 0 * b (n + n) cannot increase at the first step: b 1 ≤ b 0. If it did, the ratio r = b 1 / b 0 would exceed 1 and repeated doubling would push b (2 ^ k) past b 0 * r ^ (2 ^ k), which is unbounded.

The inequality is the shape of the Cauchy–Schwarz inequality for a positive-semidefinite Hankel sequence, or for the correlations ω (a⋆ α_{is}(a)) of a positive functional invariant under a one-parameter group α.

Main declarations

• TauCeti.apply_one_le_apply_zero_of_sq_le_mul: such a sequence satisfies b 1 ≤ b 0.

theorem TauCeti.apply_one_le_apply_zero_of_sq_le_mul {b : ℕ → ℝ} {D : ℝ} (hb0 : 0 ≤ b 0) (hsq : ∀ (n : ℕ), b n ^ 2 ≤ b 0 * b (n + n)) (hbd : ∀ (n : ℕ), b n ≤ D) : b 1 ≤ b 0

A bounded sequence of reals with 0 ≤ b 0 whose squares satisfy the Cauchy–Schwarz inequality b n ^ 2 ≤ b 0 * b (n + n) cannot increase at the first step.