Source indexedlemma · leanprover/lean4:v4.32.0

tendsto_integral_exp_neg_div_Ioi

PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:122 to 129

Mathematical statement

Exact Lean statement

lemma tendsto_integral_exp_neg_div_Ioi :
    Tendsto (fun ε => ∫ t in (1:ℝ)..(1/ε), exp (-t) / t)
      (𝓝[>] (0 : ℝ)) (𝓝 (∫ t in Ioi (1:ℝ), exp (-t) / t))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_integral_exp_neg_div_Ioi :    Tendsto (fun ε => ∫ t in (1:ℝ)..(1/ε), exp (-t) / t)      (𝓝[>] (0 : ℝ)) (𝓝 (∫ t in Ioi (1:ℝ), exp (-t) / t)) := by  -- The function $\frac{\exp(-t)}{t}$ is continuous on $[1, \infty)$ by the properties of the exponential and logarithm functions.  simp [Real.exp_pos] at * ; have h_integrable : MeasureTheory.IntegrableOn (fun t : ℝ => Real.exp (-t) / t) (Set.Ioi 1) := by    exact integrableOn_exp_neg_div_Ioi;  apply_rules [ MeasureTheory.intervalIntegral_tendsto_integral_Ioi ];  norm_num [ Filter.Tendsto ]