Source indexedtheorem · leanprover/lean4:v4.32.0

RS_prime.ioiIntegral_tendsto_zero

PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime · PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:779 to 789

Mathematical statement

Exact Lean statement

theorem ioiIntegral_tendsto_zero {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : ℝ → E} {μ : Measure ℝ} (a : ℝ) (hfi : IntegrableOn f (Set.Ioi a) μ)
    {l : Filter ι} {b : ι → ℝ} [IsCountablyGenerated l] (hb : Tendsto b l atTop) :
    Tendsto (fun i => ∫ x in Set.Ioi (b i), f x ∂μ) l (𝓝 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem ioiIntegral_tendsto_zero {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]    {f : ℝ → E} {μ : Measure ℝ} (a : ℝ) (hfi : IntegrableOn f (Set.Ioi a) μ)    {l : Filter ι} {b : ι → ℝ} [IsCountablyGenerated l] (hb : Tendsto b l atTop) :    Tendsto (fun i => ∫ x in Set.Ioi (b i), f x ∂μ) l (𝓝 0) := by  have : ∀ᶠ i in l, ∫ x in Set.Ioi a, f x ∂μ - ∫ x in a..b i, f x ∂μ =    ∫ x in Set.Ioi (b i), f x ∂μ := by    filter_upwards [hb.eventually_mem (Ici_mem_atTop a)] with i hi    rw [sub_eq_iff_eq_add', intervalIntegral.interval_add_Ioi hfi      (hfi.mono_set (Set.Ioi_subset_Ioi hi))]  exact Tendsto.congr' this (sub_self (∫ x in Set.Ioi a, f x ∂μ) ▸ (Tendsto.const_sub _ <|    intervalIntegral_tendsto_integral_Ioi a hfi hb))