Source indexedlemma · leanprover/lean4:v4.32.0

Real.tsum_inv_rpow_le_card_mul_of_lower_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:178 to 189

Source documentation

A finite shell whose radii are bounded below contributes at most card * lower_radius⁻¹ ^ τ to the inverse-power sum.

Exact Lean statement

lemma tsum_inv_rpow_le_card_mul_of_lower_bound {α : Type*} [Fintype α] {a : α → ℝ}
    {R τ : ℝ} (hR : 0 < R) (hτ : 0 < τ) (ha_nonneg : ∀ x, 0 ≤ a x)
    (ha_lower : ∀ x, R ≤ a x) :
    (∑' x : α, (a x)⁻¹ ^ τ) ≤ (Fintype.card α : ℝ) * (R⁻¹ ^ τ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tsum_inv_rpow_le_card_mul_of_lower_bound {α : Type*} [Fintype α] {a : α → ℝ}    {R τ : ℝ} (hR : 0 < R) (hτ : 0 < τ) (ha_nonneg : ∀ x, 0 ≤ a x)    (ha_lower : ∀ x, R ≤ a x) :    (∑' x : α, (a x)⁻¹ ^ τ) ≤ (Fintype.card α : ℝ) * (R⁻¹ ^ τ) := by  have hsum_le :      (∑ x : α, (a x)⁻¹ ^ τ) ≤ ∑ _x : α, R⁻¹ ^ τ := by    refine Finset.sum_le_sum ?_    intro x _hx    have hinv : (a x)⁻¹ ≤ R⁻¹ := by      simpa using (inv_anti₀ hR (ha_lower x))    exact Real.rpow_le_rpow (inv_nonneg.2 (ha_nonneg x)) hinv hτ.le  simpa [tsum_fintype, Finset.sum_const, nsmul_eq_mul, mul_comm] using hsum_le