Source indexedlemma · leanprover/lean4:v4.32.0

Complex.CartanBound.intervalIntegrable_sum_mul_phi_div

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:646 to 656

Mathematical statement

Exact Lean statement

lemma intervalIntegrable_sum_mul_phi_div
    {ι : Type} (s : Finset ι) (w : ι → ℝ) (a : ι → ℝ)
    (ha : ∀ i ∈ s, 0 < a i) {R : ℝ} (hR : 0 ≤ R) :
    IntervalIntegrable (∑ i ∈ s, fun r : ℝ => w i * φ (r / a i))
      volume R (2 * R)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_sum_mul_phi_div    {ι : Type} (s : Finset ι) (w : ι → ℝ) (a : ι → ℝ)    (ha : ∀ i ∈ s, 0 < a i) {R : ℝ} (hR : 0 ≤ R) :    IntervalIntegrable (∑ i ∈ s, fun r : ℝ => w i * φ (r / a i))      volume R (2 * R) := by  refine IntervalIntegrable.sum (μ := volume) (a := R) (b := 2 * R)    (s := s) (f := fun i : ι => fun r : ℝ => w i * φ (r / a i)) ?_  intro i hi  have hφi : IntervalIntegrable (fun r : ℝ => φ (r / a i)) volume R (2 * R) :=    intervalIntegrable_phi_div (a := a i) (R := R) (ha i hi) hR  simpa [mul_assoc] using hφi.const_mul (w i)