Sums weighted by (1 + ‖x‖) ^ s

On a seminormed additive group, the weights (1 + ‖x‖) ^ s define the weighted ℓ² spaces. On the circle these correspond, through Fourier coefficients, to the Sobolev spaces H^s. This file records two facts about sums with these weights, stated for unconditional sums in ℝ≥0∞.

Main statements

• TauCeti.sq_tsum_le_tsum_one_add_norm_rpow_mul: by the Cauchy–Schwarz inequality, a weighted ℓ² family is summable whenever the weights (1 + ‖x‖) ^ (-2 s) are: (∑' x, h x) ^ 2 ≤ (∑' x, (1 + ‖x‖) ^ (-2 s)) * ∑' x, ((1 + ‖x‖) ^ s * h x) ^ 2.
• TauCeti.ofReal_sq_one_add_abs_rpow_mul_norm: on ℤ, the real weighted square ((1 + |n|) ^ s * ‖v‖) ^ 2 in ℝ≥0∞ is ((1 + ‖n‖) ^ s * ‖v‖ₑ) ^ 2. This converts between real weighted sums on ℤ and the ℝ≥0∞ sums used here.

theorem TauCeti.sq_tsum_le_tsum_one_add_norm_rpow_mul {G : Type u_1} [SeminormedAddGroup G] (s : ℝ) (h : G → ENNReal) : (∑' (x : G), h x) ^ 2 ≤ (∑' (x : G), ENNReal.ofReal ((1 + ‖x‖) ^ (-2 * s))) * ∑' (x : G), (ENNReal.ofReal ((1 + ‖x‖) ^ s) * h x) ^ 2

Weighted ℓ² bounds ℓ¹. By the Cauchy–Schwarz inequality, (∑' x, h x) ^ 2 ≤ (∑' x, (1 + ‖x‖) ^ (-2 s)) * ∑' x, ((1 + ‖x‖) ^ s * h x) ^ 2 for every family h in ℝ≥0∞. On ℤ the first factor is finite for s > 1 / 2 (TauCeti.summable_one_add_abs_int_rpow).

theorem TauCeti.ofReal_sq_one_add_abs_rpow_mul_norm {X : Type u_1} [SeminormedAddGroup X] (s : ℝ) (n : ℤ) (v : X) : ENNReal.ofReal (((1 + |↑n|) ^ s * ‖v‖) ^ 2) = (ENNReal.ofReal ((1 + ‖n‖) ^ s) * ‖v‖ₑ) ^ 2

On ℤ, the real weighted square ((1 + |n|) ^ s * ‖v‖) ^ 2, viewed in ℝ≥0∞, is ((1 + ‖n‖) ^ s * ‖v‖ₑ) ^ 2.