OAI/NumberTheory/Ostmann/Preliminaries/WeightedMomentShift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.weighted_moment_shift line 13

   Source documentation

   Minkowski for a countable weighted moment, stated without any measure construction. The weights may have infinite support.

   theorem weighted_moment_shift {ι : Type*} (w f : ι → ℝ)
       (hw : ∀ i, 0 ≤ w i) (hf : ∀ i, 0 ≤ f i) (b : ℝ) (hb : 0 ≤ b)
       (k : ℕ) (hk : 0 < k) (hws : Summable w)
       (hfs : Summable (fun i => w i * f i ^ k)) :
       Summable (fun i => w i * (f i + b) ^ k) ∧
         (∑' i, w i * (f i + b) ^ k) ≤
           ((∑' i, w i * f i ^ k) ^ (1 / (k : ℝ)) +
             b * (∑' i, w i) ^ (1 / (k : ℝ))) ^ k := by
   …