Theorems · Theorem · number theory

locallyIntegrableOn_mul_sum_Icc

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {a : ℝ} {m : ℕ},
  0 ≤ a →
    ∀ {g : ℝ → 𝕜},
      MeasureTheory.LocallyIntegrableOn g (Set.Ici a) MeasureTheory.volume →
        MeasureTheory.LocallyIntegrableOn (fun t => g t * ∑ k ∈ Finset.Icc m ⌊t⌋₊, c k) (Set.Ici a) MeasureTheory.volume

Defined in: Mathlib.NumberTheory.AbelSummation
Cited by: 2 results in Mathlib
Foundations: Depth 247 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RCLike

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites29

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
Realstatement and proof · cited by 25,697
Finset.sumstatement and proof · cited by 5,195
LE.le.transproof · cited by 3,151
RCLikestatement and proof · cited by 2,829
Set.Nonemptyproof · cited by 2,627
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
IsCompactproof · cited by 1,282
Set.Icistatement and proof · cited by 1,070
InfSet.sInfproof · cited by 935
MeasureTheory.IntegrableOnproof · cited by 548
Finset.Iccstatement and proof · cited by 348

Cited by2

Results whose statement or proof uses this declaration.

tendsto_sum_mul_atTop_nhds_one_sub_integralproof · cited by 0
tendsto_sum_mul_atTop_nhds_one_sub_integral₀proof · cited by 0