OAI/NumberTheory/Ostmann/Characters/BonamiMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sum_add_pow_bound_pos line 13
2. theorem OAI.Ostmann.eq_zero_of_sum_pow_le_zero line 53
3. theorem OAI.Ostmann.sum_add_pow_bound line 62

   Source documentation

   The finite-sum form needed for tensorization, with no analytic limits.

   theorem sum_add_pow_bound {ι : Type*} (s : Finset ι)
       (u v : ι → ℝ) (A B : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B)
       (hu : ∀ i ∈ s, 0 ≤ u i) (hv : ∀ i ∈ s, 0 ≤ v i) (l : ℕ) (hl : 0 < l)
       (hU : (∑ i ∈ s, u i ^ l) ≤ s.card * A ^ l)
       (hV : (∑ i ∈ s, v i ^ l) ≤ s.card * B ^ l) :
       (∑ i ∈ s, (u i + v i) ^ l) ≤ s.card * (A + B) ^ l := by
   …