LiSeries.integral_log_inv_eq_integral_exp_div

theorem integral_log_inv_eq_integral_exp_div {a b : ℝ} (ha : 1 < a) (hb : a < b) :    ∫ t in a..b, 1 / log t = ∫ u in log a..log b, exp u / u := by  -- Use integral_comp_mul_deriv': ∫ u in α..β, (g ∘ f) u * f' u = ∫ t in f(α)..f(β), g t  -- with f = exp, α = log a, β = log b, g = (1/log ·)  -- Then g(eᵘ) · eᵘ = (1/u) · eᵘ = eᵘ/u  have ha0 : (0 : ℝ) < a := by linarith  have hb0 : (0 : ℝ) < b := by linarith  have hab : a ≤ b := le_of_lt hb  -- The change of variables formula gives:  -- ∫ u in log a..log b, (g ∘ exp) u * exp u = ∫ t in exp(log a)..exp(log b), g t  -- where g t = 1 / log t  have key : ∫ u in log a..log b, ((fun t => 1 / log t) ∘ exp) u * exp u =      ∫ t in exp (log a)..exp (log b), 1 / log t :=    intervalIntegral.integral_comp_mul_deriv'      (fun x _ => Real.hasDerivAt_exp x)      (continuous_exp.continuousOn)      ?_  · -- Simplify: exp(log a) = a, exp(log b) = b    rw [exp_log ha0, exp_log hb0] at key    rw [← key]    -- Show integrands agree: (1/log(exp u)) * exp u = exp u / u    apply intervalIntegral.integral_congr_ae    apply Filter.Eventually.of_forall    intro u _    simp only [Function.comp, Real.log_exp]    ring  · -- ContinuousOn (1/log ·) on (exp '' [[log a, log b]])    -- exp '' [[log a, log b]] ⊆ [[a, b]] where log > 0    apply ContinuousOn.mono (s := Set.Icc a b)    · apply ContinuousOn.div continuousOn_const      · exact continuousOn_log.mono (fun x hx => ne_of_gt (by linarith [hx.1]))      · intro x hx; exact ne_of_gt (Real.log_pos (by linarith [hx.1]))    · intro x hx      have hsub := exp_strictMono.monotone.image_uIcc_subset (a := log a) (b := log b) hx      rw [exp_log ha0, exp_log hb0] at hsub      rw [Set.uIcc_of_le (Real.log_le_log ha0 hab)] at hx      rw [Set.uIcc_of_le hab] at hsub      exact hsub