Source indexedlemma · leanprover/lean4:v4.32.0

integral_exp_div_split

PrimeNumberTheoremAnd.IEANTN.PVIdentity · PrimeNumberTheoremAnd/IEANTN/PVIdentity.lean:46 to 53

Mathematical statement

Exact Lean statement

lemma integral_exp_div_split {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    ∫ u in a..b, exp u / u = (∫ u in a..b, (exp u - 1) / u) + (log b - log a)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_exp_div_split {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :    ∫ u in a..b, exp u / u = (∫ u in a..b, (exp u - 1) / u) + (log b - log a) := by  simp +decide [ sub_div ];  rw [ intervalIntegral.integral_sub ];  · rw [ integral_inv_of_pos, Real.log_div ] <;> linarith;  · exact ContinuousOn.intervalIntegrable ( by exact continuousOn_of_forall_continuousAt fun u hu => ContinuousAt.div ( Real.continuous_exp.continuousAt ) continuousAt_id <| by linarith [ Set.mem_Icc.mp <| by simpa [ hab ] using hu ] ) ..;  · apply_rules [ ContinuousOn.intervalIntegrable ];    exact continuousOn_of_forall_continuousAt fun x hx => ContinuousAt.inv₀ continuousAt_id ( by cases Set.mem_uIcc.mp hx <;> linarith )