Source indexedlemma · leanprover/lean4:v4.32.0

intervalIntegrable_deriv_mul_B1

PrimeNumberTheoremAnd.EulerMaclaurin · PrimeNumberTheoremAnd/EulerMaclaurin.lean:41 to 49

Mathematical statement

Exact Lean statement

lemma intervalIntegrable_deriv_mul_B1 (ha : 0 ≤ a) (hab : a ≤ b) (h_cont : ContinuousOn (deriv f) [[a, b]]) :
    IntervalIntegrable (fun t ↦ deriv f t * B1 t) volume a b

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_deriv_mul_B1 (ha : 0 ≤ a) (hab : a ≤ b) (h_cont : ContinuousOn (deriv f) [[a, b]]) :    IntervalIntegrable (fun t ↦ deriv f t * B1 t) volume a b := by  refine IntervalIntegrable.continuousOn_mul ?_ h_cont  rw [intervalIntegrable_iff']  apply MeasureTheory.Measure.integrableOn_of_bounded (by simp) (by fun_prop) (M := 1 / 2)  filter_upwards [self_mem_ae_restrict (by measurability)] with x hx  rw [Set.uIcc_of_le hab, Set.mem_Icc] at hx  norm_cast  exact abs_B1_le_half (by linarith)